Note III Independent explainer
The TPTP format and syntax, with examples
Provers from different groups can read the same problem file because of one shared plain-text format. Learn its handful of rules and you can read most of it.
What TPTP is
TPTP stands for Thousands of Problems for Theorem Provers. It is both a library of test problems and the language those problems are written in, maintained by Geoff Sutcliffe and collaborators. The library first appeared in the early 1990s, and its problems are used to compare provers fairly, including in the CASC competition.
TPTP syntax: an annotated formula
A TPTP file is a list of annotated formulas. Each one has the shape language(name, role, formula). The language is fof for first-order formulas, cnf for clauses, tff for typed first-order logic and thf for higher-order logic. Lines starting with a percent sign are comments.
The classic example looks like this: fof(humans_are_mortal, axiom, ![X]: (human(X) => mortal(X))). Then fof(socrates, axiom, human(socrates)). Then fof(goal, conjecture, mortal(socrates)).
TPTP language: the symbols to remember
Variables start with an uppercase letter and constants, functions and predicates start with a lowercase letter. The symbol ! with a bracketed variable means for all, and ? means there exists. Connectives are ~ for not, & for and, | for or, => for implies and <=> for if and only if. Every formula ends with a full stop.
In cnf statements there are no quantifiers: variables are implicitly universal, and a clause is written as a disjunction such as (~human(X) | mortal(X)).
Roles tell the prover what each formula is
The role axiom marks background knowledge, hypothesis is an assumption for this problem and conjecture is the statement to prove. When a prover negates the conjecture for refutation, the negated form carries the role negated_conjecture. Other roles, such as definition, lemma and type, appear in richer problems.
Includes and the status values
Large problems reuse axiom sets through an include directive, for example include('Axioms/SET001-0.ax'). This keeps a library of hundreds of problems consistent.
Provers report an outcome from the SZS ontology, printed as a comment line such as % SZS status Theorem for problem_name. Theorem means the conjecture follows from the axioms. Unsatisfiable is the same result for a problem with no conjecture. CounterSatisfiable means the conjecture does not follow. Timeout and GaveUp mean the prover stopped without an answer. When a proof is requested, a prover can print it in a matching format so a separate checker can verify it.