The TPTP Problem Library

TPTP v8.0.0

Geoff Sutcliffe
Department of Computer Science
University of Miami
geoff@cs.miami.edu

Abstract

This report provides a detailed description of the TPTP Problem Library for automated theorem proving systems. The library forms a common basis for development of and experimentation with automated theorem provers. This report provides:

If you're new to all this and don't want to wade through the details provided in this manual, you might want to start at the TPTP and TSTP Quick Guide.
You could also work your way through the slides of the TPTP World Tutorial.


Table of Contents



Introduction

The TPTP (Thousands of Problems for Theorem Provers) is a library of problems, in classical logic with an interpreted equality symbol, for Automated Theorem Proving (ATP) systems. The TPTP contains problems in monomorphic and polymorphic typed higher-order form (THF), monomorphic and polymorphic typed first-order form (TFF, including the extended first-order form (TXF)), first-order form (FOF), and clause normal form (CNF). Interpreted arithmetic types and symbols are supported in THF, TXF, and TFF. The TPTP supplies the automated reasoning community with a comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism. The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect the capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP problems are stored in a specifically designed, easy to understand format. Utilities for manipulating the problems, for converting the problems to other known ATP formats, and for finding problems with certain characteristics, are provided. Since its first release in 1993, many researchers have used the TPTP as an appropriate and convenient basis for ATP system evaluation.

This technical report explains the motivations and reasoning behind the development of the TPTP, and thus implicitly explains the design decisions made. It also serves as a manual explaining the structure and use of the TPTP: it provides a full description of the TPTP contents and organization, details of the utility programs, and guidelines for obtaining and using the TPTP.

What's New in TPTP v8.0.0 (since TPTP v7.0.0):

Previous Problem Collections

A large number of interesting problems had accumulated over the years in the ATP community. Besides publishing particularly interesting individual problems, from early on researchers collected problems in order to obtain a basis for experimentation. Problems in First Order Form (FOF), published by mathematicians and logicians prior to the mechanization of reasoning (e.g., [
Chu56]) provided the first source for ATP researchers. The first major publication in this regard was [MOW76], which provides an explicit listing of clauses for 63 Clause Normal Form (CNF) problems, many of which are still relevant today (to our knowledge, the first circulation of problems for testing ATP systems was due to Larry Wos in the late sixties). In the same year [WM76] documented 86 CNF problems which were commonly used for ATP testing. However, the problem clauses are not supplied in [WM76]. A second major thrust was provided by [Pel86], which lists 75 problems in both FOF and CNF. Other early papers are [BL+86], [Qua92], [MW92], and [McC93], to name a few. The Journal of Automated Reasoning's Problem Corner also provided interesting challenge problems. Problems published in hardcopy form are, however, often not suitable for testing ATP systems, because they have to be transcribed to electronic form. This is a cumbersome, error-prone process, and is feasible for only small numbers of small problems.

The sparsness of research into ATP systems for FOF problems meant that no electronic collections of FOF test problems had previously been commonly available. A CNF problem collection in electronic form was made publicly available by Argonne National Laboratories (in Otter format [McC94]) in 1988 [ANL]. This collection was a major source of problems for ATP researchers. Other electronic collections of CNF problems have been available, but not announced officially (e.g., that distributed with the SPRFN ATP system [SPRFN]). Although some of these collections provided significant support to researchers, and formed the early core of the TPTP library, none (with the possible exception of the ANL collection) was specifically designed to serve as a common basis for ATP research. Rather, these collections typically were built in the course of research into a particular ATP system. As a result there are several factors that limited their usefulness as a common basis for research. In particular, previously existing problem collections:

The problem of meaningfully interpreting results can be even worse than indicated. A few problems might be selected and hand-tuned (formulae arranged in a special way, irrelevant formulae omitted, lemmas added in, etc) specifically for the ATP system being tested. The presentation of a problem can significantly affect the nature of the problem, and changing the formulae clearly makes a different problem altogether. Nevertheless the problem might be referenced under the same name as it was presented elsewhere. As a consequence the experimental results reveal little. Some researchers avoid this ambiguity by listing the formulae explicitly, but obviously this usually cannot be done for a large number of problems or for large individual problems. The only satisfactory solution to these issues is a common and stable library of problems. The TPTP is such a library.

What is Required?

The goal for building the TPTP has been to overcome previous drawbacks, and to centralize the burden of problem collection and maintenance. The TPTP tries to address all relevant issues. In particular, the TPTP:

The development of the TPTP problem library is an ongoing project, with the aim to provide all of the desired properties.

Current Limitations of the TPTP.
The TPTP library currently limited to problems expressed in classical logic.



Inside the TPTP

Scope.
The TPTP contains problems in classical logic with an interpreted equality symbol. Release v8.0.0 of the TPTP contains 15514 abstract problems, which result in 24785 ATP problems (due to
alternative presentations, and Problem Generators). There are 3432 THF abstract problems, which result in 4693 THF ATP problems, 2145 TFF abstract problems, which result in 2744 TFF ATP problems of which 104 are TXF problems, and 6033 FOF abstract problems, which result in 9091 FOF ATP problems, and 6259 CNF abstract problems, which result in 8257 CNF ATP problems. 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 TPTP 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
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
Science and Engineering Biology BIO
Hardware creation HWC
Hardware verification HWV
Medicine MED
Processes PRO
Products PRD
Social sciences Social Choice Theory SCT
Management MGT
Geography GEG
Arts and Humanities Philosophy PHI
Other Arithmetic ARI
Syntactic SYN and SYO
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 problem status 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.

The Formulae Section

Each logical formula is wrapped in an annotated formula structure of the form language(name,role,formula,source,[useful_info]).. The languages currently supported are thf - formulae in typed higher-order form, tff - formulae in typed first-order form (including extended form), fof - formulae in first order form, and cnf - formulae in clause normal form. The name identifies the formula within the problem. The role gives the user semantics of the formula, one of axiom, hypothesis, definition, assumption, lemma, theorem, corollary, conjecture, negated_conjecture, plain, type, 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 only 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 solution output. type formulae define the types of symbols globally. unknowns have unknown role, and this is an error situation.

The syntax for atoms is that of Prolog: variables start with upper case letters, atoms and terms are written in prefix notation, uninterpreted predicates and functors either start with lower case and contain alphanumerics and underscore, or are in 'single quotes'. The language also supports interpreted predicates and functors. These come in two varieties: defined predicates and functors, whose interpretation is specified by the TPTP language, and system predicates and functors, whose interpretation is ATP system specific. Interpreted predicates and functors are syntactically distinct from uninterpreted ones - they are = and !=, or start with a $, a ", or a digit. Non-variable symbols can be given a type globally, in the formula with role type. The defined types are $o - the Boolean type, $i - the type of individuals, $real - the type of reals, $rat - the type of rational, and $int - the type of integers. New types are introduced in formulae with the type role, based on $tType - the type of all types. Full details of the THF and TFF type systems are provided in [SS+12,BP13,SB10,KSR16], with the last providing an overview of the first three.

The defined predicates recognized so far are

The defined functors recognized so far are

System predicates and functors are used for interpreted predicates and functors that are available in particular ATP tools. System predicates and functors start with $$. The names are not controlled by the TPTP language, so they must be used with caution.

The connectives used to build non-atomic formulae are written using intuitive notations. The universal quantifier is !, the existential quantifier is ?, and the lambda binder is ^. Quantified formulae are written in the form Quantifier [Variables] :  Formula. In the THF, TFF, and FOF languages, every variable in a Formula must be bound by a preceding quantification with adequate scope. Typed Variables are given their type by a :type suffix. The binary connectives are infix | for disjunction, infix & for conjunction, infix <=> for equivalence, infix => for implication, infix <= for reverse implication, infix <~> for non-equivalence (XOR), infix ~| for negated disjunction (NOR), infix ~& for negated conjunction (NAND), infix @ for application. The only unary connective is prefix ~ for negation. 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. The binary connectives are left associative.

The THF and TFF languages have conditional and let expressions.

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.

An example of a THF formula section, extracted from the problem file LCL633^1.p, is shown below. An example of a TFF formula section, extracted from the problem file DAT013=1.p, is shown below that. Example THF formulae. An example of a FOF formula section, extracted from the problem file GRP194+1.p, is shown below that. An example of a clause section, extracted from the problem file GRP039-7.p, is shown below that.

%------------------------------------------------------------------------------
%----Signature
thf(a,type,(
    a: $tType )).

thf(p,type,(
    p: ( a > $i > $o ) > $i > $o )).

thf(g,type,(
    g: a > $i > $o )).

thf(e,type,(
    e: ( a > $i > $o ) > a > $i > $o )).

thf(r,type,(
    r: $i > $i > $o )).

%----Axioms
thf(positiveness,axiom,(
    ! [X: a > $i > $o] :
      ( mvalid
      @ ( mimpl @ ( mnot @ ( p @ X ) )
        @ ( p
          @ ^ [Z: a] :
              ( mnot @ ( X @ Z ) ) ) ) ) )).

thf(g,definition,
    ( g
    = ( ^ [Z: a,W: $i] :
        ! [X: a > $i > $o] :
          ( mimpl @ ( p @ X ) @ ( X @ Z ) @ W ) ) )).

thf(e,definition,
    ( e
    = ( ^ [X: a > $i > $o,Z: a,P: $i] :
        ! [Y: a > $i > $o] :
          ( mimpl @ ( Y @ Z )
          @ ( mbox @ r
            @ ^ [Q: $i] :
              ! [W: a] :
                ( mimpl @ ( X @ W ) @ ( Y @ W ) @ Q ) )
          @ P ) ) )).

%----Conjecture
thf(thm,conjecture,
    ( mvalid
    @ ^ [W: $i] :
      ! [Z: a] :
        ( mimpl @ ( g @ Z ) @ ( e @ g @ Z ) @ W ) )).
%------------------------------------------------------------------------------
Example of a THF problem file formulae section (LCL633^1.p).
%------------------------------------------------------------------------------
tff(list_type,type,(
    list: $tType )).

tff(nil_type,type,(
    nil: list )).

tff(mycons_type,type,(
    mycons: ( $int * list ) > list )).

tff(sorted_type,type,(
    fib_sorted: list > $o )).

tff(empty_fib_sorted,axiom,(
    fib_sorted(nil) )).

tff(single_is_fib_sorted,axiom,(
    ! [X: $int] : fib_sorted(mycons(X,nil)) )).

tff(double_is_fib_sorted_if_ordered,axiom,(
    ! [X: $int,Y: $int] :
      ( $less(X,Y)
     => fib_sorted(mycons(X,mycons(Y,nil))) ) )).

tff(recursive_fib_sort,axiom,(
    ! [X: $int,Y: $int,Z: $int,R: list] :
      ( ( $less(X,Y)
        & $greatereq(Z,$sum(X,Y))
        & fib_sorted(mycons(Y,mycons(Z,R))) )
     => fib_sorted(mycons(X,mycons(Y,mycons(Z,R)))) ) )).

tff(check_list,conjecture,(
    fib_sorted(mycons(1,mycons(2,mycons(4,mycons(7,mycons(100,nil)))))) )).
%------------------------------------------------------------------------------
Example of a TFF problem file formulae section (DAT002=1.p).
%--------------------------------------------------------------------------
%----Definition of a homomorphism
fof(homomorphism1,axiom,
    ( ! [X] :
        ( group_member(X,f)
       => group_member(phi(X),h) ) )).

fof(homomorphism2,axiom,
    ( ! [X,Y] :
        ( ( group_member(X,f)
          & group_member(Y,f) )
       => multiply(h,phi(X),phi(Y)) = phi(multiply(f,X,Y)) ) )).

fof(surjective,axiom,
    ( ! [X] :
        ( group_member(X,h)
       => ? [Y] :
            ( group_member(Y,f)
            & phi(Y) = X ) ) )).

%----Definition of left zero
fof(left_zero,axiom,
    ( ! [G,X] :
        ( left_zero(G,X)
      <=> ( group_member(X,G)
          & ! [Y] :
              ( group_member(Y,G)
             => multiply(G,X,Y) = X ) ) ) )).

%----The conjecture
fof(left_zero_for_f,hypothesis,
    ( left_zero(f,f_left_zero) )).

fof(prove_left_zero_h,conjecture,
    ( left_zero(h,phi(f_left_zero)) )).
%--------------------------------------------------------------------------
Example of a FOF problem file formulae section (GRP194+1.p).

%--------------------------------------------------------------------------
%----Redundant two axioms
cnf(right_identity,axiom,
    ( multiply(X,identity) = X )).

cnf(right_inverse,axiom,
    ( multiply(X,inverse(X)) = identity )).

... some clauses omitted here for brevity

cnf(property_of_O2,axiom,
    ( subgroup_member(X)
    | subgroup_member(Y)
    | multiply(X,element_in_O2(X,Y)) = Y )).

%----Denial of theorem
cnf(b_in_O2,negated_conjecture,
    ( subgroup_member(b) )).

cnf(b_times_a_inverse_is_c,negated_conjecture,
    ( multiply(b,inverse(a)) = c )).

cnf(a_times_c_is_d,negated_conjecture,
    ( multiply(a,c) = d )).

cnf(prove_d_in_O2,negated_conjecture,
    ( ~ subgroup_member(d) )).
%--------------------------------------------------------------------------
Example of a CNF problem file clause section (GRP039-7.p).

The TPTP 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. Each symbol is ad-hoc polymorphic over the numeric types (with one exception - $quotient is not defined for $int). All arguments must have the same numeric type. All the functions, except for the coercion functions $to_int and $to_rat, have the same range type as their arguments. For example, $sum can be used with the type signatures ($int * $int) > $int, ($rat * $rat) > $rat, and ($real * $real) > $real. The coercion function $to_int always has a $int result, and the coercion function $to_rat always has a $rat result. All the predicates have a $o result. For example, $less can be used with the type signatures ($int * $int) > $o, ($rat * $rat) > $o, and ($real * $real) > $o.

Symbol Operation Comments, examples                                        -
$int 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 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 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) Comparison of two numbers. The numbers must be the same atomic type (see the type system).
$less/2 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 Less-than-or-equal-to comparison of two numbers.
$greater/2 Greater-than comparison of two numbers.
$greatereq/2 Greater-than-or-equal-to comparison of two numbers.
$uminus/1 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 Sum of two numbers.
$difference/2 Difference between two numbers.
$product/2 Product of two numbers.
$quotient/2 Exact quotient of two $rat or $real numbers. 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)) )
$quotient_e/2, $quotient_t/2, $quotient_f/2 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 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 Floor of a number. The largest integral value (in the type of the argument) not greater than the argument.
$ceiling/1 Ceiling of a number. The smallest integral value (in the type of the argument) not less than the argument.
$truncate/1 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.
$round/1 Rounding of a number. The nearest integral value (in the type of the argument) to the argument. If the argument is halfway between two integral values, the nearest even integral value to the argument.
$is_int/1 Test for coincidence with an $int value.
$is_rat/1 Test for coincidence with a $rat value.
$to_int/1 Coercion of a number to $int. The largest $int not greater than the argument. If applied to an argument of type $int this is the identity function.
$to_rat/1 Coercion of a number to $rat. This function is not fully specified. If applied to a $int the result is the argument over 1. If applied to a $rat this is the identity function. If applied to a $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 Coercion of a number to $real.

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.


Physical Organization

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


Utilities

The TPTP2X Utility

The TPTP2X utility is a multi-functional utility for reformatting, transforming, and generating TPTP problem files. In particular, it TPTP2X is written in Prolog, and should run on most Prolog systems. Before using TPTP2X, it is necessary to install the code for the dialect of Prolog that is to be used. This and other installation issues are described next.

WARNING: For historical reasons TPTP2X omits the quotes around some constants and function symbols that should be 'Quoted', e.g., as found in PUZ001+2. I'm really sorry about this - it's an artifact of a very generic printing framework that became overloaded when THF formulae came into the TPTP. Changing it would be a HUGE task, and now there's TPTP4X that is better in most respects.

Installation

The TPTP2X utility consists of the following files: TPTP2X is installed by running tptp2X_install, which will prompt for required information. To install TPTP2X by hand, the following must be attended to:

Using TPTP2X

The most convenient way of using the TPTP2X utility is through the tptp2X script. The use of this script is:
tptp2X [-h][-q<Level>][-i][-s<Size>][-t<Transform>][-f<Format>] [-d<Directory>] -l<NamesFile>|<TPTPFiles>
The -h flag specifies that usage information should be output. The -q<Level> flag specifies the level of quietness at which the script should operate. There are three quietness levels; 0 is verbose mode, 1 suppresses informational output from the Prolog interpreter, and 2 suppresses all informational output except lines showing what files are produced. The default quietness level is 1. The -i flag specifies that the script should enter interactive mode after processing all other command line parameters. Interactive mode is described below. The other command line parameter values are:
The output files produced by TPTP2X are named according to the input file name and the options used. The TPTP problem name (the input file name without the .p or .g) forms the basis of the output file names. For files created from TPTP generators, the size parameters are appended to the base name, separated from the base name by a ".". Then, for each transformation applied, a suffix is appended preceded by a +. Finally an extension to indicate the output format is appended to the file name. To record how a TPTP2X output file has been formed, the TPTP2X parameters are given in a % Comments field entry of the output file.

TPTP2X Transformations

The transformations are:
The default transformation is none.

TPTP2X Output Formats

The available output formats are:
The default format is tptp.

Examples

~/TPTP/TPTP2X> tptp2X -tfr,random -f prover9 PUZ001+1
This applies two separate transformations to the problem ALG001-1. The transformations are formula order reversal and formula order randomizing. The transformed problems are output in prover9 format, in a directory prover9/PUZ below the current directory. The file names are PUZ001+1+fr.in and PUZ001+1+ran.in.

~/TPTP/TPTP2X> tptp2X -q2 -s3..5 -fotter -d~tptp/tmp SYN001-1.g
This generates three sizes of the generic problem SYN001-1. The sizes are 3, 4, and 5. The output files are formatted for Otter, to use its auto mode. The files are placed in \verb/~/tptp/tmp/SYN, and are named SYN001-1.003.lop, SYN001-1.004.lop, and SYN001-1.005.lop. The quietness level is set to 2, thus suppressing all informational output except the lines showing what files are produced. Note that the file SYN001-1.g is automatically found in the generators directory.

~/TPTP/TPTP2X> tptp2X -tmagic+shorten - < ~tptp/TPTP/Problems/GRP/GRP001-1.p
This uses the TPTP2X script as a filter, to apply the non-Horn magic set transformation and then the symbol shortening transformation to GRP001-1.p. GRP001-1.p is fed in from standard input, and the output is written to standard output (thus all informational output is suppressed).

The TPTP2X Interactive Mode

If the -i flag is set, the TPTP2X script enters interactive mode after processing all other command line parameters. In interactive mode the user can change the value of any of the command line parameters. The user is prompted for the <TPTPFiles>, the <Size>, the <Transform>, the <Format>, and the <Directory>. In each prompt the current value is given. The user can respond by specifying a new value or by entering <cr> to accept the current value. The prompt-respond loop continues for each parameter until the user accepts the value for the parameter.

Running TPTP2X from within Prolog

The TPTP2X utility can also be run from within a Prolog interpreter. The tptp2X.main file has to be loaded, and the entry point is then tptp2X/5, in the form:

?-tptp2X(<TPTPFile>,<Size>,<Transform>,<Format>,<Directory>).

The parameters are similar to the TPTP2X script command line parameters. A summary, highlighting differences with "(!)", is given here.

Writing your own Transformations and Output Formats

The transformations and output formatting are implemented in Prolog, in the files transform.<TRAN> and format.<ATP>, respectively. It is simple to add new transformations and output formats to the TPTP2X utility, by creating new transformation and format files. New files should follow the structure of the existing files. Typically, a new file can be created by modifying a copy of one of the existing files.

The entry point in a transformation file is <Transform>/6. The first three arguments are inputs: a list of the problem's formulae, the variable dictionary (a bit complicated), and the transformation specification. The next three arguments are outputs: the transformed formulae, the transformed variable dictionary (typically the same as the input dictionary), and the transformation suffix. As well as the <Transform>/6 entry point, a <Transform>_file_information/2 fact must be provided. The two arguments of the <Transform>_file_information/2 fact are the atom transform and a description of the possible transformation specifications (as used in the third argument of <Transform>/6). See the existing transform.<TRAN> files for examples.

The entry point in a format file is <Format>/3. The three arguments are inputs: the format specification, a list of the problem's formulae, and the file header information. (It is not necessary to output a file header here; this information is available only for producing supplementary documentation.) As well as the <Format>/3 entry point, a <Format>_format_information/2 fact and a <Format>_file_information/2 fact must be provided. The two arguments of the <Format>_format_information/2 fact are a character that can be used to start a comment in the output file and the format extension, both as Prolog atoms. The two arguments of the <Format>_file_information/2 fact are the atom format and a description of the possible format specifications. See the existing format.<ATP> files for examples.

New transformation and format files must be compiled in with the other TPTP2X files. This is done by adding a compile query in the tptp2X.main file, alongside the queries that compile in the existing files.

If you need help, please contact the TPTP developers.

Writing your own Problem Generators

The TPTP generators are implemented in Prolog. It is simple to write new generators. New files should follow the structure of the existing files.

The entry point in a generator file is <Problem name>/3, where <Problem name> is the file name without the .g suffix. The first argument is an input: the size parameter for generation. The second and third arguments are outputs: the formulae generated and the % Status of the formulae. The formulae must be a Prolog list of formulae in TPTP format. A <Problem name>_file_information/3 fact must also be provided. The three arguments of the fact are the atom generator, a description of the possible size parameters, and the TPTP size for this problem (this is hard to determine!). See the existing generator files for examples.

If you need help, please contact the TPTP developers.


The TPTP4X Utility

The TPTP4X utility is a multi-functional utility for reformatting, transforming, and generating TPTP problem files. It is the successor to the TPTP2X utility, and offers some of the same functionality, and some extra functionality. TPTP4X is written in C, and is thus faster than TPTP2X.

The TPTP4X usage is Usage: tptp4X <options> <files>. The options are (defaults in ()s):


The TPTP2T Script

The TPTP2T script selects lines from either the
ProblemAndSolutionStatistics file, by problem and solution characteristics.

The TPTP2T script is written in perl.

Installation

Installation of the TPTP2T utility requires simple changes in the tptp2T script. These changes can be made by running tptp2T_install, which will prompt for required information.

Using TPTP2T

The use of this script is:

tptp2T [-f FileName] [-q1 or -q2 or -q3] [-pp or -ps or -pps] {[-]Constraint {[and/or] [-]Constraint}}

The Constraints specify required problem and solution characteristics that must be satisfied for the statistics file line(s) to be selected. There are two sets of constraints, problem constraints and solution constraints, which apply to problem lines and solution lines separately. For a solution line to be printed, the problem line it accompanies must pass all problem constraints, if any are provided. Different sets of solution constraints can be applied to different systems individually.

A problem Constraint is selected from:

A solution <Constraint> is selected from:

Getting and Using the TPTP

Quick Installation Guide

This section explains how to obtain and install the TPTP, and how to syntax-convert the TPTP problems.

Obtaining the TPTP

The distribution consists of two files: There also might be a file called BuggedProblems-v8.0.0 , containing a list of files that have been found to contain errors, in the current release (bugs that have been discovered after the release has been distributed).

These files are available online.

Installing the TPTP

prompt> tar xzf TPTP-v8.0.0 .tgz

prompt> cd TPTP-v8.0.0

prompt> ./Scripts/tptp2T_install
... the script will then ask for required information

prompt> ./TPTP2X/tptp2X_install
... the script will then ask for required information

If you don't have any Prolog installed, you need to get one first. Both utilities can be installed in a default configuration by appending a -default flag to the install command.

Important: Using the TPTP

Appropriate use of the TPTP allows developers and users to meaningfully evaluate ATP systems. To that end, the following guidelines for using the TPTP and presenting results should be followed. Abiding by these conditions will allow unambigous identification of the problem, the formulae used, and further input to the ATP system. If you follow the rules, please make it clear in any presentation of your results, by an explicit statement. We propose that you state "These results were obtained in compliance with the guidelines for use of the TPTP". By making this clear statement, ATP researchers are assured of your awareness of our guidelines. Conversely, it will become clear when the guidelines might have been ignored.

Please contact the TPTP developers if ...



Conclusion

Current Activities

The collection of more problems is continuing. Everybody is invited to submit problems for inclusion.

Current proposals for extensions to the TPTP are online at http://www.tptp.org. Comments are welcome.

If you'd like to be kept informed of developments, join the TPTP World Google Group.

Acknowledgements

We are indebted to the following people and organizations who have helped with the construction of the TPTP.

For contributing problems: Argonne National Laboratory, AR Research Group at TU München, Negin Arhami, Alessandro Armando, Javier Alvez, Rob Arthan, Jaroslav Barta, Peter Baumgartner, Bjoern Pelzer, Dan Benanav, Alexander Bentkamp, Christoph Benzmüller, Marc Bezem, Jasmin Blanchette, Woody Bledsoe, Conrad Bock, Harald Boley, Johan Bos, Marc Boule, Chad Brown, Cristóbal Camarero, Marco Caminati, David Cerna, Vinay Chaudri, Koen Claessen, Simon Colton, Simon Cruanes, David Deharbe, Gerard de Melo, Louise Dennis, Alexander Dvorsky, Christian Fermüller, Jean-Christophe Filliâtre, Bernd Fischer, Paul Fodor, Deepak Garg, Thibault Gauthier, Tim Geisler, Keith Goolsbey, Sylvia Grewe, Johan Gustafsson, Jay Halcomb, John Harrison, Lifeng He, Stefan Hetzl, Thomas Hillenbrand, Tim Hinrichs, Peter Hoefner, Arjen Hommersom, Jack Horner, Ullrich Hustadt, Mikoláš Janota, Thomas Jech, Cezary Kaliszyk, Mark Kaminski, Zurab Khasidashvili, Daniel Kuehlwein, Boris Konev, Laura Kovacs, Ivan Kossey, Evgeny Kotelnikov, Tobias Kuhn, Lars Kulik, Timm Lampert, Rob Lewis, Di Long Li, Meng Luan, Bill McCune, Andreas Meier, Jia Meng, Johan Martensson, Takuya Matsuzaki, Cláudia Nalon, Julian Parsert, Juan Antonio Navarro Perez, Georg Neis, Jens Otten, Andrei Paskevich, Dominique Pastre, Adam Pease, David Plaisted, Larry Paulson, Art Quaife, Pedro Quaresma, Florian Rabe, Silvio Ranise, Thomas Raths, Pace Reagan-Smith, Martin Riener, Philipp Rümmer, Johannes Schoisswohl, Alberto Segre, Renate Schmidt, Michael Schneider, Johannes Schoisswohl, Stefan Schulz, Martina Seidl, Ted Sider, John Slaney, Nick Smallbone, David Stanovsky, Graham Steel, Alexander Steen, Mark Stickel, Nik Sultana, Hans Svensson, Tanel Tammet, Alwen Tiu, Steven Trac, Josef Urban, Bob Veroff, Petar Vukmirovic, Uwe Waldmann, Mark Wallace, Peter Watson, Christoph Weidenbach, Christoph Wernhard, Michael Wessel, Patrick Wischnewski, Thomas Wies, Bruno Woltzenlogel Paleo, Aparna Yerikalapudi, Jian Zhang.

For helping with problems and/or pointing out errors: Geoff Alexander, Johan Belinfante, Alexander Bentkamp, Ahmed Bhayat, Nikolaj Bjorner, Woody Bledsoe, Maria Poala Bonacina, Heng Chu, Koen Claessen, Ingo Dahn, Morgan Deters, Damien Doligez, Alexander Fuchs, Matthias Fuchs, Tim Geisler, John Harrison, John Hester, Thomas Jech, Konstantin Korovin, Ivan Kossey, Harald Ganzinger, Mark Lemay, Reinhold Letz, Ann Lilliestrom, Thomas Ludwig, Klaus Mayr, Bill McCune, Monty Newborn, Xumin Nie, Andrei Paskevich, Dominique Pastre, Jeff Pelletier, Petr Pudlak, Art Quaife, Dimitris Raptis, Michael Raskin, Thomas Raths, Piotr Rudnicki, Masahiro Sakai, Michael Schneider, Len Schubert, Stephan Schulz, Alberto Segre, Stuart Shapiro, Guy Shefner, Andrés Sicard-Ramírez, Nick Siegel, John Slaney, Nick Smallbone, Alex Steen, Mark Stickel, Christoph Sticksel, Martin Suda, Nik Sultana, Bob Veroff, Russell Wallace, TC Wang, Christoph Weidenbach, Hantao Zhang.

For support regarding the utilities: Jesse Alma, Stefan Berghofer, Marc Bezem, Lucas Dixon, Bernd Fischer, Alexander Fuchs, Kal Hodgson, Jose Morales, Max Moser, Gerd Neugebauer, Vladimir Pavlov, Grzegorz Prusak, Petr Pudlak, Alex Roederer, Paul Tarau, Frank Theiss, Abdul Sattar, Renate Schmidt, Andrés Sicard-Ramírez, Jing Tang, Andrei Tchaltsev, Christoph Weidenbach, Makarius Wenzel, Jürgen Zimmer.

For general advice and comments: Serge Autexier, Jasmin Blanchette, Reiner Hähnle, Joe Hurd, Reinhold Letz, Selene Makarios, Diego Páez, Andrei Paskevich, Jeff Pelletier, Florian Rabe, Stephan Schulz, Mark Stickel, Allen van Gelder, Uwe Waldmann, Russell Wallace, Christoph Walther.