Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 1998: Theorem Proving in Higher Order Logics pp 245–261Cite as

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

  • Refereed Papers
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((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.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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.

    Article  MATH  MathSciNet  Google Scholar 

  2. Peter B. Andrews, 1973. letter to Roger Hindley dated January 22, 1973.

    Google Scholar 

  3. H. P. Barendregt. The Lambda Calculus. North Holland, 1984.

    Google Scholar 

  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. Christoph Benzmüller, 1997. LEO benchmarks http://www.ags.uni-sb.de/projects/deduktion/projects/hot/mizar/.

    Google Scholar 

  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. Maria Paola Bonacina and Jieh Hsiang. Parallelization of Deduction Strategies: An Analytical Study. Journal of Automated Reasoning, (13):1–33, 1994.

    Google Scholar 

  8. Christoph Benzmüller and Michael Kohlhase. Resolution for henkin models. SEKI-Report SR-97-10, UniversitÄt des Saarlandes, 1997.

    Google Scholar 

  9. Bernhard Beckert and Joachim Posegga. Lean, Tableau-based Deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  10. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

    Article  MATH  MathSciNet  Google Scholar 

  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. R. Engelmore and T. Morgan, editors. Blackboard Systems. Addison-Wesley, 1988.

    Google Scholar 

  13. Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer Verlag, 1990.

    Google Scholar 

  14. Claire Gardent, Michael Kohlhase, and Karsten Konrad. Higher-order coloured unification: a linguistic application. Submitted for publication, 1997.

    Google Scholar 

  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].

    Article  MATH  Google Scholar 

  16. Jean H. Gallier and Wayne Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 1(67):203–260, 1989.

    Article  MathSciNet  Google Scholar 

  17. Leon Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2):81–91, 1950.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. Michael Kohlhase. Higher-order tableaux. In Proceedings of the Tableau Workshop, pages 294–309, Koblenz, Germany, 1995.

    Google Scholar 

  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. 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. Dale Miller. Proofs in Higher-Order Logic. PhD thesis, Carnegie-Mellon University, 1983.

    Google Scholar 

  24. Programming Systems Lab Saarbrücken, 1998. The Oz Webpage: http://www.ps.uni-sb.de/oz/.

    Google Scholar 

  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. Z. Trybulec and H. Swieczkowska. Boolean properties of sets. Journal of Formalized Mathematics, 1, 1989.

    Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, UniversitÄt des Saarlandes, D-66141, Saarbrücken, Germany

    Karsten Konrad

Authors
  1. Karsten Konrad
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jim Grundy Malcolm Newey

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Konrad, K. (1998). Hot: A concurrent automated theorem prover based on higher-order tableaux. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055140

Download citation

  • DOI: https://doi.org/10.1007/BFb0055140

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64987-8

  • Online ISBN: 978-3-540-49801-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation