Abstract
The Nelson-Oppen combination method combines ground satisfiability checkers for first-order theories satisfying certain conditions into a single ground satisfiability checker for the union theory. The most significant restriction that the combined theories must satisfy, for the Nelson-Oppen combination method to be applicable, is that they must have disjoint signatures. Unfortunately, this is a very serious restriction since many combination problems concern theories over non-disjoint signatures.
In this paper we present a tableau calculus for combining first-order theories over non-disjoint signatures. The calculus generalizes the Nelson-Oppen combination method to formulae with quantifiers and to the union of arbitrary theories over non necessarily disjoint signatures.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alessandro Armando, Silvio Ranise, and Michaël Rusinowitch. Uniform derivation of decision procedures by superposition. In Laurent Fribourg, editor, Computer Science Logic, volume 2142 of Lecture Notes in Computer Science, pages 513–527. Springer, 2001.
Franz Baader and Cesare Tinelli. Combining decision procedures for positive theories sharing constructors. In Sophie Tison, editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science. Springer, 2002.
Jean-Paul Billon. The disconnection method. A confluent integration of unification in the analytic framework. In Pierangelo Miglioli, Ugo Moscato, Daniele Mundici, and Mario Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, volume 1071 of Lecture Notes in Artificial Intelligence, pages 110–126. Springer, 1996.
Eric Domenjoud, Francis Klay, and Christophe Ringeissen. Combination techniques for non-disjoint equational theories. In Alan Bundy, editor, Automated Deduction-CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 267–281. Springer, 1994.
Melvin C. Fitting. First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Springer, 2nd edition, 1996.
Bernhard Gramlich. On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems. Theoretical Computer Science, 165(1):97–131, 1996.
Thomas Kaufl and Nicolas Zabel. Cooperation of decision procedures in a tableau-based theorem prover. Reveu d’Intelligence Artificielle, 4(3):99–126, 1990.
Shie-Jue Lee and David A. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 9(1):25–42, 1992.
Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979.
Enno Ohlebusch. Modular properties of composable term rewriting systems. Journal of Symbolic Computation, 20(1):1–41, 1995.
Christophe Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Andrei Vonronkov, editor, Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Artificial Intelligence, pages 261–272. Springer, 1992.
Christophe Ringeissen. Cooperation of decision procedures for the satisfiability problem. In Franz Baader and Klaus U. Schulz, editors, Frontiers of Combining Systems, volume 3 of Applied Logic Series, pages 121–140. Kluwer Academic Publishers, 1996.
Raymond M. Smullyan. First-Order Logic. Springer, 1968.
Cesare Tinelli. Cooperation of background reasoners in theory reasoning by residue sharing. Technical Report 02-03, Department of Computer Science, University of Iowa, 2002.
Cesare Tinelli and Mehdi T. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In Franz Baader and Klaus U. Schulz, editors, Frontiers of Combining Systems, volume 3 of Applied Logic Series, pages 103–120. Kluwer Academic Publishers, 1996.
Cesare Tinelli and Christophe Ringeissen. Unions of non-disjoint theories and combinations of satisfiability procedures. Technical Report 01-02, Department of Computer Science, University of Iowa, 2001.
Ashish Tiwari. Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook, 2000.
Calogero G. Zarba. Combining non-disjoint theories. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, International Joint Conference on Automated Reasoning (Short Papers), Technical Report DII 11/01, pages 180–189. University of Siena, Italy, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zarba, C.G. (2002). A Tableau Calculus for Combining Non-disjoint Theories. In: Egly, U., Fermüller, C.G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2002. Lecture Notes in Computer Science(), vol 2381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45616-3_22
Download citation
DOI: https://doi.org/10.1007/3-540-45616-3_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43929-5
Online ISBN: 978-3-540-45616-2
eBook Packages: Springer Book Archive