TY - GEN
T1 - THF0 - The core of the TPTP language for higher-order logic
AU - Benzmüller, Christoph
AU - Rabe, Florian
AU - Sutcliffe, Geoff
PY - 2008/10/7
Y1 - 2008/10/7
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
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 491
EP - 506
BT - Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings
T2 - 4th International Joint Conference on Automated Reasoning, IJCAR 2008
Y2 - 12 August 2008 through 15 August 2008
ER -