The TPTP contains problems in first-order (FOF) and clause normal form (CNF), monomorphic and polymorphic typed first-order form (TFF, which includes the extended first-order form (TXF)), monomorphic and polymorphic typed higher-order form (THF), dependently typed monomorphic and polymorphic typed higher-order form (DHF), and non-classical typed first-order (NXF) and higher-order (NHF) forms. Interpreted arithmetic types and symbols are supported in all the typed logics.
TPTP problems and TSTP solutions are built from annotated formulae of the form:
language(name,role,formula,source,useful_info).
The languages supported are cnf, fof, tff, and thf.
The role gives the user semantics of the formula, one of axiom, hypothesis, definition, assumption, lemma, theorem, corollary, conjecture, negated_conjecture, plain, type, interpretation, logic, and unknown.
The axiom-like formulae are those with the roles axiom, hypothesis, definition, assumption, lemma, theorem, and corollary. They are accepted, without proof, as a basis for proving conjectures in THF, TFF, and FOF problems. In CNF problems the axiom-like formulae are accepted as part of the set whose satisfiability has to be established. There is no guarantee that the axiom-like formulae of a problem are consistent.
hypothesiss are assumed to be true for a particular problem.
definitions are used to define symbols.
assumptions must be discharged before a derivation is complete.
lemmas and theorems have been proven from the other axiom-like formulae, and are thus redundant wrt those axiom-like formulae. theorem is used also as the role of proven conjectures, in output. A problem containing a lemma or theorem that is not redundant wrt the other axiom-like formulae is ill-formed. theorems are more important than lemmas from the user perspective.
corollarys have been proven from the axioms and a theorem, and are thus redundant wrt the other axiom-like and theorem formulae. A problem containing a corollary that is not redundant wrt the other axiom-like formulae and theorem formulae is ill-formed.
conjectures occur in THF, TFF, and FOF problems, and are to all be proven from the axiom-like formulae. A problem is solved only when all conjectures are proven. (TPTP problems never contain more than one conjecture, and the creation of problems with more than one conjecture is currently deprecated, because contemporary ATP systems commonly treat them as a disjunction, and will prove only one of them.)
negated_conjectures are formed from negation of a conjecture, typically in FOF to CNF conversion.
plain formulae have no special user semantics, and are typically used in derivation output.
type formulae define the types of symbols globally.
interpretation formulae are used for writing interpretations, typically models of satisfiable sets of formulae, in particular the axioms and negated_conjecture of a non-theorem.
logic formulae are used for defining the logic in non-classical logics.
unknowns have unknown role, and this is an error situation.
The useful_info field of an annotated formula is optional, and if it is not used then the source field becomes optional. The source field is used to record where the annotated formula came from, and is most commonly a file() record, an introduced() record, or an inference() record. A file() record stores the name of the file from which the annotated formula was read, and optionally the name of the annotated formula as it occurs in that file - this might be different from the name of the annotated formula itself, e.g., if an ATP systems reads an annotated formula, renames it, and then prints it out. An introduced() record may occur in a derivation to record the introduction of a formula by the ATP system, e.g., the introduction of a tautology. An inference() record stores information about an inferred formula. The useful_info field of an annotated formula is a list of arbitrary useful information formatted as Prolog terms, as required for user applications.
Logical Formulae
In a formula, terms and atoms follow Prolog conventions - functions and predicates start with a lowercase letter or are 'single quoted', and variables start with an uppercase letter. Symbols may be overloaded with different arity signatures, and are treated as different symbols (but it’s deprecated, because most ATP systems and tools don’t know this). The language also supports interpreted symbols that are either defined symbols that start with a $, or are composed of non-alphabetic characters. Defined symbols come in two varieties: TPTP defined predicates and functors, whose interpretation is specified by the TPTP language, and system defined predicates and functors, whose interpretation is ATP system specific. The defined predicates and functors recognized so far are listed below.
The logical connectives in the classical TPTP languages are !>, ?*, @+, @-, ^, !, ?, @, ~, |, &, =>, <=, <=>, and <~>, for Pi, Sigma, choice (indefinite description), definite description, lambda abstraction, universal quantification, existential quantification, function application, negation, disjunction, conjunction, implication, reverse implication, equivalence, and non-equivalence (XOR). Equality and inequality are expressed as the infix predicates = and !=. Quantified formulae are written in the form
Quantifier [Variables] : Formula
In all except the CNF language, every variable in a formula must be bound by a preceding quantification with adequate scope. Negation has higher precedence than quantification, which in turn has higher precedence than the binary connectives. No precedence is specified between the binary connectives; brackets are used to ensure the correct association. See the section on non-classical logics for information about the non-classical connectives.
Types
The typed languages (TFF, TXF, THF, DHF, NXF, NHF) support types and type declarations (all the details are in the section on the type system). Symbols are declared before their use, with type signatures that specify the types of their arguments and result. Two TPTP defined types are available, $i for individuals, and $o for booleans. User defined types can be introduced as being of the "type" $tType. In the first-order languages, a signature of the form (t1 * ... * tn) > r is the type of an n-ary symbol, where the i-th argument is of type ti and the result type is r. If r is $o then the symbol is a predicate. Variables are given their type by a :type suffix. Equality is ad hoc polymorphic over all types. A useful feature of TFF is default typing for symbols that are not explicitly declared: predicates default to ($i,...,$i) > $o, and functions default to ($i,...,$i) > $i. This allows TFF to effectively degenerate to untyped FOF. The typed extended first-order form (TXF) augments TFF with FOOL constructs: formulae of type $o as terms; variables of type $o as formulae; tuples; $ite() (if-then-else) expressions; and $let (let-defn-in) expressions. The typed higher-order form (THF) includes type declarations in curried form, lambda-terms with a binder symbol ^ for lambda, explicit application with @, and quantification over variables of any type. A curried type signature has the form t1 > ... > tn > r. THF does not admit default typing - all symbol types must be declared before use. The polymorphic languages use a !> to quantify over types, producing types signatures of the form !> [T:$tType] : t1 > ... > tn > r. where any ti or r can be the type T. When using polymorphic symbols the concrete type(s) must be provided as the first arguments in the use.
Defined Symbols
The defined symbols are:
The truth constants $true and $false.
Integer/rational/real numbers such as 27, 43/92, -99.66.
$distinct, FIX THIS whose arguments are hence known to be unequal from each other (but not necessarily unequal to any other constants). In the typed languages $distinct is ad hoc polymorphic with all arguments having the same type.
"distinct object"s, written in double quotes. All "distinct object"s are unequal to all "different distinct object"s (but not necessarily unequal to any other constants), e.g., "Apple" != "Microsoft". In typed contexts FIX THIS "distinct object"s are of type $i (and as a result, are unequal to all numbers because their interpretation domains are disjoint in the TPTP type systems).
Numbers (numeric constants). These are used in only the typed languages (numbers require a type system in order to make sense). Numbers are interpreted as themselves (as domain elements). All different numbers are unequal, e.g., 1 != 2 (but not necessarily unequal to any other constants of the same type). All numbers are also unequal to terms of type $i (because their interpretation domains are disjoint in the TPTP type systems).
Conditional and Let Expressions
The THF and TXF languages have conditional and let expressions.
Conditional expressions have $ite as the functor. The expressions are parametric polymorphic, taking a boolean expression as the first argument, then two expressions of any one type as the second and third arguments, as the true and false return values respectively, i.e., the return type is the same as that of the second and third arguments.
Let expressions have $let as the functor. The expressions provide the types of defined symbols, definitions for the symbols, and a formula/term in which the definitions are applied. Each type declaration is the same as a type declaration in an annotated formula with the type role, and multiple type declarations are given in []ed tuples of declarations. Each definition defines the expansion of one of the declared symbols, and multiple definitions are given in []ed tuples of definitions. If variables are used in the lefthand side of a definition, their values are supplied in the defined symbol's use. Such variables do not need to be declared (they are implicitly declared to be of the type defined by the symbol declaration), but must be top-level arguments of the defined symbol and be pairwise distinct. In the polymorphic case, type declarations may include type variables introduced in an enclosing scope, such as:
%----The constant function using A from 'outside' and B from 'inside'.
%----B is required in the use of const, but not A.
tff(let_polymorphic_both_types, axiom,
!>[A: $tType] :
$let(
const : !>[B: $tType] : (A * B) > A,
const(B, X, Y) := X),
... ).
No extra type arguments are needed when using such $let-defined symbols.