Encoding TLA+ into Many-Sorted First-Order Logic

Stephan Merz and Hernán Vanzetto

Abstract

This paper presents an encoding of a non-temporal fragment of the TLA+ language, which includes untyped set theory, functions, arithmetic expressions, and Hilbert's ε 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 TLA+ Proof System.

© Springer 2016

Available as: PDF

Reference

@InProceedings{azmy:rigorous,
  author =       {Stephan Merz and Hern{\'a}n Vanzetto},
  title =        {Encoding {TLA+} into Many-Sorted First-Order Logic},
  booktitle =    {5th Intl. Conf. Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016)},
  publisher = {Springer},
  year =      2016,
  editor =    {Michael Butler and Klaus-Dieter Schewe and Atif Mashkoor and Mikl{\'o}s Bir{\'o}},
  series =    {LNCS},
  volume =    {9675},
  pages =     {54-69},
}