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

Stephan Merz 1, 2 Hernán Vanzetto 2, 1
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Preprints, Working Papers, ...
Liste complète des métadonnées

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01244627
Contributor : Stephan Merz <>
Submitted on : Wednesday, December 16, 2015 - 9:13:21 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Thursday, March 17, 2016 - 11:30:18 AM

File

sets2015.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01244627, version 1
  • ARXIV : 1508.03838

Collections

Citation

Stephan Merz, Hernán Vanzetto. Encoding TLA+ set theory into many-sorted first-order logic. 2015. ⟨hal-01244627⟩

Share

Metrics

Record views

511

Files downloads

88