Abstract
We propose several methods for writing efficient subsumption procedures for non-unit clauses, tested in practice as parts incorporated into the Gandalf family of theorem provers. Versions of Gandalf exist for classical logic, first order intuitionistic logic and type theory.
Preview
Unable to display preview. Download preview PDF.
References
C. Fermüller, A. Leitsch, T. Tammet, N. Zamov. Resolution methods for decision problems. Lecture Notes in Artificial Intelligence vol. 679, Springer Verlag, 1993.
P. Graf. Term Indexing. Lecture Notes in Computer Science. 1053, Springer Verlag, 1996.
G. Gottlob, A. Leitsch. On the efficiency of subsumption algorithms, Journa of ACM 32(2):280–295, April 1985.
L. Magnusson, B. Nordström. The ALF proof editor and its proof engine. In Types for Proofs and Programs, pages 213–237, Lecture Notes in Computer Science vol. 806, Springer Verlag, 1994.
G. Mints. Resolution Calculus for The First Order Linear Logic. Journal of Logic, Language and Information, 2, 58–93 (1993).
W. McCune. OTTER 3.0 Reference Manual and Users Guide. Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, January 1994.
W. McCune. Experiments with discrimination tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147–167, 1992.
T. Tammet. Completeness of Resolution for Definite Answers. Journal of Logic and Computation, (1995), vol 4 nr 5, 449–471.
T. Tammet. A Resolution Theorem Prover for Intuitionistic Logic. In CADE-13, pages 2–16, Lecture Notes in Computer Science vol. 1104, Springer Verlag, 1996.
T. Tammet, J. Smith. Optimised Encodings of Fragments of Type Theory in First Order Logic. In Types for Proofs and Programs, pages 265–287, Lecture Notes in Computer Science vol. 1158, Springer Verlag,1996.
T. Tammet. Gandalf. Journal of Automated Reasoning, 18(2): 199–204, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tammet, T. (1998). Towards efficient subsumption. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054276
Download citation
DOI: https://doi.org/10.1007/BFb0054276
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64675-4
Online ISBN: 978-3-540-69110-5
eBook Packages: Springer Book Archive