Abstract
In a previous paper we proposed an approach to exploit literal equivalences in connection tableau based calculi. There we showed that making equivalences explicit offers new possibilities for search space reduction by applying literal demodulation for simplification and by strengthening the well-known regularity refinement. In this paper we generalize this approach to handle conditional equivalences. The generalization is mainly motivated by the circumstance that non-conditional equivalences, if not present at the beginning of a deduction, are much harder to generate than conditional ones.
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.
Reference
O. L. Astrachan and M. E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. In Proc. of CADE, vol. 607 of LNAI, pages 224–238. Springer, 1992.
P. Baumgartner, N. Eisinger, and U. Furbach. Intellectics and Computational Logic, chapter A Confluent Connection Calculus, pages 3–26. Kluwer, 2000.
W. Bibel. Deduction: Automated Logic. Academic Press, London, 1993.
W. Bibel, S. Brüning, U. Egly, and T. Rath. Komet. In Proc. of CADE, number 814 in LNAI, pages 783–787. Springer, 1994. System description.
G. Brewka, editor. Principles of Knowledge Representation. CSLI Publications, 1996.
_ S. Brüning. Exploiting Equivalences in Connection Calculi. Journal of the Interest Group in Pure and Applied Logics (IGPL), 3(6):857–886, 1995.
_ S. Brüning and T. Schaub. Prolog technology for default reasoning: Proof theory and compilation techniques. Artificial Intelligence, 106(1):1–75, 1998.
_ S. Brüning and T. Schaub. Avoiding non-ground variables. In Proc. of the Fifth European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, vol. 1638 of LNAI, pages 92–103. Springer, 1999.
_ S. Ceri, G. Gottlob, and L. Tanca. Logic Programming and Databases. Springer, 1990.
M. Fuchs. System Description: Similarity-Based Lemma Generation for Model Elimination. In Proc. of CADE, vol. 1421 of LNAI, pages 33–37. Springer, 1998.
S.-J. Lee and D. A. Plaisted. Reasoning with Predicate Replacement. In Proc. of ISMIS, 1990.
R. Letz. First-Order Calculi and Proof Procedures for Automated Deduction. PhD thesis, TH Darmstadt, 1993.
R. Letz, K. Mayr, and Ch. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13(3):297–338, 1994.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO-A High-Performance Theorem Prover for First-Order Logic. Journal of Automated Reasoning, 8:183–212, 1992.
A. F. McMichael. An Automated Reasoner For Equivalences, Applied To Set Theory. In Proc. of CADE, pages 308–321, 1990.
R. Socher-Ambrosius. A Resolution Calculus Extended by Equivalence. In Proc. of the German Workshop on Artificial Intelligence, pages 102–106. Springer, 1989.
L. Wos. Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brüning, S. (2001). Exploiting Conditional Equivalences in Connection Calculi. In: Baader, F., Brewka, G., Eiter, T. (eds) KI 2001: Advances in Artificial Intelligence. KI 2001. Lecture Notes in Computer Science(), vol 2174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45422-5_10
Download citation
DOI: https://doi.org/10.1007/3-540-45422-5_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42612-7
Online ISBN: 978-3-540-45422-9
eBook Packages: Springer Book Archive