Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing

We propose a general way of combining background reasoners in theory reasoning. Using a restricted version of the Craig interpolation lemma, we show that background reasoner cooperation can be achieved as a form of constraint propagation, much in the spirit of existing combination methods for decision procedures. In this case, constraint information is propagated across reasoners eexchanging residues that are, in essence, disjunctions of ground literals over a common signature. As an application of our approach, we describe a multitheory version of the semantic tableau calculus, and we prove it sound and complete.