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

Domenico Cantone, Andrea De Domenico, Pietro Maugeri

The Satisfiability Modulo Theories (SMT) issue concerns the satisfiability of formulae from multiple background theories, usually expressed in the language of first-order predicate…