Inside the TPTP

Scope.
The TPTP contains problems in classical and non-classical logic, with an interpreted equality symbol. Release v9.0.0 of the TPTP contains: The TPTP documents OverallSynopsis, THFSynopsis, TFFSynopsis, FOFSynopsis, and CNFSynopsis provide some overall statistics about the TPTP.

The problems in the TPTP are syntactically diverse, as is indicated by the ranges of the values in the tables. The problems in the TPTP are also semantically diverse, as is indicated by the range of domains that are covered. The problems are grouped into domains, covering topics in the fields of logic, mathematics, computer science, engineering, social sciences, arts and humanities, and others.

Sources
The problems have been collected from various sources. Early sources were existing electronic problem collections and the ATP literature. Other sources include logic programming, mathematics, puzzles, and correspondence with ATP researchers. Many people and organizations have contributed towards the TPTP: the foundations of the TPTP were laid with David Plaisted's SPRFN collection; many problems were taken from Argonne National Laboratory's ATP problem library (special thanks to Bill McCune here); Art Quaife provided several hundred problems in set theory and algebra; the Journal of Automated Reasoning, CADE Proceedings, and Association for Automated Reasoning Newsletters have provided a wealth of material; many problems have been provided by ATP users and system developers (see the Acknowledgements).

Releases
The TPTP is managed in the manner of a software product, in the sense that fixed releases are made. Each release of the TPTP is identified by a release number, in the form vVersion.Edition.Patch level. The Version number enumerates major new releases of the TPTP, in which important new features have been added. The Edition number is incremented each time new problems are added to the current version. The Patch level is incremented each time errors, found in the current edition, are corrected. All non-trivial changes are recorded in a history file, as well as in the file for an affected problem.

The Domain Structure

This section provides the structure according to which the problems are grouped into domains. Some information about the domains is also given.

An attempt has been made to classify the totality of the TPTP problems in a systematic and natural way. The resulting domain scheme reflects the natural hierarchy of scientific domains, as presented in standard subject classification literature. The current classification is based mainly on the Dewey Decimal Classification (DDC) [CB+89] and the Mathematics Subject Classification (MSC) [MSC92] used for the Mathematical Reviews by the American Mathematical Society. Seven fields are defined: logic, mathematics, computer science, engineering, social sciences, arts and humanities, and other. Each field contains further subdivisions, called domains. Each domain is identified by a three-letter mnemonic. These mnemonics are also part of the TPTP problem naming scheme. The TPTP domains constitute the basic units of the classification. The full classification scheme is shown in Figure  The Domain Structure of the TPTP, and the numbers of abstract problems, problems, and generic problems in each domain are shown in the TPTP document OverallSynopsis

Logic Combinatory logic COL
Logic calculi LCL
Henkin models HEN
Mathematics Set theory SET, SEU, and SEV
Graph theory GRA
Algebra Relation algebra REL
MV Algebras MVA
Boolean algebra BOO
Robbins algebra ROB
Left distributive LDA
Lattices LAT
Quantales QUA
Kleene algebra KLE
Groups GRP
Rings RNG
Fields FLD
Homological algebra HAL
Real Algebra RAL
General algebra ALG
Arithmetic ARI
Number theory NUM and NUN
Topology TOP
Analysis ANA
Geometry GEO
Category theory CAT
Computer science Computing theory COM
Knowledge representation KRS
Natural Language Processing NLP
Planning PLA
Agents AGT
Commonsense Reasoning CSR
Semantic Web SWB
Interactive Theorem Proving ITP
Data Structures DAT
Software creation SWC
Software verification SWV and SWW and SWX
Science and Engineering Biology BIO
Hardware creation HWC
Hardware verification HWV
Medicine MED
Processes PRO
Products PRD
Time TIM
Social sciences Social Choice Theory SCT
Management MGT
Geography GEG
Arts and Humanities Philosophy PHI
Other Syntactic SYN and SYO and SYP
Puzzles PUZ
Miscellaneous MSC
The Domain Structure of the TPTP.

A brief description of the domains, with a non-ATP reference for a general introduction and a generic ATP reference, is given below. For each domain, appropriate DDC and MSC numbers are also given if available:

Problem Versions and Standard Axiomatizations

There are often many ways to formulate a problem for presentation to an ATP system. Thus, in the TPTP, there are often alternative presentations of a problem. The alternative presentations are called versions of the underlying abstract problem. As the problem versions are the objects that ATP systems must deal with, they are referred to simply as problems, and the abstract problems are referred to explicitly as such. Each problem is stored in a separate physical file. In the TPTP the most coarse grain differentiation between problem versions is whether the problem is presented in THF (with the subdivisions TH0 for monomorphic logic and TH1 for polymorphic logic), TFF (with the subdivisions TXF for extended logic (with the subdivisions TX0 for monomorphic logic and TX1 for polymorphic logic), TF0 for monomorphic logic, and TF1 for polymorphic logic), FOF, or CNF. Within a given presentation, the primary reason for different versions of an abstract problem is the use of different axiomatizations. This issue is discussed below. A secondary reason is different formulations of the problem to be solved, e.g., different clausal forms of a FOF problem.

Different Axiomatizations
Commonly, many different axiomatizations of a theory exist. By using different axiomatizations of a particular theory, different versions of a problem can be formed.

In the TPTP an axiomatization is standard if it is a complete axiomatization of an established theory, no lemmas have been added, and it is not designed specifically to be suited or ill-suited to any ATP system, calculus, or control strategy. A problem version is standard if it uses a standard axiomatization. (Note: A standard axiomatization might be redundant, because some axioms are dependent on others. In general, it is not known whether or not an axiomatization is minimal, and thus the possibility of redundancy in standard axiomatizations must be tolerated.) In the TPTP, standard axiomatizations are kept in separate axiom files, and are included in problems as appropriate. Sets of specialization axioms might be used to extend or constrain an axiomatization. Specialization axioms are also kept in separate axiom files.

Within the ATP community, some problems have been created with non-standard axiomatizations. A non-standard axiomatization can be formed by modifying a standard axiomatization: the standard axiomatization can be reduced (i.e., axioms are removed) and the result is an incomplete axiomatization, or it can be augmented (i.e., lemmas are added) and the result is a redundant axiomatization. Incomplete and redundant axiomatizations are typically used to find a proof of a conjecture (based on the axiomatization) using a particular ATP system. An axiomatization can also be non-standard because it is biased, i.e., designed specifically to be suited or ill-suited to some ATP system, calculus, or control strategy. A problem version is incomplete, redundant, or biased if its axiomatization is. Finally, an axiomatization can be non-standard because it does not capture any established theory, i.e., a standard axiomatization does not exist, but the axioms are not biased. A problem version with such an axiomatization is especial. Typically, the axioms in an especial problem are specific to that problem, and are not used in any other problem.

In any 'real' application of an ATP system, a standard or especial problem version would typically be used, at least initially. The use of standard axiomatizations is particularly desirable.

Equality Axiomatization
In the TPTP equality is represented in infix using = and != for equality and inequality. An inequality has the same meaning as a negated equality. If equality is present in a problem, axioms of equality are not provided; it is assumed that equality reasoning is builtin to every ATP system. If equality axioms are required by an ATP system they can be added using the TPTP2X or TPTP4X utility. If any axioms are added when the problems are submitted to an ATP system, then the addition must be explicitly noted in reported results/

Problem Generators

Some abstract problems have a generic nature, and particular instances of the abstract problem are formed according to some size parameter(s). An example of a generic problem is the N-queens problem: place N queens on a N by N chess board such that no queen attacks another. The formulae for any size of this problem can be generated automatically, for any size of N >= 2. Note that the problem status might depend on the problem size.

Up to TPTP v1.1.3, the TPTP contained problem files for particular sizes of generic problems. This, however, was undesirable. Firstly, only a finite number of different problem sizes could be included, and therefore a desired size might have been missing. Secondly, even a small number of different problem sizes for each generic problem could consume a considerable amount of disk space. To overcome these problems, the TPTP contains generator files. Generator files are used to generate instances of generic problems, according to user supplied size parameters. The generators are used in conjunction with the tptp2X utility.

For convenience, the TPTP still contains, where they exist, interesting size instances of each generic problem. The TPTP sizes were chosen to be non-trivial, The statistics in the TPTP documents take into account these instances of generic problems.

Problem and Axiomatization Naming

Providing unambiguous names for all problems is necessary in a problem library. A naming scheme has been developed for the TPTP, to provide unique, stable names for abstract problems, problems, axiomatizations, and generators. Files are assigned names according to the schemes depicted in Tables Problem Naming and Axiom Naming. The DDDNNN combination provides an unambiguous name for an abstract problem or axiomatization. The DDDNNNFV[.SSS] combination provides an unambiguous name for a problem or generator, and the DDDNNNFE combination provides an unambiguous name for a set of axioms. The complete file names are unique within the TPTP. For example, the file GRP135-1.002.p contains the group theory problem number 135, version number 1, generated size 2. Similarly, the file CAT001-0.ax contains the basic category theory axiomatization number 1.

A regular expression for recognizing problem file names is "[A-Z]{3}[0-9]{3}[-+^=_][1-9][0-9]*(\.[0-9]{3})*\.p". A regular expression for recognizing axiom file names is "[A-Z]{3}[0-9]{3}[-+^=_][1-9][0-9]*\.ax".

DDD NNN F V .SSS .T
DDD - Domain name abbreviation.
NNN - Abstract problem number. It is unique within the domain.
F - Form. ^ for THF, _ for TFF without arithmetic, = for TFF with arithmetic, + for FOF, and - for CNF.
V - Version number. It differentiates between different versions of the abstract problem.
SSS - Size parameter(s). These only occur for generated problems, and give the size parameter(s).
T - File name extension. p for problem files, g for generator files.

Problem file naming scheme.

The version numbers used for each abstract problem do not always start at 1, and are not always successive. This is because the same version number is assigned (wherever possible) to all problems that come from the same source, within each domain.

DDD NNN F V .TT
DDD - Domain name abbreviation.
NNN - Axiomatization number. It is unique within the domain.
F - Form. ^ for THF, _ for TFF without arithmetic, = for TFF with arithmetic, + for FOF, and - for CNF.
V - Specialization number. It identifies sets of axioms that are used to specialize an axiomatization. Axiomatizations of basic theories are allocated the number 0, and specialization axiom sets are numbered from 1 onwards.
T - File name extension. An extension is always ax.

Axiom file naming scheme.

If a file is ever removed from or renamed in the TPTP, then its extension is changed to .rm. The file is not physically removed, and a comment is added to the file to explain what has happened. This mechanism maintains the unique identification of problems and axiomatizations.

Problem Presentation

The physical presentation of the TPTP problem library is such that ATP researchers can easily use the problems. The syntax of all files is that of Prolog (with some operators defined). This conformance makes it trivial to manipulate the files using Prolog. All information that is not for use by ATP systems is formatted as comments. Comments extend from a % character to the end of the line, or may be block comments within /* ... */ bracketing. The TPTP file format, for problem files and axiom files, has three main sections. The first section is a header section that contains information for the user. This information is not for use by ATP systems. The second section contains include directives for axiom files. The last section contains the formulae that are specific to the problem or axiomatization. TPTP generator files have three sections, different from the problem and axiom files. The header section of generator files is similar to that of problem and axiom files, but with place-holders for information that is filled in based on the size of problem and the formulae generated. Following that comes Prolog source code to generate the formulae, and finally data describing the permissible sizes and the chosen TPTP size for the problem. More details are provided here.

A full BNF specification of the problem and axiom file formats is provided in the Documents directory of the TPTP. The TPTP2X and TPTP4X utilities can be used to convert TPTP files to other known ATP system formats. A description of the information contained in TPTP files is given below.

The problem files SYN000* are contrived to use most features of the TPTP language, and are thus suitable for testing parsers, etc. They are not suitable for evaluating ATP systems' reasoning capabilities.

The Header Section

This section contains information about the problem, for the user. It is divided into four parts separated by blank lines. The first part identifies and describes the problem. The second part provides information about occurrences of the problem in the literature and elsewhere. The third part gives the problem's ATP status and a table of syntactic measurements made on the problem. The last part contains general information about the problem. An example of a TPTP header, from the problem file GRP194+1.p, is shown in Figure Example header. 

%--------------------------------------------------------------------------
% File     : GRP194+1 : TPTP v8.0.0. Released v2.0.0.
% Domain   : Group Theory (Semigroups)
% Problem  : In semigroups, a surjective homomorphism maps the zero
% Version  : [Gol93] axioms.
% English  : If (F,*) and (H,+) are two semigroups, phi is a surjective
%            homomorphism from F to H, and id is a left zero for F,
%            then phi(id) is a left zero for H.

% Refs     : [Gol93] Goller (1993), Anwendung des Theorembeweisers SETHEO a
% Source   : [Gol93]
% Names    :

% Status   : Theorem
% Rating   : 0.22 v7.5.0, 0.25 v7.4.0, 0.10 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.36 v6.1.0, 0.47 v6.0.0, 0.35 v5.5.0, 0.37 v5.4.0, 0.50 v5.3.0, 0.48 v5.2.0, 0.40 v5.1.0, 0.33 v4.1.0, 0.35 v4.0.1, 0.30 v4.0.0, 0.29 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.21 v3.3.0, 0.14 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.12 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1, 0.00 v2.1.0
% Syntax   : Number of formulae    :    8 (   2 unt;   0 def)
%            Number of atoms       :   21 (   4 equ)
%            Maximal formula atoms :    4 (   2 avg)
%            Number of connectives :   13 (   0   ~;   0   |;   6   &)
%                                         (   1 <=>;   6  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   5 avg)
%            Maximal term depth    :    3 (   1 avg)
%            Number of predicates  :    3 (   2 usr;   0 prp; 2-2 aty)
%            Number of functors    :    5 (   5 usr;   3 con; 0-3 aty)
%            Number of variables   :   15 (  14   !;   1   ?)
% SPC      : FOF_THM_RFO_SEQ

% Comments :
%--------------------------------------------------------------------------
Example of a problem file header (GRP194+1.p).

The % File field.
This field contains three items of information. The first item is the problem's name. The current TPTP release number is given next, followed by the TPTP release in which the problem was released or last bugfixed (i.e., the formulae were changed).

The % Domain field.
The domain field identifies the domain, and possibly a subdomain, from which the problem is drawn. The domain corresponds to the first three letters of the problem name.

The % Problem field.
This field provides a one-line, high-level description of the abstract problem. In axiom files, this field is called % Axioms, and provides a one-line, high-level description of the axiomatization.

The % Version field.
This field gives information that differentiates this version of the problem from other versions of the problem. The first possible differentiation is the axiomatization that is used. If a specific axiomatization is used, a citation is provided. If the axiomatization is a pure equality axiomatization (uses only the equal/2 predicate) then this is noted too.

The second possible differentiation is the status of the axiomatization. There are 12 possiblities:

The third possible differentiation between problem versions is in the theorem formulation. Variations in the theorem formulation are noted in a Theorem formulation entry, e.g.,
% Version  : [McCharen, et al., 1976] (equality) axioms.
%            Theorem formulation : Explicit formulation of the commutator.

The % English field.
This field provides a full description of the problem, if the one-line description in the % Problem field is too terse.

The % Refs field.
This field provides a list of abbreviated references for material in which the problem has been presented. Other relevant references are also listed. The reference keys identify BibTeX entries in the Bibliography.bib file supplied with the TPTP.

The % Source field.
This field acknowledges the source of the problem, usually as a citation. If the problem was sourced from an existing problem collection then the collection name is given in [ ] brackets. The problem collections used thus far are:

The % Names field.
Problems that have appeared in other problem collections or the literature, often have names which are known in the ATP community. This field lists such names for the problem, along with the source of the name. If the source is an existing problem collection then the collection name is cited, as in the % Source field. If the source of a name is a paper then a citation is given. If a problem is not given a name in a paper then ``-'' is used as the known name and a citation is given. Problems that first appeared in the TPTP have source TPTP, and no other name. In generator files all known names for instances of the abstract problem are listed, with the instance size given before the source. A reverse index, from known names to TPTP names, is distributed with the TPTP.

The % Status field.
This field gives the ATP status of the problem, according to the SZS ontology. For THF, TFF, and FOF problems it is one of the following values. For THF problems the default semantics is Henkin with extensionality and choice. If the status is different for other semantics, this is noted on lines after the % Status field.

For CNF problems it is one of: The % Rating field.
This field gives the difficulty of the problem, measured relative to state-of-the-art ATP systems. It is a comma separated list of ratings, each with a TPTP release number. The rating is a real number in the range 0.0 to 1.0, where 0.0 means that all state-of-the-art ATP systems can solve the problem (i.e., the problem is easy), and 1.0 means no state-of-the-art ATP system can solve the problem (i.e., the problem is hard). The rating is followed by a TPTP release number, indicating in which release the rating was assigned. If no rating has been assigned, a ? is given.

The % Syntax field.
This field lists various syntactic measures of the problem's formulae. The measures for THF problems are:

The measures for TFF problems are: The measures for FOF problems are: The measures for CNF problems are: See A HREF="#InsideTheTPTP">the summary of this information over the entire TPTP.

The % SPC field.
This field indicates to which Specialist Problem Class (SPC) the problem belongs. SPCs are sets of problems that have similar syntactic characteristics, so that that the problems are reasonably homogeneous with respect ATP systems' performances on the problems. SPCs are used for caclulating the difficulty rating [SS01], and for recommending systems to use on problems [SS99]. The characteristics used to build the SPCs are:

The % Comments field.
This field contains free format comments about the problem, e.g., the significance of the problem, or the reason for creating the problem. If the problem was created using the TPTP2X utility then the TPTP2X parameters are given.

The % Bugfixes field.
This field describes any bugfixes that have been done to the formulae of the problem. Each entry gives the release number in which the bugfix was done, and attempts to pinpoint the bugfix accurately.

The Include Section

The include section contains include directives for TPTP axiom files. An example extracted from the problem file GEO146+1.p is shown below. 

%--------------------------------------------------------------------------
%----Include simple curve axioms
include('Axioms/GEO004+0.ax').
%----Include axioms of betweenness for simple curves
include('Axioms/GEO004+1.ax').
%----Include oriented curve axioms
include('Axioms/GEO004+2.ax').
%----Include trajectory axioms
include('Axioms/GEO004+3.ax',[connect_defn,symmetry_of_at_the_same_time]).
%--------------------------------------------------------------------------
Example of a problem file include section (adapted from GEO146+1.p).

Each of the include directives indicates that the formulae in the named file should be included at that point. Include files with relative path names are expected to be found either under the directory of the current file, or if not found there then under the directory specified in the TPTP environment variable. If the include directive has a []ed list of formulae names as a second argument, the named file must be filtered to retain only those formulae (this filter also applies to formulae that have been recursively included into the named file). If any member of the list cannot be found, or there are multiple formulae with a given name, that is an error condition. If there is no second argument, or the second argument is all, then all the formulae in the file are included. In the example above only connect_defn and symmetry_of_at_the_same_time are included from Axioms/GEO004+3.ax.

Full versions of TPTP problems (without include directives) can be created by using the TPTP2X and TPTP4X utilities.

A side effect of separating out the axioms into axiom files is that the formula order in the TPTP presentation of problems is typically different from that of any original presentation. This reordering is acceptable because the performance of a decent ATP system should not be very dependent on a particular formula ordering.

Annotated Formulae

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 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 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 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. 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 types and type declarations). 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; conditional (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 and !> [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:

Conditional and Let Expressions
The THF and TXF languages have conditional and let expressions.

Examples
An example CNF problem is PUZ003-1. An example FOF problem is PUZ001+1. An example TFF problem is PUZ031_1. An example TXF problem is PUZ081_8. An example THF problem is PUZ081^1. An example DHF problem is DAT346^1. An example NXF problem is PUZ001_10. An example NHF problem is PHI003^8.

The Type System

A high-level overview is in the section on annotated formulae.

Subtypes
None of the type systems offer subtypes, despite the subtype symbol << being part of the THF and TFF languages. I tried to convince the ATP system developers it would be useful, but they cried crocodile tears. Here's an example of what was planned: 

    tff(food_type,type, food: $tType).

    tff(fruit_type,type, fruit: $tType).

    tff(vegetable_type,type, vegetable: $tType).

    tff(fruit_is_food,type, 
        fruit << food ).

    tff(vegetable_is_food,type, 
        vegetable << food ). 

    tff(apple_decl,type, apple: fruit).

    tff(potatoe_decl,type, potatoe: vegetable).
All subtypes of an atomic type are disjoint, i.e., it is implicit that apple != potatoe.

The Typed First-order Monomorphic Type System (TF0 and TX0)

Refer to [SS+12] (TF0) and [SK18] (TX0) for more details on type checking and semantics, and much more.

Defined atomic types
The atomic types $i (individuals), $o (Booleans), and $tType are defined. ($tType is the "type" of atomic types - it is not really a type, and in other places this is known as the "kind" of atomic types. See below for motivation for its existence and usage.) Other defined atomic types are associated with specific theories. In particular, $int, $rat, and $real are types for arithmetic. The type $i of individuals is predefined but has no peculiar semantics, whereas the arithmetic types $int, $rat, and $real are modeled by ℤ, ℚ, and ℝ, respectively.

User atomic type declarations:
User atomic types are declared in advance of use, to be of "type" $tType. Example: 

    tff(food_type,type, 
        food: $tType ).

    tff(fruit_type,type, 
        fruit: $tType ).

    tff(list_type,type, 
        list: $tType ).

Defined functions and predicates
Defined functions and predicates have preassigned types.

Function and predicate type declarations
Every function and predicate symbol has maximally one declared type. Example: 

    tff(cons_type,type, 
        cons: (fruit * list) > list   ).

    tff(is_empty_type,type, 
        isEmpty: list > $o   ).
The argument types must be atomic, and cannot be $o in TFF, but can be $o in TXF. The range type of a function must be atomic, and cannot be $o. The range type of a predicate is $o. Currying is not possible in TFF or TXF, i.e., the first example above cannot be written cons: fruit > list > list (currying is used in THF and DHF). If a symbol's type is declared more than once, and the types are not the same, that's an error.

Every variable is given an atomic type at quantification time. Example: 

    tff(list_not_empty,axiom, 
        ! [X: fruit,Xs: list] : ~isEmpty(cons(X,Xs))   ).

Implicit typing for functions and predicates
If a symbol is used and its type has not been declared, then default types are assumed.

If a symbol's type is declared later to be different from the assumed type, that's an error.

The Typed First-order Polymorphic Type System (TF1 and TX1)

Refer to [BP13] for more details on type checking and semantics, and much more.

The TF1 polymorphic type system extends the monomorphic type system with rank-1 polymorphism. Syntactically, the types, terms, and formulas of TF1 are analogous to those of TF0, except that function and predicate symbols can be declared to be polymorphic, types can contain type variables, and n-ary type constructors are allowed. Type variables in type signatures and formulas are explicitly bound. Instances of polymorphic symbols are specified by explicit type arguments, rather than inferred.

Types and type signatures
The types of TF1 are built from type variables and type constructors of fixed arities. A type is polymorphic if it contains type variables (otherwise, it is monomorphic). Polymorphic type signatures are of the form: !>[α1 : $tType, ..., αn : $tType]: ς for n > 0, where α1, ..., αn are distinct type variables and ς is a monomorphic type. The binder !> denotes universal quantification.

Type declarations
Type constructors can be declared, e.g., the following declarations introduce a type constant bird, a unary type constructor list, and a binary type constructor map: 

    tff(bird_t, type, bird: $tType).
    tff(list_t, type, list: $tType > $tType).
    tff(map_t, type, map: ($tType * $tType) > $tType).
Every type variable must be bound by a !>-binder. The following declarations introduce a polymorphic predicate is_empty, and a pair of polymorphic functions cons and lookup: 
    tff(is_empty_t, type, is_empty : !>[A : $tType]: (list(A) > $o)).
    tff(cons_t, type, cons : !>[A : $tType]: ((A * list(A)) > list(A))).
    tff(lookup_t, type, lookup : !>[A : $tType, B : $tType]: ((map(A, B) * A) > B)).

Using symbols with a polymorphic type
Every use of a polymorphic symbol must explicitly specify the type instance. A function or predicate symbol with a type signature !>[α1$: $tType, ..., αm : $tType]: ((τ1 * ... * τn) > υ) must be applied to m type arguments and n term arguments. Given the above signatures, the term lookup($int, list(A), M, 2) and the atom is_empty($i, cons($i, X, nil($i))) are well-formed and contain free occurrences of the type variable A and the term variable X, respectively. As TF1 is restricted to rank-1 polymorphism, type variables can be instantiated with only concrete types. In particular, $o, $tType, and !>-binders cannot occur in type arguments of polymorphic symbols.

Every variable in a TF1 formula must be bound. In particular, every type variable in a TF1 formula must be bound with the pseudotype $tType: 

    tff(bird_list_not_empty, axiom,
        ![B : bird, Bs : list(bird)]: ~ is_empty(bird, cons(bird, B, Bs))).

    tff(lookup_update_same, axiom,
        ! [A : $tType, B : $tType, M : map(A, B), K : A, V : B]:
          lookup(A, B, update(A, B, M, K, V), K) = V).
Universal and existential quantifiers over type variables may not occur in the scope of a quantifier over a term variable (as is possible in dependent types).

Example
An example TF1 problem is PUZ139_1.

The Typed Higher-order Monomorphic Type System (TH0)

Refer to [SB10] for more details on type checking and semantics, and much more.

The TH0 monomorphic type system lifts the TF0 type system to simply typed λ-calculus, with Henkin semantics (i.e., including Boolean and functional extensionality) and choice. Type signatures are curried, and variables can have function types. Example: 

    thf(mix_type,type,
        mix: beverage > syrup > beverage ).
    
    thf(mixed_coffee,conjecture,
        ? [Mixture: beverage > syrup > beverage] :
        ! [S: syrup] :
          ( ( Mixture @ coffee @ S ) = coffee ) ).

An example TH0 problem is PUZ140^1.

The Typed Higher-order Polymorphic Type System (TH1)

Refer to [KSR16] for more details on type checking and semantics, and much more.

The TH1 polymorphic type system combines the polymorphic features of TF1/TX1 with the higher-order features of TH0.
Example: 

    thf(list,type, list: $tType > $tType ).
    
    thf(nil,type, nil: !>[A: $tType] : ( list @ A ) ).
    
    thf(append,type, append: !>[A: $tType] : ( ( list @ A ) > ( list @ A ) > ( list @ A ) ) ).
    
    thf(append_nil,axiom,
        ! [A: $tType,L: list @ A] :
          ( ( append @ A @ ( nil @ A ) @ L ) = L ) ).

TH1 has five additional polymorphic constants: !! for Π (universal quantification), ?? for Σ (existential quantification), @@+ for ε (indefinite description, aka choice), @@- for ι (definite description), and @= (equality). The type of the first four is !>[A: $tType] : (A > $o) > $o, and the type of @= is !>[A: $tType]: (A > A) > $o. When used they must be instantiated by applying them to a type argument. Example: 

    thf(eps,type, eps: ( $i > $o ) > $i ).
    
    thf(choiceax,axiom,
        ! [P: $i > $o] :
          ( ? [X: $i] : ( P @ X )
         => ( P @ ( eps @ P ) ) ) ).
    
    thf(conj,conjecture,
        ( ( ^ [P: $i > $o] : ( P @ ( eps @ P ) ) )
        = ( ^ [P: $i > $o] : ( ?? @ $i @ P ) ) ) ).
    
    thf(bird_type,type, bird: $tType).

    thf(tweety_decl,type, tweety: bird).

    thf(some_tweety,axiom,
        ? [B: bird] : ( (@= @ bird) @ tweety @ B ) ).

An example TH1 problem is DAT434^1.

The Dependently Typed Higher-order Type System (DH0 and DH1)

Refer to [RK+25] for more details on type checking and semantics, and much more.

The DH0 and DH1 type systems add dependent types, i.e., types that take term arguments, to TH0 and TH1. As such they are classical and extensional type theories. The !> binder used for TF1 and TH1 polymorphism is reused to specify the term typess on which a type depends. Example: 

    thf(elem_type,type, elem: $tType ).

    thf(nat_type,type, nat: $tType ).

    thf(zero_type,type, zero: nat ).

    thf(suc_type,type, suc: nat > nat ).

    thf(plus_type,type, plus: nat > nat > nat ).

    thf(list_type,type, list: nat > $tType ).

    thf(nil_type,type, nil: list @ zero ).

    thf(cons_type,type, cons:
        !>[N: nat] : (elem > (list @ N) > (list @ (suc @ N))) ).

    thf(app_type,type, app:
        !>[N: nat,M: nat] : ((list @ N) > (list @ M) > (list @ (plus @ N @ M))) ).
The application operator @ is used to instantiate the terms to the dependent type. With polymorphic types, the variable list is prepended with the type variables. Example: 
    thf(ax1,axiom,
        ! [N: nat] : ((plus @ zero @ N) = N) ).

    thf(ax2,axiom,
        ! [N: nat,X: list @ N] : ((app @ zero @ N @ nil @ X) = X) ).

    thf(list_app_assoc_base,conjecture,
        ! [M2: nat,L2: list @ M2,M3: nat,L3: list @ M3] :
          ( ( app @ zero @ ( plus @ M2 @ M3 ) @ nil @ ( app @ M2 @ M3 @ L2 @ L3 ) )
          = ( app @ ( plus @ zero @ M2 ) @ M3 @ ( app @ zero @ M2 @ nil @ L2 ) @ L3 ) ) ).
An example DH0 problem is DAT346^1. An example DH1 problem is DAT342^1.

The Arithmetic System

Arithmetic must be done in the context of the THF or TFF types logics, which support the predefined atomic numeric types $int, $rat, and $real. Using THF or TFF enforces semantics that separate $int from $rat from $real from $i from $o. The numbers are unbounded, and the reals of infinite precision (rather than some specific implementation such as 32 bit 2's complement integer, or IEEE floating point). Systems that implement limited arithmetic must halt in an SZS error state if they hit overflow.

The following interpreted predicates and interpreted functions are defined. The symbols are overloaded (i.e., ad-hoc polymorphic) for the provided type signatures.

Symbol Types Operation Comments, examples                                        -
$int $tType The type of integers 123, -123
<integer>            ::- (<signed_integer>|<unsigned_integer>)
<signed_integer>     ::- <sign><unsigned_integer>
<unsigned_integer>   ::- <decimal>
<decimal>            ::- (<zero_numeric>|<positive_decimal>)
<positive_decimal>   ::- <non_zero_numeric><numeric>*
<sign>               ::: [+-]
<zero_numeric>       ::: [0]
<non_zero_numeric>   ::: [1-9]
<numeric>            ::: [0-9]
$rat $tType The type of rationals 123/456, -123/456, +123/456 
<rational>           ::- (<signed_rational>|<unsigned_rational>)
<signed_rational>    ::- <sign><unsigned_rational>
<unsigned_rational>  ::- <decimal><slash><positive_decimal>
<slash>              ::: [/]
$real $tType The type of reals 123.456, -123.456,
123.456E789, 123.456e789, -123.456E789,
123.456E-789, -123.456E-789 
<real>               ::- (<signed_real>|<unsigned_real>)
<signed_real>        ::- <sign><unsigned_real>
<unsigned_real>      ::- (<decimal_fraction>|<decimal_exponent>)
<decimal_exponent>   ::- (<decimal>|<decimal_fraction>)<exponent><decimal>
<decimal_fraction>   ::- <decimal><dot_decimal>
<dot_decimal>        ::- <dot><numeric><numeric>*
<dot>                ::: [.]
<exponent>           ::: [Ee]
= (infix) ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
 Comparison of two numbers. The numbers must be the same atomic type (see the type system).
$less/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
 Less-than comparison of two numbers. $less, $lesseq, $greater, and $greatereq are related by
  ! [X,Y] : ( $lesseq(X,Y) <=> ( $less(X,Y) | X = Y ) )
  ! [X,Y] : ( $greater(X,Y) <=> $less(Y,X) )
  ! [X,Y] : ( $greatereq(X,Y) <=> $lesseq(Y,X) )
i.e, only $less and equality need to be implemented to get all four relational operators.
$lesseq/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
 Less-than-or-equal-to comparison of two numbers.
$greater/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
 Greater-than comparison of two numbers.
$greatereq/2 ($int * $int) > $o
($rat * $rat) > $o
($real * $real) > $o
 Greater-than-or-equal-to comparison of two numbers.
$uminus/1 $int > $int
$rat > $rat
$real > $real
 Unary minus of a number. $uminus, $sum, and $difference are related by
  ! [X,Y] : $difference(X,Y) = $sum(X,$uminus(Y))
i.e, only $uminus and $sum need to be implemented to get all three additive operators.
$sum/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
 Sum of two numbers.
$difference/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
 Difference between two numbers.
$product/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
 Product of two numbers.
$quotient/2 ($int * $int) > $rat
($rat * $rat) > $rat
($real * $real) > $real
 Exact quotient of two numbers of the same type. For non-zero divisors, the result can be computed. For zero divisors the result is not specified. In practice, if an ATP system does not "know" that the divisor is non-zero, it should simply not evaluate the $quotient. Users should always guard their use of $quotient using inequality, e.g.,
  ! [X: $real] : ( X != 0.0 => p($quotient(5.0,X)) )
For $rat or $real operands the result is the same type. For $int operands the result is $rat; the result might be simplied.
$quotient_e/2, $quotient_t/2, $quotient_f/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
 Integral quotient of two numbers. The three variants use different rounding to an integral result:
  • $quotient_e(N,D) - the Euclidean quotient, which has a non-negative remainder. If D is positive then $quotient_e(N,D) is the floor (in the type of N and D) of the real division N/D, and if D is negative then $quotient_e(N,D) is the ceiling of N/D.
  • $quotient_t(N,D) - the truncation of the real division N/D.
  • $quotient_f(N,D) - the floor of the real division N/D.
For zero divisors the result is not specified.
$remainder_e/2, $remainder_t/2, $remainder_f/2 ($int * $int) > $int
($rat * $rat) > $rat
($real * $real) > $real
 Remainder after integral division of two numbers. For τ ∈ {$int,$rat, $real}, ρ ∈ {e, t,f}, $quotient_ρ and $remainder_ρ are related by
  ! [N:τ,D:τ] : $sum($product($quotient_ρ(N,D),D),$remainder_ρ(N,D)) = N
For zero divisors the result is not specified.
$floor/1 $int > $int
$rat > $rat
$real > $real
 Floor of a number. The largest integral value (in the type of the argument) not greater than the argument (i.e., ! [X] : ($is_int($floor(X)))).
$ceiling/1 $int > $int
$rat > $rat
$real > $real
 Ceiling of a number. The smallest integral value (in the type of the argument) not less than the argument (i.e., ! [X] : ($is_int($ceiling(X)))).
$truncate/1 $int > $int
$rat > $rat
$real > $real
 Truncation of a number. The nearest integral value (in the type of the argument) with magnitude not greater than the absolute value of the argument (i.e., ! [X] : ($is_int($truncate(X)))).
$round/1 $int > $int
$rat > $rat
$real > $real
 Rounding of a number. The nearest integral value (in the type of the argument) to the argument (i.e., ! [X] : ($is_int($rount(X)))). If the argument is halfway between two integral values, the nearest even integral value to the argument.
$abs/1 $int > $int
$rat > $rat
$real > $real
 Absolute value of a number. $abs is related to other operators by 
    ! [X] :
      ( ( $greatereq(X,0)
       => $abs(X) = X )
      & ( $less(X,0)
       => $abs(X) = $uminus(X) ) )
$is_int/1 $int > $o
$rat > $o
$real > $o
 Test for coincidence with an $int value.
$is_rat/1 $int > $o
$rat > $o
$real > $o
 Test for coincidence with a $rat value.
$to_int/1 $int > $int
$rat > $int
$real > $int
 Coercion of a number to $int. The largest $int not greater than the argument; the argument effectively gets truncated before conversion: ! [X] : ($to_int($truncate(X)) = $to_int(X)). If applied to an argument of type $int, this is the identity function.
$to_rat/1 $int > $rat
$rat > $rat
$real > $rat
 Coercion of a number to $rat. This function is not fully specified. If applied to an argument of type $int, the result is the argument over 1. If applied to an argument of type $rat, this is the identity function. If applied to an argument of type $real that is (known to be) rational, the result is the $rat value. For other reals the result is not specified. In practice, if an ATP system does not "know" that the argument is rational, it should simply not evaluate the $to_rat. Users should always guard their use of $to_rat using $is_rat, e.g.,
  ! [X: $real] : ( $is_rat(X) => p($to_rat(X)) )
$to_real/1 $int > $real
$rat > $real
$real > $real
 Coercion of a number to $real. If applied to an argument of type $real, this is the identity function.

The extent to which ATP systems are able to work with the arithmetic predicates and functions can vary, from a simple ability to evaluate ground terms, e.g., $sum(2,3) can be evaluated to 5, through an ability to instantiate variables in equations involving such functions, e.g., $product(2,$uminus(X)) = $uminus($sum(X,2)) can instantiate X to 2, to extensive algebraic manipulation capability. The syntax does not axiomatize arithmetic theory, but may be used to write axioms of the theory.

The Non-classical Logics

The TPTP recognizes several normal modal logics, and one temporal logic. Each logic has a define name: Connectives
The non-classical connectives of NTF have the form {$name}. For the logics recognized by the TPTP the connectives are: (System names may also be used for user-defined connectives, e.g., {$$canadian_conditional}, thus allowing use of the TPTP syntax when experimenting with logics that have not yet been formalized in the TPTP.) A connective can be parameterized to reflect more complex non-classical connectives. The form is {$name(param1,param2,param2)}. If the connective is indexed the index is given as the first parameter prefixed with a #, e.g., {$knows(#manuel)} @ (nothing)}, so that the connective is {$knows(#manuel)} (and not the connective {$knows} applied to the index #manuel). All other parameters are key-value assignments, e.g., to list the agents of common knowledge the form might be {$common($agents:=[alice,bob,claire])}.

In NXF the non-classical connectives are applied in a mixed higher-order-applied/first-order-functional style, with the connectives applied using @ to a ()ed list of arguments. In NHF the non-classical connectives are applied using @ in usual higher-order style with curried function applications. There are also short form unary connectives for unparameterised {$box} and {$dia}, applied directly like negation: [.] and <.>, e.g., {$box} @ (p) can be written [.] p. Short forms and long forms can be used together, e.g., it’s OK to use {$necessary} and [.] in the same problem or formula.

Full specification of the connectives and their use in formulae is in the BNF starting at <nxf_atom> and <thf_defined_atomic>.

Semantics Specification
An annotated formula with the role logic is used to specify the semantics of formulae. The semantic specification typically comes first in a file. A semantic specification consists of the defined name of the logic followed by == and a list of properties value assignments. Each specification is the property name, followed by == and either a value or a tuple of specification details. If the first element of a list of details is a value, that is the default value for all cases that are not specified in the rest of the list. Each detail after the optional default value is the name of a relevant part of the vocabulary of the problem, followed by == and a value for that named part. The BNF grammar is here. The grammar is not very restrictive on purpose, to enable working with other logics as well. It is possible to create a lot of nonsense specifications, and to say the same thing in different meaningful ways. A tool to check the sanity of a specification is available.

A semantic specification changes the meaning of things such as the boolean type $o, universal quantification with !, etc - their existing meaning in classical logic should not be confused with the meaning in the declared logic.

For plain $modal and all the *_modal logics the properties that may be specified are $domains, $designation, $terms, and $modalities.

For $temporal_instant the properties are the $domains, $designation, and $terms of the modal logic, $modalities with different possible values, and another property $time.

The formulae of a problem can be either local (true in the current world) or global (true in all worlds). By default, formulae with the roles hypothesis and conjecture are local, and all others are global. These defaults can be overridden by adding a subrole, e.g., axiom-$local, conjecture-$global.

Physical Organization

The TPTP is physically organized into six subdirectories, as follows: