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. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Benzmüller, C., Rabe, F., & Sutcliffe, G. (2008). THF0 - The core of the TPTP language for higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 491–506). https://doi.org/10.1007/978-3-540-71070-7_41
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
