System description: Leo — A higher-order theorem prover

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


Theorem Prover Extensionality Principle Automate Deduction Empty Clause Primitive Substitution 
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.
    P. B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321–353, 1996.MathSciNetCrossRefGoogle Scholar
  2. 2.
    C. 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
  3. 3.
    C. Benzmüller and M. Kohlhase. Extensional Higher-Order Resolution. Proc. CADE-15, this volume, 1998.Google Scholar
  4. 4.
    P. Graf. Term Indexing. Number 1053 in LNCS. Springer Verlag, 1996.Google Scholar
  5. 5.
    X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann. Keim: A toolkit for automated deduction. In Alan Bundy, editor, Proc. CADE-13, number 814 in LNAI, pages 807–810, 1994. Springer Verlag.Google Scholar
  6. 6.
    G. P. Huet. An unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.zbMATHMathSciNetCrossRefGoogle Scholar
  7. 7.
    L. Klein. Indexing für Terme höherer Stufe. Master's thesis, FB Informatik, UniversitÄt des Saarlandes, 1997.Google Scholar
  8. 8.
    M. Kohlhase. A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle. PhD thesis, UniversitÄt des Saarlandes, 1994.Google Scholar
  9. 9.
    D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321–358, 1992.zbMATHMathSciNetCrossRefGoogle Scholar
  10. 10.
    Z. Trybulec and H. Swieczkowska. Boolean properties of sets. Journal of Formalized Mathematics, 1, 1989.Google 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