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

TL;DR

This paper introduces a method to encode TLA+ set theory into many-sorted first-order logic, enabling the use of SMT solvers for formal verification within the TLA+ Proof System.

Contribution

It presents a novel encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic for SMT solvers, integrated into the TLA+ Proof System.

Findings

Effective encoding of set theory into SMT-compatible logic

Integration with TLA+ Proof System enhances verification capabilities

Facilitates automated reasoning using SMT solvers

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.