Encoding TLA + + into Many-Sorted First-Order Logic

Abstract

This paper presents an encoding of a non-temporal fragment of the ({\textsc {TLA}} ^{{+}}) language, which includes untyped set theory, functions, arithmetic expressions, and Hilbert’s (\varepsilon ) operator, into many-sorted first-order logic, the input language of state-of-the-art smt solvers. This translation, based on encoding techniques such as boolification, injection of unsorted expressions into sorted languages, term rewriting, and abstraction, is the core component of a back-end prover based on smt solvers for the ({\textsc {TLA}} ^{{+}}) Proof System.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{MerzV16,
  author       = {Stephan Merz and
                  Hern{\'{a}}n Vanzetto},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {Encoding {TLA} {\^{}}+ + into Many-Sorted First-Order Logic},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {54--69},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_3},
  doi          = {10.1007/978-3-319-33600-8\_3},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/MerzV16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}