THF0 - The Core of the TPTP Language for Higher-Order Logic

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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe
• Keywords: Automated Reasoning, CADE 2008, First-order Tptp Language, Simple Type Theory, Theorem Provers