Advertisement

Hot: A concurrent automated theorem prover based on higher-order tableaux

  • Karsten Konrad
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

Abstract

Hot is an automated higher-order theorem prover based on HTE, an extensional higher-order tableaux calculus. The first part of this paper introduces an improved variant of the calculus which closely corresponds to the proof procedure implemented in Hot. The second part discusses Hot's design that can be characterized as a concurrent blackboard architecture. We show the usefulness of the implementation by including benchmark results for over one hundred solved problems from logic and set theory.

Keywords

Theorem Prover Proof Procedure Proof Search Unification Problem 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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.zbMATHMathSciNetCrossRefGoogle Scholar
  2. 2.
    Peter B. Andrews, 1973. letter to Roger Hindley dated January 22, 1973.Google Scholar
  3. 3.
    H. P. Barendregt. The Lambda Calculus. North Holland, 1984.Google Scholar
  4. 4.
    C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. Ω Mega: Towards a mathematical assistant. In William McCune, editor, Proceedings of the 14th Conference on Automated Deduction, number 1249 in LNAI, pages 252–255, Townsville, Australia, 1997. Springer Verlag.Google Scholar
  5. 5.
    Christoph Benzmüller, 1997. LEO benchmarks http://www.ags.uni-sb.de/projects/deduktion/projects/hot/mizar/.Google Scholar
  6. 6.
    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
  7. 7.
    Maria Paola Bonacina and Jieh Hsiang. Parallelization of Deduction Strategies: An Analytical Study. Journal of Automated Reasoning, (13):1–33, 1994.Google Scholar
  8. 8.
    Christoph Benzmüller and Michael Kohlhase. Resolution for henkin models. SEKI-Report SR-97-10, UniversitÄt des Saarlandes, 1997.Google Scholar
  9. 9.
    Bernhard Beckert and Joachim Posegga. Lean, Tableau-based Deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.zbMATHMathSciNetCrossRefGoogle Scholar
  10. 10.
    Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.zbMATHMathSciNetCrossRefGoogle Scholar
  11. 11.
    Ingo Dahn, 1997. Statistics for Problems from the Mizar Library. http://www-irm.mathematik.hu-berlin.de/~ilf/miz2atp/mizstat.html.Google Scholar
  12. 12.
    R. Engelmore and T. Morgan, editors. Blackboard Systems. Addison-Wesley, 1988.Google Scholar
  13. 13.
    Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer Verlag, 1990.Google Scholar
  14. 14.
    Claire Gardent, Michael Kohlhase, and Karsten Konrad. Higher-order coloured unification: a linguistic application. Submitted for publication, 1997.Google Scholar
  15. 15.
    Kurt Gödel. über formal unentscheidbare SÄtze der Principia Mathematica und verwandter Systeme I. Monatshefte der Mathematischen Physik, 38:173–198, 1931. English Version in [27].zbMATHCrossRefGoogle Scholar
  16. 16.
    Jean H. Gallier and Wayne Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 1(67):203–260, 1989.MathSciNetCrossRefGoogle Scholar
  17. 17.
    Leon Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2):81–91, 1950.zbMATHMathSciNetCrossRefGoogle Scholar
  18. 18.
    Dieter Hutter and Michael Kohlhase. A coloured version of the λ-calculus. SEKI-Report SR-95-05, UniversitÄt des Saarlandes, 1995.Google Scholar
  19. 19.
    Michael Kohlhase and Karsten Konrad. Higher-order automated theorem proving for natural language semantics. Seki Report SR-98-04, Fachbereich Informatik, UniversitÄt Saarbrücken, 1998.Google Scholar
  20. 20.
    Michael Kohlhase. Higher-order tableaux. In Proceedings of the Tableau Workshop, pages 294–309, Koblenz, Germany, 1995.Google Scholar
  21. 21.
    Michael Kohlhase. Higher-order automated theorem proving. In Wolfgang Bibel and Peter Schmitt, editors, Automated Deduction — A Basis for Applications, volume 2. Kluwer, 1998. forthcoming.Google Scholar
  22. 22.
    Luiz V. Leao and Sarosh N. Talukdar. COPS: A System for Constructing Multiple Blackboards. In Alan H. Bond and Les Gasser, editors, Readings in Distributed Artificial Intelligence, page 547ff. Morgan Kaufmann, 1988.Google Scholar
  23. 23.
    Dale Miller. Proofs in Higher-Order Logic. PhD thesis, Carnegie-Mellon University, 1983.Google Scholar
  24. 24.
    Programming Systems Lab Saarbrücken, 1998. The Oz Webpage: http://www.ps.uni-sb.de/oz/.Google Scholar
  25. 25.
    Gert Smolka. The oz programming model. In Jan van Leeuwen, editor, Computer Science Today, volume 1000 of LNCS, pages 324–343. Springer Verlag, 1995.Google Scholar
  26. 26.
    Z. Trybulec and H. Swieczkowska. Boolean properties of sets. Journal of Formalized Mathematics, 1, 1989.Google Scholar
  27. 27.
    Jean van Heijenoort, editor. From Frege to Gödel A Source Book in Mathematical Logic, 1879–1931. Source Books in the History of the Sciences. Harvard University Press, 1967.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Karsten Konrad
    • 1
  1. 1.Fachbereich InformatikUniversitÄt des SaarlandesSaarbrückenGermany

Personalised recommendations