Encoding TLA+ set theory into many-sorted first-order logic
Stephan Merz, Hernán Vanzetto · arXiv (Cornell University) · 2015
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.