2 papers
cs.LO2015
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…
cs.SE2012
TLA+ Proofs
Denis Cousineau, Damien Doligez, Leslie Lamport +3
TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them wi…