Abstract
The connection or matings method (Andrews, 1981; Bibel, 1981; Bibel, 1987) and tableau calculi with connections like model elimination (Loveland, 1968) are related paradigms in automated deduction. While this is intuitively evident, the precise relations and differences have not been sufficiently investigated so far. In this paper, we give a thorough exposition of the two frameworks and illustrate that a careful analysis of the relations may lead to advances in automated deduction in general. We begin with a brief comparison of the inherent principles of both paradigms.
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
P. Andrews. (1981). Theorem Proving via General Matings. Journal of the Association for Computing Machinery, 28 (2): 193–214.
O. W. Astrachan and M. E. Stickel. (1992). Caching and Lemmaizing in Model Elimination Theorem Provers. Proceedings of the 11th Conference on Automated Deduction (CADE-11), LNAI 607, pages 224–238, Springer.
M. Baaz and A. Leitsch. (1992). Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic, 57: 181–215.
W. Bibel. (1981). On Matrices with Connections. Journal of the ACM, 28: 633–645.
W. Bibel. (1987). Automated Theorem Proving. Vieweg, second edition.
M. Davis and H. Putnam. (1960). A Computing Procedure for Quantification Theory. Journal of the ACM, 7: 201–215.
M. Davis, G. Logemann, and D. Loveland. (1962). A Machine Program for Theorem Proving. Communications of the ACM, 5 (7): 394–397.
M. Fitting. (1996). First-Order Logic and Automated Theorem Proving,Springer, seconnd edition.
O. Ibens and R. Letz. (1997). Subgoal Alternation in Model Elimination. In Proceedings of TABLEAUX’97,LNAI 1227, pages 201–215, Springer.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. (1992). SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8 (2): 183–212.
R. Letz, K. Mayr, and C. Goller. (1994). Controlled Integration of the Cut Rule into Connection Tableaux Calculi. Journal of Automated Reasoning, 13: 297–337.
R. Letz. (1998). Clausal Tableaux. In W. Bibel, P. H. Schmitt, editors, Automated Deduction. A basis for applications,Vol. 1, pages 39–68, Kluwer.
R. Letz. (1998). Using Matings for Pruning Connection Tableaux. In Proceedings of the 15th Conference on Automated Deduction (CADE-15),LNAI 1421, pages 381–396, Springer.
R. Letz. (1999). First-order Tableau Methods. In M. D’Agostino, D. Gabbay, R. Hähnle, J. Posegga, editors, Handbook of Tableau Methods,pages 125–196, Kluwer.
D. W. Loveland. (1968). Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15 (2): 236–251.
D. W. Loveland. (1978). Automated Theorem Proving: a Logical Basis. North-Holland.
M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, K. Mayr. (1997). SETHEO and ESETHEO. Journal of Automated Reasoning, 18: 237–246.
S.-J. Lee and D. Plaisted. (1992). Eliminating Duplication with the Hyper-Linking Strategy. Journal of Automated Reasoning, 9 (1): 25–42.
D. Prawitz. (1960). An Improved Proof Procedure. Theoria, 26: 102–139.
D. Prawitz. (1969). Advances and Problems in Mechanical Proof Procedures. Machine Intelligence, 4:59–71, Edinburgh U. Press.
R. M. Smullyan. (1968). First-Order Logic. Springer.
M. A. Stickel. (1988). A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4: 353–380.
A. Voronkov. (1998). Herbrand’s theorem, automated reasoning and semantic tableaux. In Proceedings of LICS-98.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Letz, R. (2000). Properties and Relations of Tableau and Connection Calculi. In: Hölldobler, S. (eds) Intellectics and Computational Logic. Applied Logic Series, vol 19. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9383-0_15
Download citation
DOI: https://doi.org/10.1007/978-94-015-9383-0_15
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5438-8
Online ISBN: 978-94-015-9383-0
eBook Packages: Springer Book Archive