Encoding TLA+ set theory into many-sorted first-order logic

Stephan Merz (1, 2) , Hernán Vanzetto (2, 1)

1 MSR - INRIA - Microsoft Research - Inria Joint Centre
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems

We present an encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This translation is the main component of a back-end prover based on SMT solvers in the TLA+ Proof System.

Domaines: Logique en informatique [cs.LO]

Stephan Merz, Hernán Vanzetto. Encoding TLA+ set theory into many-sorted first-order logic. 2015. ⟨hal-01244627⟩