The TPTP

Typed Higher-order Form

by Christoph Benzmüller, Florian Rabe, Allen Van Gelder, Geoff Sutcliffe, Chad Brown

This merges the current first-order TPTP syntax with Allen van Gelder's development, and the Simple Type System for FOF.

Problems using the THF0 syntax will be part of the next TPTP release, TPTP v4.0.0.
The THF0 problems are already available in the THF beta release, TPTP v3.7.0.

The proposal breaks the "typed higher-order form" (THF) syntax into three levels, and a separate first-order form syntactic sugar:

The THF core (THF0) provides the common core of Church's typed lambda calculus.
The full THF language (THF) adds tuples, unions, binary types, type statements, etc., as formulae, and unitary formulae as types.
The extended language (THFX) adds definitions, letrecs, sequents, etc.
The first-order form extension (THFF) add first-order style formulae and terms.

All of the variants include the full TPTP annotated formulae structure, so the BNF looks like quite a lot. However, if you focus on the THF formula part, it is easy to see that it retains the elegance and simplicity of the lambda caclulus. Here are ...

The THF0 syntax BNF, and the THF0Parser parser binary for THF0, which takes formulae on stdin and outputs the parse tree.
The full THF syntax BNF, and the THFParser parser binary for THF, which takes formulae on stdin and outputs the parse tree.
The THF syntax levels BNF with THF, THFX, and THFF commented out to show the extensions.
Some examples.

The parsers are available online through the SystemB4TPTP interface.

Here are some old proposals that influenced the development of this final product.