J. Avigad, Eliminating definitions and Skolem functions in first-order logic, ACM Transactions on Computational Logic, vol.4, issue.3, pp.402-415, 2003.
DOI : 10.1145/772062.772068

F. Baader and T. Nipkow, Term rewriting and all that, 1999.

C. Barrett, A. Stump, and C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2010.

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Journal of Automated Reasoning, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.194.1769

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, 14th Intl. Conf. LPAR, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13

URL : https://hal.archives-ouvertes.fr/inria-00315920

D. Déharbe, P. Fontaine, Y. Guyot, and L. Voisin, SMT Solvers for Rodin, 3rd Intl. Conf. Abstract State Machines, Alloy, B, VDM, and Z, pp.194-207, 2012.
DOI : 10.1007/978-3-642-30885-7_14

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LNCSARCoSS, vol.8312, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20

URL : https://hal.archives-ouvertes.fr/hal-00909784

J. R. Douceur, J. R. Lorch, B. Parno, J. Mickens, and J. M. Mccune, Memoir? Formal Specs and Correctness Proofs, 2011.

M. Jacquel, K. Berkani, D. Delahaye, and C. Dubois, Tableaux Modulo Theories Using Superdeduction, Proc. of the 6th Intl. Joint Conf. on Automated Reasoning, IJCAR'12, pp.332-338
DOI : 10.1007/978-3-642-31365-3_26

URL : https://hal.archives-ouvertes.fr/hal-01099338

M. Konrad and L. Voisin, Translation from set-theory to predicate calculus, 2012.

L. Lamport, Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers, 2002.

M. Manzano, Extensions of First-Order Logic. Cambridge Tracts in Theoretical Computer Science, 2005.

D. Mentré, C. Marché, J. Filliâtre, and M. Asuka, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, Proc. of the 3rd Intl. Conf. ABZ, pp.238-251, 2012.
DOI : 10.1007/978-3-642-30885-7_17

S. Merz and H. Vanzetto, Automatic Verification of TLA???+??? Proof Obligations with SMT Solvers, Lecture Notes in Computer Science, vol.7180, pp.289-303, 2012.
DOI : 10.1007/978-3-642-28717-6_23

URL : https://hal.archives-ouvertes.fr/hal-00760570

S. Merz and H. Vanzetto, Harnessing SMT Solvers for TLA + Proofs, ECEASST, vol.53, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00760579

S. Merz and H. Vanzetto, Refinement Types for tla ???+???, NASA Formal Methods, pp.143-157, 2014.
DOI : 10.1007/978-3-319-06200-6_11

URL : https://hal.archives-ouvertes.fr/hal-01063516

J. Urban, Translating Mizar for First Order Theorem Provers, Mathematical Knowledge Management, pp.203-215, 2003.
DOI : 10.1007/3-540-36469-2_16