Towards efficient subsumption

  • Tanel Tammet
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


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.


Classical Logic Type Theory Intuitionistic Logic Unit Clause Proof Search 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    C. Fermüller, A. Leitsch, T. Tammet, N. Zamov. Resolution methods for decision problems. Lecture Notes in Artificial Intelligence vol. 679, Springer Verlag, 1993.Google Scholar
  2. 2.
    P. Graf. Term Indexing. Lecture Notes in Computer Science. 1053, Springer Verlag, 1996.Google Scholar
  3. 3.
    G. Gottlob, A. Leitsch. On the efficiency of subsumption algorithms, Journa of ACM 32(2):280–295, April 1985.CrossRefMathSciNetGoogle Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    G. Mints. Resolution Calculus for The First Order Linear Logic. Journal of Logic, Language and Information, 2, 58–93 (1993).CrossRefMathSciNetGoogle Scholar
  6. 6.
    W. McCune. OTTER 3.0 Reference Manual and Users Guide. Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, January 1994.Google Scholar
  7. 7.
    W. McCune. Experiments with discrimination tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147–167, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    T. Tammet. Completeness of Resolution for Definite Answers. Journal of Logic and Computation, (1995), vol 4 nr 5, 449–471.zbMATHMathSciNetGoogle Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    T. Tammet. Gandalf. Journal of Automated Reasoning, 18(2): 199–204, 1997.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Tanel Tammet
    • 1
  1. 1.Department of Computing ScienceUniversity of GöteborgGöteborgSweden

Personalised recommendations