| 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. |
