Encoding TLA+ into many-sorted first-order logic

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