Abstract
This work1 is concerned with basic issues of the design of calculi and proof procedures for first-order connection methods and tableaux calculi. Proof procedures for these type of calculi developed so far suffer from not exploiting proof confluence, and very often unnecessarily rely on a heavily backtrack oriented control regime.
As a new result, we present a variant of a connection calculus and prove its strong completeness. This enables the design of backtrack-free contro regimes. To demonstrate that the underlying fairness condition is reasonably implementable we define an effective search strategy.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
F. Baader and K. U. Schulz. Unification Theory. In W. Bibel and P. H. Schmitt, editors, Automated Deduction. A Basis for Applications. Kluwer, 1998.
P. Baumgartner. Hyper Tableaux — The Next Generation. In H. de Swaart, editor, Automated Reasoning with Analytic Tableaux and Related Methods. LNAI 1397, Springer, 1998. 4 This strategy resembles much a tableau procedure-one that takes advantage of confluence, however.
P. Baumgartner, N. Eisinger, and U. Furbach. A Confluent Connection Calculus. Fachberichte Informatik 23–98, Universität Koblenz-Landau, Universität Koblenz-Landau, D-56075 Koblenz, 1998.
P. Baumgartner, U. Furbach, and I. Niemelä. Hyper Tableaux. In Proc. JELIA 96, LNAI 1126. Springer, 1996.
B. Beckert and J. Posegga. leanTAP: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.
W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.
J.-P. Billon. The Disconnection Method. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071. Springer, 1996.
F. Bry and N. Eisinger. Unit resolution tableaux. Research Report PMS-FB-1996-2, Institut für Informatik, LMU München, 1996.
M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.
H. Fujita and R. Hasegawa. A Model Generation Theorem Prover in KL1 using a Ramified-Stack Algorithm. In Proc.8th of the Eighth International Conference on Logic Programming, pages 535–548, Paris, France, 1991.
R. Hähnle, B. Beckert, and S. Gerberding. The Many-Valued Theorem Prover 3TAP. Interner Bericht 30/94, Universität Karlsruhe, 1994.
R. Hähnle and S. Klingenbeck. A-Ordered Tableaux. Journal of Logic and Computation, 6(6):819–833, 1996.
R. Hähnle and C. Pape. Ordered tableaux: Extensions and applications. In D. Galmiche, editor, Automated Reasoning with Analytic Tableaux and Related Methods, LNAI 1227, pages 173–187. Springer, 1997.
S. Klingenbeck and R. Hähnle. Semantic tableaux with ordering restrictions. In A. Bundy, editor, CADE 12, LNAI 814, pages 708–722. Springer, 1994.
D. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1968.
R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In E. Lusk and R. Overbeek, editors, CADE 9, LNCS 310, pages 415–434. Springer, 1988.
D. A. Plaisted and Y. Zhu. Ordered Semantic Hyper Linking. In Proceedings of AAAI-97, 1997.
D. Prawitz. An improved proof procedure. Theoria, 26:102–139, 1960.
A. Voronkov. Strategies in rigid-variable methods. In IJCAI 97, Nagoya, 1997.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baumgartner, P., Eisinger, N., Furbach, U. (1999). A Confluent Connection Calculus. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_30
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive