Encoding TLA+ set theory into many-sorted first-order logic
classification
💻 cs.LO
keywords
encodingfirst-orderlogicmany-sortedsolverstheoryback-endcomponent
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.