The Nelson-Oppen combination method combines decision procedures for first-order theories satisfying certain conditions into a single decision procedure for the union theory. The Nelson-Oppen combination method can be applied only if the signatures of the combined theories are disjoint.
Combination tableaux (C-tableaux) are an extension of Smullyan tableaux for combining first-order theories whose signatures may not be disjoint. C-tableaux are sound and complete, but not terminating in general.
In this paper we show that, when we combine first-order theories that share the theory of dense orders, C-tableaux can be made terminating without sacrificing completeness. Thus, C-tableaux provide a decision procedure for the combination of first-order theories sharing the theory of dense orders.
In Automated Reasoning with Analytic Tableaux and Related Methods: Position Papers and Tutorials Marta Cialdea Mayer and Fiora Pirri, editors. Technical Report RT-DIA-80-2003, pages 83-98, Università di Roma Tre. Aracne Editrice, 2003
Postscript, PDF. © 2003, Springer Verlag.