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

Stephan Merz, Hernán Vanzetto

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…