The TPTP Language

The TPTP language supports a hierarchy of logics from propositional up to dependently types higher-order logic, and non-classical logics. Each logic uses a variant of the TPTP language, to express features of formulae in the logic, thus leading to a family of TPTP languages. All the languages are expressed in a Prolog-based syntax, with each logical formula wrapped in an "annotated formula" record, with one of four principle symbols. From the TFF level upwards, all the languages use the TPTP type system, with increasingly more powerful constructs, with monomorphic (ending in '0') and polymorphic (ending in '1') variants. All the typed languages include arithmetic constructs.