Combining Theories Sharing Dense Orders

Calogero Zarba, Zohar Manna, Henny Sipma

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.


© Henny Sipma / sipma@cs.stanford.edu
Last modified: Thu Jan 12 14:40:50 PDT 2004