J. Abrial, Modeling in Event-B ? System and Software Engineering, 2010.

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
URL : http://repository.cmu.edu/cgi/viewcontent.cgi?article=1041&context=philosophy

S. Azaiez, D. Doligez, M. Lemerre, T. Libal, S. Merz et al., Proving Determinacy of the PharOS Real-Time Operating System, 5th Intl. Conf. Abstract State Machines, pp.70-85, 2016.
DOI : 10.1007/978-3-319-33600-8_4
URL : https://hal.archives-ouvertes.fr/hal-01322335

N. Azmy and C. Weidenbach, Computing Tiny Clause Normal Forms, Proceedings of the 24th International Conference on Automated Deduction, CADE'13, pp.109-125, 2013.
DOI : 10.1007/978-3-642-38574-2_7
URL : https://hal.archives-ouvertes.fr/hal-00931893

N. Azmy, S. Merz, C. Weidenbach-alloy, B. Tla, and Z. Vdm, A Rigorous Correctness Proof for Pastry, pp.86-101, 2016.
DOI : 10.1007/978-3-319-33600-8_5
URL : https://hal.archives-ouvertes.fr/hal-01322342

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.13, issue.5, pp.109-128, 2013.
DOI : 10.1016/B978-044450813-3/50029-1

S. Conchon, E. Contejean, J. Kanig, and S. Lescuyer, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Electronic Notes in Theoretical Computer Science, vol.198, issue.2, pp.51-69, 2008.
DOI : 10.1016/j.entcs.2008.04.080

S. Conchon and M. Iguernelala, Tuning the Alt-Ergo SMT Solver for B Proof Obligations, Lecture Notes in Computer Science, vol.8477, pp.294-297, 2014.
DOI : 10.1007/978-3-662-43652-3_27
URL : https://hal.archives-ouvertes.fr/hal-01093000

L. De-moura and N. Bjorner, Z3: An Efficient SMT Solver, 14th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

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 (ABZ 2012), 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

A. Grabowski, A. Kornilowicz, and A. Naumowicz, Mizar in a Nutshell, Journal of Formalized Reasoning, vol.3, issue.2, pp.152-245, 2010.

D. Hansen and M. , Translating TLA???+??? to B for Validation with ProB, Proceedings of the 9th Intl. Conference on Integrated Formal Methods, IFM'12, pp.24-38, 2012.
DOI : 10.1007/978-3-642-30729-4_3
URL : http://www.stups.uni-duesseldorf.de/mediawiki/images/1/1c/Pub-HansenLeuschelTLA2012.pdf

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

P. B. Jackson and G. O. Passmore, Proving SPARK Verification Conditions with SMT solvers, 2009.

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras . Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

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

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

L. Lamport and L. C. Paulson, Should your specification language be typed, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.502-526, 1999.
DOI : 10.1145/319301.319317

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

D. Mentré, C. Marché, J. Filliâtre, M. Asuka, Z. Vdm et al., Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, Proceedings of the Third International Conference on Abstract State Machines, 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, pp.2012-289
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 Communications of the European Assoc. of Software, Science and Technology, vol.53

S. Merz, H. Vanzetto, M. J. Butler, K. Schewe, A. Mashkoor et al., Encoding TLA + into Many-Sorted First-Order Logic Abstract State Machines, VDM, and Z -5th International Conference, pp.54-69, 2016.
DOI : 10.1007/978-3-319-33600-8_3

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

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: a proof assistant for higher-order logic, LNCS, vol.2283, 2002.
DOI : 10.1007/3-540-45949-9

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, Handbook of Automated Reasoning, pp.335-367, 2001.
DOI : 10.1016/B978-044450813-3/50008-4

L. C. Paulson, Set theory for verification: I. From foundations to functions, Journal of Automated Reasoning, vol.8, issue.1, pp.353-389, 1993.
DOI : 10.1007/BF00881873

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

G. S. Tseitin, On the complexity of derivation in propositional calculus, Studies in constructive mathematics and mathematical logic, pp.115-12510, 1968.

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

C. Weidenbach, SPASS: Combining superposition, sorts and splitting. Handbook of automated reasoning, pp.1965-2013, 1999.

Y. Zheng, V. Ganesh, S. Subramanian, O. Tripp, M. Berzish et al., Z3str2: an efficient solver for strings, regular expressions, and length constraints, Formal Methods in System Design, vol.22, issue.4, pp.249-288, 2017.
DOI : 10.1145/2491411.2491456