Combining Non-Stably In¯nite Theories

Abstract. The Nelson-Oppen combination method combines decision procedures for ¯rst-order theories over disjoint signatures into a single decision procedure for the union theory. To be correct, the method requires that the component theories be stably in¯nite. This restriction makes the method inapplicable to many interesting theories such as, for instance, theories having only ¯nite models. In this paper, we describe two extensions of the Nelson-Oppen method that address the problem of combining theories that are not stably in¯nite. In our ex-tensions, the component decision procedures exchange not only equalities between shared variables, but also certain cardinality constraints. Applications of our results include the combination of theories having only ¯nite models, as well as the combination of non-stably in¯nite theories with the theory of equality, the theories of total and partial orders, and the theory of lattices with maximum and minimum