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 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 491-506 |
| Number of pages | 16 |
| Volume | 5195 LNAI |
| DOIs | |
| State | Published - 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) | 03029743 |
| ISSN (Electronic) | 16113349 |
Other
| Other | 4th International Joint Conference on Automated Reasoning, IJCAR 2008 |
|---|---|
| Country | Australia |
| City | Sydney, NSW |
| Period | 8/12/08 → 8/15/08 |
Fingerprint
ASJC Scopus subject areas
- Computer Science(all)
- Theoretical Computer Science
Cite this
THF0 - The core of the TPTP language for higher-order logic. / Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoffrey.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5195 LNAI 2008. p. 491-506 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5195 LNAI).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - THF0 - The core of the TPTP language for higher-order logic
AU - Benzmüller, Christoph
AU - Rabe, Florian
AU - Sutcliffe, Geoffrey
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=53049095806&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=53049095806&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-71070-7_41
DO - 10.1007/978-3-540-71070-7_41
M3 - Conference contribution
AN - SCOPUS:53049095806
SN - 3540710698
SN - 9783540710691
VL - 5195 LNAI
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 491
EP - 506
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -