The Nelson-Oppen framework can be used to build a decision procedure for the combination
of two disjoint decidable stably infinite theories.
We study the more general case of combining theories for which there exist refutationally complete
procedures. We consider two cases and provide complete (semi-)algorithms for them. First, we
show that it is possible under minor technical conditions to combine a decidable
(not necessarily stably infinite) theory and a disjoint finitely axiomatize theory, obtaining a refutationally
complete procedure. Second, we provide a refutationally complete procedure for the union of two
disjoint finitely axiomatized theories, that uses the assumed procedures for the underlying theories without
modifying them.
(Joint work with Stephan Merz and Christoph Weidenbach)