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

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, LPAR-19: Logic for Programming, Artificial Intelligence, and Reasoning: 19th International Conference, 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.

D. Hansen and M. Leuschel, Translating TLA???+??? to B for Validation with ProB, Proceedings of the 9th International Conference on Integrated Formal Methods, IFM'12, pp.24-38, 2012.
DOI : 10.1007/978-3-642-30729-4_3

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, Proceedings of the Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ'12, 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, Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'12, 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, Electronic Comm. of the European Assoc. of Software Science and Technology, vol.53, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00760579

S. Merz and H. Vanzetto, Refinement Types for tla ???+???, NASA Formal Methods: 6th International Symposium, NFM 2014, pp.143-157, 2014.
DOI : 10.1007/978-3-319-06200-6_11
URL : https://hal.archives-ouvertes.fr/hal-01063516

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

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