Encoding TLA+ set theory into many-sorted first-order logic
Abstract
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.
Origin : Files produced by the author(s)
Loading...