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.
@article{arxiv.1508.03838,
title = {Encoding TLA+ set theory into many-sorted first-order logic},
author = {Stephan Merz and Hernán Vanzetto},
journal= {arXiv preprint arXiv:1508.03838},
year = {2015}
}