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

摘要

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 e 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.