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 language | English (US) |
|---|---|
| Title of host publication | Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings |
| Pages | 491-506 |
| Number of pages | 16 |
| DOIs | |
| State | Published - Oct 7 2008 |
| Event | 4th International Joint Conference on Automated Reasoning, IJCAR 2008 - Sydney, NSW, Australia Duration: Aug 12 2008 → Aug 15 2008 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 5195 LNAI |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 4th International Joint Conference on Automated Reasoning, IJCAR 2008 |
|---|---|
| Country | Australia |
| City | Sydney, NSW |
| Period | 8/12/08 → 8/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