On the Convexity of a Fragment of Pure Set Theory with Applications within a Nelson-Oppen Framework

TL;DR

This paper proves that a specific fragment of set theory, Multi-Level Syllogistic, is convex, enabling efficient polynomial-time decision procedures within the Nelson-Oppen SMT framework.

Contribution

It establishes the convexity of the Multi-Level Syllogistic fragment of set theory, facilitating its integration into efficient SMT solving methods.

Findings

Proves convexity of Multi-Level Syllogistic fragment.

Enables polynomial-time decision procedures for this set theory fragment.

Facilitates integration into Nelson-Oppen SMT framework.

Abstract

The Satisfiability Modulo Theories (SMT) issue concerns the satisfiability of formulae from multiple background theories, usually expressed in the language of first-order predicate logic with equality. SMT solvers are often based on variants of the Nelson-Oppen combination method, a solver for the quantifier-free fragment of the combination of theories with disjoint signatures, via cooperation among their decision procedures. When each of the theories to be combined by the Nelson-Oppen method is convex (that is, any conjunction of its literals can imply a disjunction of equalities only when it implies at least one of the equalities) and decidable in polynomial time, the running time of the combination procedure is guaranteed to be polynomial in the size of the input formula. In this paper, we prove the convexity of a fragment of Zermelo-Fraenkel set theory, called Multi-Level Syllogistic, most of whose polynomially decidable fragments we have recently characterized.