THF0 - The core of the TPTP language for higher-order logic

Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Scopus citations

Abstract

One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This paper introduces the core of the TPTP language for higher-order logic - THF0, based on Church's simple type theory. THF0 is a syntactically conservative extension of the untyped first-order TPTP language.

Original languageEnglish (US)
Title of host publicationAutomated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings
Pages491-506
Number of pages16
DOIs
StatePublished - Oct 7 2008
Event4th International Joint Conference on Automated Reasoning, IJCAR 2008 - Sydney, NSW, Australia
Duration: Aug 12 2008Aug 15 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5195 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Joint Conference on Automated Reasoning, IJCAR 2008
CountryAustralia
CitySydney, NSW
Period8/12/088/15/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'THF0 - The core of the TPTP language for higher-order logic'. Together they form a unique fingerprint.

  • Cite this

    Benzmüller, C., Rabe, F., & Sutcliffe, G. (2008). THF0 - The core of the TPTP language for higher-order logic. In Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings (pp. 491-506). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5195 LNAI). https://doi.org/10.1007/978-3-540-71070-7_41