Extensional higher-order resolution

  • Christoph Benzmüller
  • Michael Kohlhase
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


In this paper we present an extensional higher-order resolution calculus that is complete relative to Henkin model semantics. The treatment of the extensionality principles — necessary for the completeness result — by specialized (goal-directed) inference rules is of practical applicability, as an implentation of the calculus in the LEO-System shows. Furthermore, we prove the long-standing conjecture, that it is sufficient to restrict the order of primitive substitutions to the order of input formulae.


Inference Rule Extensionality Principle Head Variable Empty Clause Extensionality Rule 
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. [ABI+96]
    Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321–353, 1996.MathSciNetCrossRefGoogle Scholar
  2. [And71]
    Peter B. Andrews. Resolution in type theory. Journal of Symbolic Logic, 36(3):414–432, 1971.zbMATHMathSciNetCrossRefGoogle Scholar
  3. [And72]
    Peter B. Andrews. General models descriptions and choice in type theory. Journal of Symbolic Logic, 37(2):385–394, 1972.zbMATHMathSciNetCrossRefGoogle Scholar
  4. [And86]
    Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.Google Scholar
  5. [And89]
    Peter B. Andrews. On Connections and Higher Order Logic. Journal of Automated Reasoning, 5:257–291, 1989.zbMATHMathSciNetCrossRefGoogle Scholar
  6. [Bar84]
    H. P. Barendregt. The Lambda Calculus. North Holland, 1984.Google Scholar
  7. [Ben97]
    Christoph Benzmüller. A calculus and a system architecture for extensional higher-order resolution. Research Report 97-198, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh,USA, June 1997.Google Scholar
  8. [BK97]
    Christoph Benzmüuller and Michael Kohlhase. Model existence for higher-order logic. SEKI-Report SR-97-09, UniversitÄt des Saarlandes, 1997.Google Scholar
  9. [BK98]
    Christoph Benzmüller and Michael Kohlhase. LEO, a higher-order theorem prover. to appear at CADE-15, 1998.Google Scholar
  10. [dB72]
    Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5):381–392, 1972.Google Scholar
  11. [Göd31]
    Kurt Gödel. über formal unentscheidbare SÄtze der Principia Mathematica und verwandter Systeme I. Monatshefte der Mathematischen Physik, 38:173–198, 1931.zbMATHCrossRefGoogle Scholar
  12. [Hen50]
    Leon Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2):81–91, 1950.zbMATHMathSciNetCrossRefGoogle Scholar
  13. [Hue73]
    Gérard P. Huet. A mechanization of type theory. In Donald E. Walker and Lewis Norton, editors, Proc. IJCAI'73, pages 139–146, 1973.Google Scholar
  14. [JP76]
    D. C. Jensen and T. Pietrzykowski. Mechanizing Ω-order type theory through unification. Theoretical Computer Science, 3:123–171, 1976.MathSciNetCrossRefGoogle Scholar
  15. [Koh94]
    Michael Kohlhase. A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle. PhD thesis, UniversitÄt des Saarlandes, 1994.Google Scholar
  16. [Koh95]
    Michael Kohlhase. Higher-Order Tableaux. In P. Baumgartner, et al. eds, TABLEAUX'95, volume 918 of LNAI, pages 294–309, 1995.Google Scholar
  17. [Mil83]
    Dale Miller. Proofs in Higher-Order Logic. PhD thesis, Carnegie-Mellon University, 1983.Google Scholar
  18. [Smu63]
    Raymond M. Smullyan. A unifying principle for quantification theory. Proc. Nat. Acad Sciences, 49:828–832, 1963.zbMATHMathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Christoph Benzmüller
    • 1
  • Michael Kohlhase
    • 1
  1. 1.Fachbereich InformatikUniversitÄt des SaarlandesGermany

Personalised recommendations