The combination problem in automated reasoning
Zohar Manna, Calogero G. Zarba · 2004
Decision procedures are algorithms that can reason about the validity or satisfiability of logical formulae in a given decidable theory, and that always terminate with a positive or negative answer. The major advantage of decision procedures is efficiency. It is often possible to obtain a fast and efficient decision procedure for a specific domain by cleverly exploiting the structure of the domain itself. However, this efficiency comes at the price of specialization. Most reasoning problems typically involve a complex mixture of multiple domains, which means that a decision procedure for a specific domain can be applied only if it can be combined with the decision procedures for the other domains. One of the first and most important results in the field of combination was obtained by Nelson and Oppen, who presented a method for combining decision procedures for first-order theories satisfying certain conditions into a single decision procedure for the union theory. Although the Nelson-Oppen method is still considered to be state-of-the-art, it has two major restrictions: (1) the theories to combine must be stably infinite; (2) the signatures of the theories must be disjoint. In this thesis we introduce new techniques for relaxing the restrictions of the Nelson-Oppen method, thus widening the range of reasoning problems that can be solved with combination methods. Our main contributions include: (1) new combination methods that address the problem of combining theories that are not stably infinite; (2) the introduction of Combination tableaux (C-tableaux), a general framework, based on Smullyan tableaux, that can be seen as a generalization of the Nelson-Oppen method to the combination of arbitrary theories, not necessarily stably infinite, and not necessarily over disjoint signatures; (3) new combination methods for combining sets and multisets with integers.