L. Bachmair, N. Dershowitz, and J. Hsiang, Orderings for equational proofs, LICS '86, pp.346-357, 1986.
DOI : 10.1007/978-1-4684-7118-2_1

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994.

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi´cjovanovi´c et al., CAV 2011, vol.6806, pp.171-177, 2011.

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB standard: Version 2.7. Tech. rep., University of Iowa, 2017.

C. Barrett, I. Shikanian, and C. Tinelli, An abstract decision procedure for satisfiability in the theory of inductive data types, J. Satisf. Boolean Model. Comput, vol.3, pp.21-46, 2007.

N. S. Bjørner, Integrating Decision Procedures for Temporal Verification, 1998.

J. C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu et al., Truly modular (co)datatypes for Isabelle/HOL, ITP 2014, vol.8558, pp.93-110, 2014.
DOI : 10.1007/978-3-319-08970-6_7
URL : http://eprints.mdx.ac.uk/15167/1/codat-impl.pdf

J. C. Blanchette, N. Peltier, and S. Robillard, Superposition with datatypes and codatatypes, 2018.
DOI : 10.1007/978-3-319-94205-6_25
URL : https://hal.archives-ouvertes.fr/hal-01904588

H. Comon and P. Lescanne, Equational problems and disunification, J. Symb. Comput, vol.7, issue.3-4, pp.371-425, 1989.
DOI : 10.1016/s0747-7171(89)80017-3
URL : https://hal.archives-ouvertes.fr/inria-00075652

S. Cruanes, Superposition with structural induction, FroCoS 2017, vol.10483, pp.172-188, 2017.
DOI : 10.1007/978-3-319-66167-4_10
URL : https://hal.archives-ouvertes.fr/tel-01223502

A. Kersani and N. Peltier, Combining superposition and induction: A practical realization, FroCoS 2013, vol.8152, pp.7-22, 2013.
DOI : 10.1007/978-3-642-40885-4_2
URL : https://hal.archives-ouvertes.fr/hal-00934610

L. Kovács, S. Robillard, and A. Voronkov, Coming to terms with quantified reasoning, pp.260-270, 2017.

L. Kovács and A. Voronkov, First-order theorem proving and Vampire, Computer Aided Verification (CAV 2013), vol.8044, pp.1-35

. Springer, , 2013.

K. R. Leino and M. Moskal, Co-induction simply-Automatic co-inductive proofs in a program verifier, FM 2014, vol.8442, pp.382-398, 2014.

L. De-moura and N. Bjørner, Z3: An efficient SMT solver, TACAS 2008, vol.4963, pp.337-340, 2008.

R. Nieuwenhuis and A. Rubio, Paramodulation-based theorem proving, Handbook of Automated Reasoning, vol.I, pp.371-443, 2001.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol.2283, 2002.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, IWIL-2010. EPiC, vol.2, pp.1-11, 2012.

T. Pham and M. W. Whalen, RADA: A tool for reasoning about algebraic data types with abstractions, ESEC/FSE '13, pp.611-614, 2013.

A. Reynolds and J. C. Blanchette, A decision procedure for (co)datatypes in SMT solvers, J. Autom. Reason, vol.58, issue.3, pp.341-362, 2017.
DOI : 10.1007/978-3-319-21401-6_13
URL : https://hal.archives-ouvertes.fr/hal-01397082

A. Reynolds and V. Kuncak, Induction for SMT solvers, VMCAI 2015, vol.8931, pp.80-98, 2014.
DOI : 10.1007/978-3-662-46081-8_5

S. Robillard, An inference rule for the acyclicity property of term algebras, EPiC, EasyChair, 2017.

P. Suter, A. S. Köksal, and V. Kuncak, Satisfiability modulo recursive programs, SAS 2011, vol.6887, pp.298-315, 2011.
DOI : 10.1007/978-3-642-23702-7_23
URL : http://lara.epfl.ch/%7Ekuncak/papers/SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf

D. Wand, Superposition: Types and Polymorphism, 2017.