Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure

Authors

  • Geoff Sutcliffe University of Miami
  • Christoph Benzmueller Articulate Software

DOI:

https://doi.org/10.6092/issn.1972-5787/1710

Abstract

The Thousands of Problems for Theorem Provers (TPTP) problem library is the basis of a well known and well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The extension of the TPTP from first-order form (FOF) logic to typed higher-order form (THF) logic has provided a basis for new development and application of ATP systems for higher-order logic. Key developments have been the specification of the THF language, the addition of higher-order problems to the TPTP, the development of the TPTP THF infrastructure, several ATP systems for higher-order logic, and the use of higher-order ATP in a range of domains. This paper describes these developments.

Downloads

Published

2010-04-14

How to Cite

Sutcliffe, G., & Benzmueller, C. (2010). Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning, 3(1), 1–27. https://doi.org/10.6092/issn.1972-5787/1710

Issue

Section

Articles