TPTP Problem Library Manual

Abstract

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

• the motivations for building the library;

• a discussion of the inadequacies of previous problem collections, and how these have been resolved in the TPTP;

• a description of the library structure, including overview information;

• descriptions of supplementary utility programs;

• guidelines for obtaining and using the library.

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.

Introduction

The TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for Automated Theorem Proving (ATP) systems, in classical and non-classical logics, with an interpreted equality symbol and assuming the axiom of choice. The TPTP contains problems in first-order form (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), and dependently typed monomorphic and polymorphic typed higher-order form (DHF). Interpreted arithmetic types and symbols are supported in the typed logics.

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 manual 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 v9.0.0 (since TPTP v8.0.0):

• This is the first release with non-classical logic problems. There are 147 non-classical logic problems in 8 domains.

• 1 new domain has been added: MVA (MV-algebras)

• The separator for arithmetic problems is no longer '=', but rather whatever is used for the host language, i.e., '_' for TFF and TXF problems, '^' for THF problems.

• The SZS ontology has a new value USM (Unsemantic), and been extended to include non-logical data.

• Many many changes to SyntaxBNF.

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 sparseness 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:

• were often hard to discover and obtain.
  System development and system evaluations typically relied on a small set of test problems, depending on the collections of problems available to the researcher.

• needed to be transformed to the syntax of the ATP system being considered.
  The problem format used in a collection was often inappropriate for the desired purpose, and a comparatively large effort was required just to make the problems locally usable (which in practice often meant that such collections of problems were simply ignored).

• were often limited in scope and size.
  The problems used were often homogeneous, and thus could not be used for broad testing of the capabilities of the ATP system under consideration. If there are too few problems, statistically significant testing is not possible.

• were often outdated.
  The problems did not sufficiently reflect the current state-of-the-art in ATP research.

• were sometimes designed and tuned (regarding formula selection, formula ordering, and formula structure) for a particular ATP system.
  Using a collection designed and tuned for a particular ATP system leads to biases in results.

• provided no indication of the significance or difficulty of the problems.
  The significance and difficulty of a problem, with respect to the current state-of-the-art in ATP systems, is hard to assess by newcomers to the field. Existing test problems are often not adequate anymore (e.g., Schubert's Steamroller [Sti86]), while others might be solvable only with specialized techniques (e.g., LIM+ [Ble90]), and therefore are much too hard to start with.

• were inconsistent in their presentation of equally named problems.
  Copies and variants of the same "original" problem existed in different collections. This meant that unambiguous identification of problems, and therefore a clear interpretation of performance figures for given problems, was difficult.

• were usually undocumented.
  It was hard to obtain information on problem semantics, the original problem source, and the particular style of axiomatization. This also contributed to the problem of unambiguous problem identification.

• were almost always unserviced.
  Collections did not provide a mechanism for adding new problems or correcting errors in existing problems, and could not be used to electronically distribute new and corrected problems to the ATP community. This in turn perpetuated the use of old and erroneous problems.

• provided no guidelines for their use.
  Quite often, inadequate system evaluations were performed. As a consequence, results that provided little indication of the system properties were reported.

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:

• is easy to discover and obtain.
  Awareness of the TPTP is assured by extensive formal and informal announcements. The TPTP is available online, and is thus easily available to the research community.

• is easy to use.
  Problems are presented in a specifically designed, easy to understand format. Automatic conversion to other known formats is also provided, thus eliminating the necessity for any other transcription.

• spans a diversity of subject matters.
  This reduces biases in the development and testing of ATP systems, which arise from the use of a limited scope of problems. It also provides an overview of the domains in which ATP systems are used.

• is large enough for statistically significant testing.
  In contrast to common practice, an ATP system should be evaluated over a large number of problems, rather than a small set of judiciously selected examples. The large size of the TPTP makes this possible.

• is comprehensive.
  The TPTP contains most problems known to the community. There is no longer a need to look elsewhere.

• is up-to-date.
  As new problems appear in the literature and elsewhere, they are added to the TPTP as soon as possible.

• is independent of any particular ATP system.
  The problems are arranged so as to be modular and human-readable, rather than arranged for a particular ATP system.

• contains problems varying in difficulty, with a difficulty rating for each problem.
  The difficulty of problems in the TPTP ranges from very simple problems through to open problems. This allows all interested researchers, from newcomers to experts, to rely on the same problem library. The difficulty ratings provided with each problem are important for several reasons:

  1. It simplifies problem selection according to the user's intention.

  2. It allows the quality of an ATP system to be judged.

  3. Over the years, changes in the problem ratings will provide an indicator of the advancement in ATP.

• provides statistics for each problem and for the library as a whole.
  This provides information about the syntactic nature of the problems.

• has an unambiguous naming scheme.
  This provides unambiguous problem reference, and makes the comparison of results meaningful.

• is well structured and documented.
  This allows effective and efficient use of the library. Useful background information, such as an overview of ATP application domains, is provided.

• documents each problem.
  This contributes to the unambiguous identification of each problem.

• provides a mechanism for adding new problems.
  The TPTP contains standard axiomatizations that can be used in new problems. This simplifies the collection of new problems. A template is provided for submission of new problems. The TPTP is thus a channel for making new problems available to the community, in a simple and effective way.

• provides a mechanism for correcting errors in existing problems.
  All errors, noticed by the developers or reported by users, are corrected. Patched TPTP releases are made regularly.

• provides guidelines for its use in evaluating ATP systems.
  A standard library of problems together with evaluation guidelines makes reported results meaningful and reproducible by others. This will in turn simplify and improve system comparisons, and allow ATP researchers to accurately gauge their progress.

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

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:

• 15888 abstract problems, which result in 25775 ATP problems (due to alternative presentations and problem generators).

• 25628 problems in classical logic, and 147 problems in non-classical logic

• 20172 problems with equality

• 3549 THF abstract problems, which result in 5042 THF ATP problems, of which ??? are DHF problems and ??? are NHF problems

• 2439 TFF abstract problems, which result in 3297 TFF ATP problems, of which 436 are TXF problems and ??? are NXF problems

• 6033 FOF abstract problems, which result in 9091 FOF ATP problems

• 6312 CNF abstract problems, which result in 8345 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 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 and the numbers of abstract problems, problems, and generic problems in each domain are shown in the TPTP document OverallSynopsis:

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:

• AGT Agents.
  An agent is an autonomous software component of a computer program, typically designed to act intelligently and communicate with other agents.
  Indices: DDC 006.3; MSC 68T35.
  References: General [RN95]; ATP --.

• ALG Algebra.
  Algebra is a branch of mathematics concerning the study of structure, relation, and quantity. An algebra is a set with a system of operations defined on it.
  Indices: DDC 512; MSC 06XX, 20XX.
  References: General [Bou89, BM65, BB70]; ATP --.

• ANA Analysis.
  Analysis is a branch of mathematics concerned with functions and limits. The main parts of analysis are differential calculus, integral calculus, and the theory of functions.
  Indices: DDC 515; MSC 26XX.
  References: General [Ros90]; ATP [Ble90].

• ARI Arithmetic.
  Arithmetic problems that do arithmetic computations (but do not reason about arithmetic - see the NUM domain).
  Indices: DDC 513; MSC 97FXX.
  References: General [Hig10]; ATP [Sim86].

• BIO Biology.
  Biology is a natural science concerned with the study of life and living organisms, including their structure, function, growth, evolution, distribution, and taxonomy.
  Indices: DDC 570; MSC 92XX.
  References: General [RU+13]; ATP [CC+13, CDI13].

• BOO Boolean Algebra.
  A Boolean algebra is a set of elements with two binary operations that are idempotent, commutative, and associative. These operations are mutually distributive, there exist universal bounds 0, 1, and there is a unary operation of complementation.
  Indices: DDC 511.324, 512.89; MSC 06EXX.
  References: General [Whi61, BM65, BB70]; ATP --.

• CAT Category Theory.
  A category is a mathematical structure together with the morphisms that preserve this structure.
  Indices: DDC 512.55; MSC 18XX.
  References: General [Mac71]; ATP [MOW76].

• COL Combinatory Logic.
  Combinatory logic is about applying one function to another. It can be viewed as an alternative foundation of mathematics (or, due to its Turing-completeness, as a programming language). More formally, it is a system satisfying two combinators and satisfying reflexivity, symmetry, transitivity, and two equality substitution axioms for the function that exists implicitly for applying one combinator to another.
  Indices: DDC 510.101; MSC 03B40.
  References: General [CF58, CHS72, Bar81]; ATP [WM88].

• COM Computing Theory.
  Computing theory is a subfield of computer science dealing with theoretical issues such as decidability (whether or not a given problem admits an algorithmic solution), completeness (does an algorithm always find a solution if one exists?), correctness (are only solutions produced?), and computational complexity (the resource requirements of algorithms).
  Indices: DDC 004-006; MSC 68XX.
  References: General [HU79]; ATP --.

• CSR Commonsense Reasoning.
  Commonsense reasoning is the branch of artificial intelligence concerned with replicating human thinking. There are several components to this problem, including: developing adequately broad and deep commonsense knowledge bases; developing reasoning methods that exhibit the features of human thinking, including the ability to reason with knowledge that is true by default, the ability to reason rapidly across a broad range of domains, and the ability to tolerate uncertainty in your knowledge; developing new kinds of cognitive architectures that support multiple reasoning methods and representations.
  Indices: DDC 121.3; MSC 68TXX.
  References: General [Sha97]; ATP [Lif95, McC59, SME04]

• DAT Data Structures.
  A data structure is a particular way of storing and organizing data in a computer so that it can be used efficiently.
  Indices: DDC 005.73; MSC 68P05.
  References: General [AHU87]; ATP --.

• FLD Field Theory.
  A field is a ring (see below) in which the * operation is commutative, and for which there is an identity element in G, and for which each non-identity element of G has an inverse in G.
  Indices: DDC 512.32; MSC 12XX.
  References: General [Ada82]; ATP [Dra93].

• GEG Geography.
  Geography is the study of the Earth and its lands, features, inhabitants, and phenomena.
  Indices: DDC 910; MSC 91C99.
  References: General [NGS99]; ATP --.

• GEO Geometry.
  Geometry is a branch of mathematics that deals with the measurement, properties, and relationships of points, lines, angles, surfaces, and solids.
  Indices: DDC 516; MSC 51.
  References: General [Tar51, Tar59]; ATP [Qua92].

• GRA Graph Theory.
  A graph consists of a finite non-empty set of vertices together with a prescribed set of edges, each edge connecting a pair of vertices.
  Indices: DDC 510.09; MSC 05CXX, 68R10.
  References: General [Har69, BB70]; ATP --.

• GRP Group Theory.
  A group is a set G and a binary operation +:GxG -> G which is associative, and for which there is an identity element in G, and for which each element of G has an inverse in G.
  Indices: DDC 512.2; MSC 20
  References: General [Bou89, BM65]; ATP [MOW76].

• HAL Homological Algebra.
  Homological algebra is an abstract algebra concerned with results valid for many different kinds of spaces. Modules are the basic tools used in homological algebra.
  Indices: DDC 512.55; MSC 18XX.
  References: General [Wei94]; ATP --.

• HEN Henkin Models.
  Henkin models provide a generalized semantics for higher order logics. This leads to a larger class of models and, as a consequence, fewer true sentences. However, in contrast to standard semantics, complete and correct calculi can be found.
  Indices: DDC 160; MSC 03CXX.
  References: General [Hen50, Leb83]; ATP --.

• HWC Hardware Creation.
  Computer hardware is created by inter-connecting logic gates. Hardware creation is used to form a circuit that will transform given input patterns to required output patterns.
  Indices: DDC 621.395; MSC 94CXX.
  References: General [Hay93]; ATP [WW83].

• HWV Hardware Verification.
  Hardware verification is used to ensure that a previously designed circuit performs the desired transformation of input patterns to required output patterns. One approach is to check the performance of the circuit for every possible combination of given inputs. Other techniques are also used.
  Indices: DDC 621.395; MSC 94CXX.
  References: General [Hay93]; ATP [Woj83].

• ITP Interactive Theorem Proving.
  An interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
  Indices:
  References: General [Wie06, Geu09]; ATP [Urb06, BG+19].

• KLE Kleene Algebra.
  A Kleene Algebra is a bounded distributive lattice with an involution satisfying De Morgan's laws, and the inequality x ∧ x' ≤ y ∨ y'. Alternatively, a Kleene Algebra is an algebraic structure that generalizes the operations known from regular expressions.
  Indices: DDC 512.74; MSC 06A99
  References: General [Koz90, BMS03]; ATP [HS07].

• KRS Knowledge Representation.
  Knowledge Representation is concerned with writing down descriptions that can be manipulated by a machine.
  Indices: DDC 006.3; MSC 68T30.
  References: General [BL85, CM87]; ATP --.

• LAT Lattice Theory.
  A lattice is a set of elements, with two binary operations which are idempotent, commutative, and associative, and which satisfy the absorption law.
  Indices: DDC 512.865; MSC 06BXX.
  References: General [BM65]; ATP [McC88].

• LCL Logic Calculi.
  A logic calculus defines axioms and rules of inference that can be used to prove theorems. Indices: DDC 511.3; MSC 03XX. References: General [Luk63]; ATP [MW92].

• LDA Left Distributive Algebra.
  LD-algebras are related to large cardinals. Under a very strong large cardinal assumption, the free-monogenic LD-algebra can be represented by an algebra of elementary embeddings. Theorems about this algebra can be proven from a small number of properties, suggesting the definition of an embedding algebra.
  Indices: DDC 512; MSC 20N02, 03E55, 08B20
  References: General --; ATP [Jec93].

• LIN Linear Algebra.
  Linear algebra is the branch of mathematics concerning vector spaces and linear mappings between such spaces. Indices: DDC 512.5; MSC 15Axx.
  References: General [Poo10]; ATP --.

• MED Medicine.
  The science of diagnosing and treating illness, disease, and injury.
  Indices: DDC 610; MSC --.
  References: General [LH+01]; ATP [HLB05].

• MGT Management.
  Management is the study of systems, and their use and production of resources.
  Indices: DDC 302-303; MSC 90XX.
  References: General --; ATP [PM94, PB+94].

• MSC Miscellaneous.
  A collection of problems which do not fit well into any other domain.

• MVA MV Algebras.
  An MV algebra is an algebraic structure with a binary "plus" operation, a unary "negate" operation, and the constant 0, satisfying certain axioms. Indices: DDC 512; MSC 03G20
  References: General [Mun11, GT75]; ATP --.

• NLP Natural Language Processing.
  Natural language processing considers the automated generation and comprehension of languages used by humans.
  Indices: DDC 006.3; MSC 68T50
  References: General [Obe89, GWS86]; ATP [Bos00].

• NUM Number Theory.
  Number theory is the study of integers and their properties.
  Indices: DDC 512.7; MSC 11.
  References: General [HW92]; ATP [Qua92].

• PHI Philosophy.
  Philosophy is the study of general and fundamental problems, such as those connected with reality, existence, knowledge, values, reason, mind, and language.
  Indices: DDC 100; MSC -
  References: General [TE99]; ATP -.

• PLA Planning.
  Planning is the process of determining the sequence of actions to be performed by an agent, to reach a specified desired state from a specified initial state.
  Indices: DDC 006.3; MSC 68T99.
  References: General [AK+91]; ATP [Pla81, Pla82].

• PRD Products.
  A product is anything that can be offered to a market that might satisfy a want or need.
  Indices: DDC 658.5; MSC 90B50.
  References: General [KA+06]; ATP --.

• PRO Processes.
  Process information includes production scheduling, process planning, workflow, business process reengineering, simulation, process realization process modeling, and project management.
  Indices: DDC 670; MSC 93-XX.
  References: General [Sch99]; ATP [Rei01, BG05].

• PUZ Puzzles.
  Puzzles are designed to test the ingenuity of humans.
  Indices: DDC 510, 793.73; MSC --.
  References: General [Car86, Smu78, Smu85]; ATP --.

• QUA Quantales.
  Quantales are partially ordered algebraic structures that generalize locales (point free topologies) as well as various lattices of multiplicative ideals from ring theory and functional analysis. Quantales are sometimes referred to as complete residuated semigroups.
  Indices: DDC 512; MSC 06F07.
  References: General [Mul01, Con71]; ATP --.

• RAL Real Algebra.
  Real algebra is the study of "real" objects such as real rings, real places and real varieties. Indices: DDC 512; MSC 13J30
  References: General [Lam84]; ATP --.

• REL Relation Algebra.
  A relation algebra is a residuated Boolean algebra supporting an involutary unary operation called converse. The motivating example of a relation algebra is the algebra 2^X^2 of all binary relations on a set X, with RoS interpreted as the usual composition of binary relations.
  Indices: DDC 512; MSC 03G15, 06D99
  References: General [SS93, Mad06]; ATP [HS08].

• RNG Ring Theory.
  A ring is a group (see above) in which the binary operation is commutative, with an associative and distributive operation *:GxG -> G for which there is an identity element in G.
  Indices: DDC 512.4; MSC 16.
  References: General [Bou89, BB70]; ATP [MOW76].

• ROB Robbins Algebra.
  The Robbins Algebra domain revolves around the question "Is every Robbins algebra Boolean?". Most of the problems in this domain identify conditions that make a near-Boolean algebra Boolean.
  Indices: DDC 512; MSC 03G15.
  References: General [HMT71]; ATP [Win90].

• SCT Social Choice Theory.
  Social choice theory is a theoretical framework for measuring individual interests, values, or welfares as an aggregate towards collective decision.
  Indices: DDC 330.1; MSC -.
  References: General [Arr63]; ATP [Nip09].

• SET, SEU, and SEV Set Theory.
  Classically, a set is a totality of certain definite, distinguishable objects of our intuition or thought - called the elements of the set. Due to paradoxes that arise from such a naive definition, mathematicians now regard the notion of a set as an undefined, primitive concept [How72].
  Indices: DDC 511.322, 512.817; MSC 03EXX, 04XX.
  References: General [Neu25, Qui69]; ATP [Qua92].

• SWB Semantic Web.
  Semantic Web is a group of methods and technologies to allow machines to understand the meaning "or "semantics" of information on the World Wide Web.
  Indices: DDC ??.?; MSC --.
  References: General [BHL01]; ATP [HV06].

• SWC Software Creation.
  Software creation is used to form a computer program that meets given specifications.
  Indices: DDC 005.1; MSC 68N30.
  References: General --; ATP --.

• SWV and SWW and SWX Software Verification.
  Software verification formally establishes that a computer program does the task it is designed for.
  Indices: DDC 005.14; MSC 68Q60.
  References: General --; ATP [WO+92, MOW76].

• SYN and SYO and SYP Syntactic.
  Syntactic problems have no obvious semantic interpretation.
  Indices: DDC --; MSC --.
  References: General [Chu56]; ATP [Pel86].

• TIM Time.
  Time is the continuous progression of existence that occurs in an apparently irreversible succession from the past, through the present, and into the future. Indices: DDC 115, 529, 389.17; MSC --.
  References: General [Haw88, Har11]; ATP [All83, AH89].

• TOP Topology.
  Topology is the study of properties of geometric configurations (e.g., point sets) which are unaltered by elastic deformations (homeomorphisms, i.e., functions that are 1-1 mappings between sets, such that both the function and its inverse are continuous).
  Indices: DDC 514; MSC 54.
  References: General [Kel55, Mun75]; ATP [WM89].

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 TPTP4X or TPTP2X 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 this scheme: 

DDDNNNFV[.SSS].T

• DDD - Domain name acronym.

• NNN - Abstract problem number. It is unique within the domain.

• F - Form. ^ for DHF, THF and NHF, _ for TXF, TFF, and NXF, + for FOF, and - for CNF.

• V - Version number. It differentiates between different versions of the abstract problem.

• SSS - Size parameter(s). This is optional (as indicated by the []s).  It occurs for problems that come in various sizes, e.g., N-queens.

• T - File name extension. p for problem files, ax for axiom files, and g for generator files.

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 or set of axioms. 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. For axioms files the version number 0 is used for a base axiomatisation, with higher version numbers used for axiom sets that augment the base axiomatisation. 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, size 2. Similarly, the file CAT001-0.ax contains the basic category theory axiomatization number 1.

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.

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}[-+^_][0-9][0-9]*\.ax".

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 TPTP4X and TPTP2X 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 below:

%--------------------------------------------------------------------------

% File     : GRP194+1 : TPTP v9.3.1. 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.26 v9.3.0, 0.15 v9.1.0, 0.18 v9.0.0, 0.19 v8.1.0, 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 :

%--------------------------------------------------------------------------

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, one of:

• empty. Indicates that the axiomatization is standard, i.e., it is complete and has had no lemmas added (it might be redundant).

• Especial. Indicates that the axiomatization does not capture any established theory.

• Biased. Indicates that the axiomatization is designed specifically to be suited or ill-suited to some ATP system, calculus, or control strategy.

• Incomplete. Indicates that the axiomatization is incomplete.

• Reduced > Complete. Indicates that an existing standard axiomatization has had axioms removed, and the result is complete. The existing axiomatization is necessarily redundant.

• Reduced > Incomplete. Indicates that an existing standard axiomatization has had axioms removed, and the result is non-standard due to incompleteness.

• Augmented. Indicates that an existing standard axiomatization has had lemmas added, and the result is non-standard due to redundancy.

• Reduced & Augmented > Complete. Indicates that an existing standard axiomatization has had axioms removed and lemmas added, and the result is complete.

• Reduced & Augmented > Incomplete. Indicates that an existing standard axiomatization has had axioms removed and lemmas added, and the result is non-standard due to incompleteness.

• Incomplete > Reduced > Incomplete. Indicates that an existing incomplete axiomatization has had axioms removed, and the result is non-standard due to incompleteness.

• Incomplete > Augmented > Complete. Indicates that an existing incomplete axiomatization has had axioms added, and the result is complete.

• Incomplete > Augmented > Incomplete. Indicates that an existing incomplete axiomatization has had lemmas added, and the result is non-standard due to incompleteness.

• Incomplete > Reduced & Augmented > Complete. Indicates that an existing incomplete axiomatization has had axioms removed and lemmas added, and the result is complete.

• Incomplete > Reduced & Augmented > Incomplete. Indicates that an existing incomplete axiomatization has had axioms removed and lemmas added, and the result is non-standard due to incompleteness.

• Especial > Reduced > Especial. Indicates that an especial axiomatization has had axioms removed, and the result remains especial.

• Especial > Augmented > Especial. Indicates that an especial axiomatization has had axioms added, and the result remains especial.

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 initially were:

• ANL - the Argonne National Laboratory library [ANL]

• OTTER - the collection distributed with the Otter ATP system [McC98]

• Quaife - Art Quaife's collection of set theory (based) problems [Qua92]

• ROO - the problems used to test the ROO ATP system [LM92]

• SPRFN - the collection distributed with the SPRFN ATP system [SPRFN]

• TPTP - the problem first ever appeared in the TPTP

• SETHEO - the collection used to test the SETHEO ATP system [LS+92]

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 a dash 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.

• Theorem - Every model of the axioms (and other non-conjecture formulae, e.g., hypotheses and lemmas), and there are some such models, is a model of all the conjectures.

• ContradictoryAxioms - There are no models of the axioms (and other non-conjecture formulae, e.g., hypotheses and lemmas).

• CounterSatisfiable - Some models of the axioms (and there are some) are models of the negation of at least one of the conjectures.

• Unsatisfiable - There are no conjectures, and no interpretations are models of the axioms.

• Satisfiable - There are no conjectures, and some interpretations are models of the axioms.

• Unknown - The problem has never been solved by an ATP system.

• Open - The abstract problem has never been solved.

For CNF problems it is one of:

• Unsatisfiable - No interpretations are models of the clauses.

• Satisfiable - Some interpretations are models of the clauses.

• Unknown - The problem has never been solved by an ATP system.

• Open - The abstract problem has never been solved.

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 (items can be omitted if there are none):

• the numbers of formulae, unit formulae, type formulae, definition formulae

• the numbers of atoms, equality atoms, connective atoms

• the maximal and average number of atoms in a formula

• the number of global definitions

• the numbers of logical connectives, each logical connective

• the maximal and average formula depth

• the numbers of tuples, if-then-else formulae, and let-in formulae

• the numbers of arithmetic formulae, atoms, terms, numbers, and variables

• the numbers of types, user types, arithmetic types, datatypes, codatatypes

• the numbers of type declarations, polymorphic type declarations, dependent type declarations

• the numbers of type connectives, each type connective

• the numbers of distinct (non-variable) symbols, user symbols, constant symbols, the arity range of the symbols, typed equality constants

• the numbers of uses of the Π, Σ, ε, ι constants

• the numbers of distinct variables, lambda quantifications, universal quantifications, existential quantifications, typed variables, Π, Σ, ε, and ι binders

The measures for TFF problems are (items can be omitted if there are none):

• the numbers of formulae, unit formulae, type formulae, definition formulae

• the numbers of atoms, equality atoms

• the maximal and average number of atoms in a formula

• the number of global definitions

• the numbers of logical connectives, each logical connective

• the maximal and average formula depth

• the maximal and average term depth

• the numbers of extended terms, nested formulae, boolean variables

• the numbers of tuples, if-then-else formulae, and let-in formulae

• the numbers of arithmetic formulae, terms, numbers, and variables

• the numbers of types, user types, arithmetic types, datatypes, codatatypes

• the numbers of type declarations, polymorphic type declarations

• the numbers of type connectives, each type connective

• the numbers of distinct predicates, user predicates, propositions, and the arity range of the predicates

• the numbers of distinct function, user functions, constants, and the arity range of the functions

• the numbers of distinct variables, universal quantifications, existential quantifications, typed variables, Π and Σ binders

The measures for FOF problems are (items can be omitted if there are none):

• the numbers of formulae, unit formulae, definition formulae

• the numbers of atoms, equality atoms

• the number of global definitions

• the numbers of logical connectives, each logical connective

• the maximal and average formula depth

• the maximal and average term depth

• the numbers of distinct predicates, user predicates, propositions, and the arity range of the predicates

• the numbers of distinct function, user functions, constants, and the arity range of the functions

• the numbers of distinct variables, universal quantifications, existential quantifications

The measures for CNF problems are (items can be omitted if there are none):

• the numbers of clauses, unit clauses, non-Horn clauses, range restricted clauses

• the numbers of literals, equality literals, negative literals

• the maximal and average clause size

• the number of global definitions

• the maximal and average term depth

• the numbers of distinct predicates, user predicates, propositions, and the arity range of the predicates

• the numbers of distinct function, user functions, constants, and the arity range of the functions

• the numbers of distinct variables, singletons

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 the problems are reasonably homogeneous with respect to ATP systems' performances on the problems. SPCs are used for calculating the difficulty rating [SS01], and for recommending systems to use on problems [SS99]. The characteristics used to build the SPCs are:

• The form of the problem: DH1, DH0, NH0, TH1, TH0, NX0, TX1, TX0, TF1, TF0, FOF, CNF

• The known or expected logical (SZS) status: THM (theorem), CAX (contradictory axioms), CSA (countersatisfiable), UNS (unsatisfiable), SAT (satisfiable), UNK (unknown), OPN (open)

• The effective order of the logic for FOF and CNF problems: PRP (propositional), EPR (effectively propositional), RFO (really first-order)

• The amount of equality in the problem: EQU (with equality), SEQ (some, but not only, equality), PEQ (pure equality), UEQ (unit equality), NUE (non-unit pure equality), NEQ (no equality)

• The amount of arithmetic for THF and TFF problems: ARI (with arithmetic) NAR (no arithmetic)

• The use of (co)datatypes: DAT (with (co)datatypes), NDT (no (co)datatypes)

• Horness (for some CNF problems): HRN (Horn), NHN (non-Horn)

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 generated 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]).

%--------------------------------------------------------------------------

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 TPTP4X and TPTP2X 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 TPTP Language for Formulae (a separate web site)

• Overview

• Annotated Formulae

• Type System

• Arithmetic

• Non-classical

Physical Organization

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

• Problems - The problem files directory, with subdirectories for each domain. The domain name abbreviations are used as subdirectory names. The subdirectories contain the problem files.

• Axioms - The axiom files directory.

• Generators - The generator files directory.

• TPTP2X - The directory containing the TPTP2X utility.

• Scripts - A directory containing the TPTP4X and TPTP2T utilities (the directory is called "Scripts" because originally it was planned to put shell scripts there, but things changed).

• Documents - A directory containing documents that relate to the TPTP:

  • ReadMe - General information about the TPTP.

  • History - A history of the changes made to the TPTP up to the current release.

  • ProblemList - A list of all the abstract problems in the TPTP, giving their names, number of THF, TFF, FOF, and CNF versions, and one-line descriptions.

  • AxiomList - A list of the axiomatizations in the TPTP, giving their names, number of THF, TFF, FOF, and CNF specializations, and one-line descriptions.

  • GeneratorList - A list of the generic problems in the TPTP, giving their names, number of FOF and CNF versions, and one-line descriptions. For each version the constraints that determine the permissible sizes, and the TPTP sizes, are given.

  • ReverseIndex - An index from existing known names for problems to their TPTP file names.

  • Bibliography.bib - The BibTeX file containing references for all material cited in the TPTP.

  • ProblemAndSolutionStatistics - Lists all the problems in the TPTP, giving statistics about the problems and information about ATP systems' performances on the problems. The fields are listed and explained below.

  • THFSynopsis, TFFSynopsis, FOFSynopsis, and CNFSynopsis - Statistics on the THF, TFF, FOF, and CNF problems in the TPTP, and charts showing the structure of the TPTP problem domains.

  • OverallSynopsis - Statistics on the overall TPTP, and a chart showing the structure of the TPTP problem domains.

  • VerySimilarProblemsLists - A directory containing lists of very similar problems. Problems are considered to be "very similar" if:

    • They have many formulae in common, e.g., when the same axioms are used for very many conjectures.

    • They have very similar characteristics, e.g., when the problems have been created using different parameters in some automated process.

  • SyntaxBNF - BNF of the TPTP syntax

  • Template - A template for submitting new TPTP problems.

• The files in the Documents directory contain comprehensive online information about the TPTP. They summarize much of the information contained in this report, in specific files. Their format provides quick access to the data, using standard system tools (e.g., grep, awk).
  The fields in the problem lines of the ProblemAndSolutionStatistics file are:

  • Problem name

  • Frm - one of THF, TFF, FOF, or CNF.

  • SZS - the SZS status (using the SZS ontology)

  • Rtng - the problem's difficulty rating.

  • SPC - the problem's Specialist Problem Class

  • FmlCls - the number of formulae/clauses

  • UnitF - the number of unit formulae/clauses

  • TypeF - the number of type declarations (THF and TFF)

  • Atoms - the number of atoms

  • EquAts - the number of equality atoms

  • Conns - the number of logical connectives

  • FOOLs - the number of FOOL logic atoms/terms (TXF)

  • Ariths - the number of arithmetic atoms/terms (THF and TFF)

  • Types - the number of Types (THF and TFF)

  • Symbls - the number of distinct non-variable symbols

  • Preds - the number of distinct predicate symbols

  • Arity - the arity range of predicate symbols

  • Funcs - the number of distinct function symbols

  • Arity - the arity range of function symbols

  • Vars - the number of distinct variables

  • ^ - the number of lambda quantified variables (THF)

  • ! - the number of universally quantified variables

  • ? - the number of existentially quantified variables

  • !> - the number of lambda-pi quantified (polymorphic) variables (TH1 and TF1)

  • {.} - the number of mono-modal non-classical connectives

  • {#} - the number of multi-modal non-classical connectives

  • DataT  - the number of datatypes

  • CoDaT- the number of codatatypes

• The fields in the solution lines of the ProblemAndSolutionStatistics file are:

  • System name

  • Res - the result established (using the SZS ontology)

  • RsT - the CPU time taken to get the result

  • Out - the output claimed (using the SZS ontology)

  • SZO - the output detected during analysis (it might be different from what was claimed, e.g., if the output was not in TPTP format)

  • DDpDSz - if the output is some form of derivation then the derivation depth; if the output is a finite domain model then the domain size

  • Leaves - if the output is a derivationthe number of leaves

  • All other fields as for a problem.

Utilities

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 described below, and offers some of the same functionality, and some extra functionality. TPTP4X is written in C, and is thus faster than TPTP2X.

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

• -q<quietness> - control amount of output (1)

• -d<directory> - output directory (stdout)

• -f<format> - output format (tptp)

  • tptp - long tptp format

  • tptp:short - short tptp format

• -t<transform> - transform the formulae (none)

  • add_equality - adds all axioms of equality

  • add_equality:rstfp - adds selected axioms of equality

  • fofify -V - make universally quantified fof

  • fofify:! -V - make universally quantified fof

  • noint - rename integers to constants

  • aritize - make function and predicate names unique by arity

  • dequote - make function and predicate names unquoted

  • numbernamesN - add N digit extension to formula names

  • uniquenamesN - add N digit extension to duplicate formula names

  • randomize - randomize formulae and their order

  • negate_conjectures - negate all conjectures

• -u<user> - user type (human)

  • human - pretty printed with indenting

  • machine - one line per formula

• -r<delay> - delay between formula output (none)

  • fixed - fixed delay of that many milliseconds

  • min:max - random delay from min to max milliseconds

• -V - allow free variables (no)

• -N - allow duplicate formula names (no)

• -x - expand includes (no)

• -c - clean away non-logicals (no)

• -w - warnings (no)

• -z - SZS ontology status output (no)

• -v - print version number

• -h - print this help

The TPTP2T Utility

The TPTP2T utility selects lines from the ProblemAndSolutionStatistics file, by problem and solution characteristics. The script is written in perl, and uses mawk to extract the lines from the file. TPTP2T can also be used online.

Usage: tptp2T [-f <FileName>] [-q1 | -q2 | -q3] [-pp | -ps | -pps]  <Constraints>

Options (before the constraints, in any order):

• -f <FileName> - Consider only the problems listed in the file (one per line, name first)

• -q1 - Progress ticks while searching, plus headers and final count

• -q2 - Headers and final count (default)

• -q3 - Matching lines only

• -pp - Print problem lines (default if there is no System constraint)

• -ps - Print solution lines

• -pps - Print both (default if there is a System constraint)

• -h, --help - Print this help

Constraints

A query is a boolean expression of constraints:

• Constraints next to each other must all hold ("and" may also be written).

• A or B - Either holds. "and" binds tighter than "or".

• { ... } - Grouping, e.g., Form FOF { Status Theorem or Status Unsatisfiable }

• -C  - Negates the constraint C, e.g., -Equality

• -{ ... }  - Negates a group

• Constraint names are case-insensitive; values (Form, Status, Result, Output) are as shown.

• Bounds "<Lo> <Hi>" are numbers, inclusive; "-" means no bound, e.g., Rating 0.5 -

• A statistic recorded as "-" (unknown) never satisfies bounds.

Problem constraints

• Domains <D>[,<D>...]  - The problem is in one of the domains, e.g., Domains ALG,ANA (space separated also works: Domains ALG ANA)

• Form <F> - The logical form, from the SPC. <F> is one of DH0 DH1 TH0 TH1 TX0 TX1 NH0 NH1 NX0 NX1 TF0 TF1 FOF CNF. ANY matches all. *F matches *0 and *1

• Status <S> - The SZS status: Theorem (THM), ContradictoryAxioms (CAX), FiniteTheorem (FTH), CounterSatisfiable (CSA), Satisfiable (SAT), Unsatisfiable (UNS), FinitelySatisfiable (FSA), FinitelyUnsatisfiable (FUN), Unknown (UNK), Open (OPN). Use either the long or short form, but note that capitalisation is relevant.

• Rating <Lo> <Hi> - The difficulty rating, 0.00 to 1.00

• Equality - The problem has equality atoms

• PureEquality - All the atoms are equality atoms

• UnitEquality - CNF, pure equality, and every clause is a unit

• Arithmetic - The problem has arithmetic symbols

• Propositional - All predicates have arity 0

• PredicateArity <Lo> <Hi> - The smallest predicate arity is >= Lo and the largest <= Hi

• FunctionArity <Lo> <Hi> - The smallest function arity is >= Lo and the largest <= Hi, e.g., FunctionArity 0 0 = no functions (a problem with no functions counts as arity 0)

• Counts: each is true if the count is > 0, or with bounds, if the count is within them, e.g., Variables, -Lambdas, Formulae 100 -, Datatypes 1 1. Options are:

  • Formulae - Number of annotated formulae

  • UnitFormulae - Number of unit formulae

  • TypeFormulae - Number of type formulae

  • Atoms - Number of atoms in the formulae

  • EqualityAtoms - Number of (in)equality atoms in the formulae

  • Connectives - Number of connectives in the formulae

  • FOOLs - Number of FOOL (that make a problem TXF) constructs in the formulae

  • Arithmetics - Number of arithmetic constructs in the formulae

  • Types - Number of types used in the formulae

  • Symbols  - Number of distinct symbols in the formulae (for THF that does not differentiate between predicates and functions)

  • Predicates - Number of distinct predicates in the formulae

  • Functions - Number of distinct functions in the formulae

  • Variables - Number of distinct variables in the formulae

  • Lambdas - Number of lambda quantifications in the formulae

  • Universals - Number of universal quantifications in the formulae

  • Existentials - Number of existential quantifications in the formulae

  • PiUniversals - Number of polymorphic quantifications in the formulae

  • NonClassicalConnectives - Number of mono-modal non-classical connectives used in the formulae

  • MultiModalNCCs - Number of multi-modal non-classical connectives used in the formulae

  • Datatypes - Number of datatypes in the formulae

  • Codatatypes - Number of codatatypes in the formulae

Solution constraints

System <Name> <solution constraints>

True for a problem if one of its solution lines is from a system whose name starts with <Name> (case-insensitive; ANY matches every system) and meets the solution constraints that follow. The set ends at the next System, or at a constraint that is not a solution constraint. -System <Name> means a system whose name does not start with <Name>. To require that no line meets a set, negate it: -{ System <Name> ... }. Sets combine with each other and with problem constraints using and, or, { } and -{ }.

• Result <R> - The SZS result: Theorem (THM), ContradictoryAxioms (CAX), FiniteTheorem (FTH), CounterSatisfiable (CSA), Satisfiable (SAT), Unsatisfiable (UNS), FinitelySatisfiable (FSA), FinitelyUnsatisfiable (FUN), Timeout (TMO), GaveUp (GUP), Error (ERR), Unknown (UNK), Inappropriate (IAP), MemoryOut (MMO), ResourceOut (RSO), Incomplete (INC).  Success (SUC) means any one of Theorem (THM), ContradictoryAxioms (CAX), FiniteTheorem (FTH), CounterSatisfiable (CSA), Satisfiable (SAT), Unsatisfiable (UNS), FinitelySatisfiable (FSA), FinitelyUnsatisfiable (FUN). NoSuccess (NOS) means any one of Timeout (TMO), GaveUp (GUP), Error (ERR), Unknown (UNK), Inappropriate (IAP), MemoryOut (MMO), ResourceOut (RSO), Incomplete (INC). Use either the long or short form, but note that capitalisation is relevant.

• Output <O> - The SZS output: Proof (Prf), Refutation (Ref), CNFRefutation (CRf), Model (Mod), FiniteModel (FMo), Saturation (Sat), Assurance (Ass), None (Non). Proof (Prf) includes Refutation (Ref) and CNFRefutation (CRf).  Model (Mod) includes FiniteModel (FMo), Saturation (Sat). Solution (Sol) means all proofs and models. Use either the long or short form, but note that capitalisation is relevant.

• ResultTime <Lo> <Hi> - The time taken in seconds to establish the result

• SolutionDepth <Lo> <Hi> - The depth of a derivation, or the domain size of a finite model

• SolutionLeaves <Lo> <Hi> - The number of leaves of a derivation

• SolutionFormulae <Lo> <Hi> - The number of formulae in a derivation

• SolutionAtoms <Lo> <Hi> - The number of atoms in a derivation

• Equality - The solution has equality atoms

• Arithmetic - The solution has arithmetic symbols

• Selectivity <Lo> <Hi>  - Leaves/the number of problem formulae

• Girth <Lo> <Hi>  - Leaves/depth in a derivation

Not supported (no data): Horn, NonHorn, RangeRestricted

Examples

• FOF theorems with a rating between 0.5 and 0.9:

       tptp2T Form FOF Status Theorem Rating 0.5 0.9

• CNF problems without equality in the GRP and RNG domains:

       tptp2T Domains GRP,RNG Form CNF -Equality

• THF theorems that Vampire proved in under 10 seconds, with Vampire's solutions:

       tptp2T Form THF Status Theorem System Vampire Result THM ResultTime 0 10

• FOF theorems that E or Vampire proved:

      tptp2T Form FOF System E--- Result THM or System Vampire Result THM

• FOF theorems that Vampire did not prove:

       tptp2T -pp Form FOF Status Theorem -{ System Vampire Result THM }

Getting and Using the TPTP

Obtaining the TPTP

The distribution consists of two files:

• ReadMe contains an overview of the TPTP.

• TPTP-v9.0.0.tgz (879.0 MByte, 9.8 GByte unpacked) contains the library (including a copy of the ReadMe file).

These files are available online.

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.

• The TPTP release number must be stated.

• Each problem must be referenced by its unambiguous syntactic name.

• The problem formulae should, as far as is possible, not be changed in any way. Any changes made (addition, removal, reordering, reformatting, etc.) must be explicitly noted.

• Any information given to the ATP system, other than that in the formulae, must be explicitly noted. All system switches and settings must be recorded. The header information in each problem may not be used by the ATP system without explicit notice.

Abiding by these conditions will allow unambiguous 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 ...

• You find any mistakes in the TPTP.

• You are able to provide further information for a TPTP problem.

• You want to contribute a problem to the TPTP. Please use the problem template that comes with the distribution. Fill in header information as far as possible. Any unambiguous representation will do for the formulae.

• You have any suggestions for improving the TPTP library.

Conclusion

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

The TPTP World is indebted to the following people and organizations who have helped with the construction of the TPTP World.

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, Dan Benanav, Alexander Bentkamp, Christoph Benzmüller, Marc Bezem, Wolfgang Bibel, 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, Stefano Demarchi, Gerard de Melo, Louise Dennis, Samiro Discher, Alexander Dvorsky, Christian Fermüller, Jean-Christophe Filliâtre, Bernd Fischer, Paul Fodor, Deepak Garg, Dario Guidotti, 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, Milene Johns, Ulf Kahlert, Cezary Kaliszyk, Mark Kaminski, Zurab Khasidashvili, Daniel Kuehlwein, Lydia Kondylidou, Boris Konev, Laura Kovacs, Ivan Kossey, Evgeny Kotelnikov, Evgeny Kruglov, Tobias Kuhn, Lars Kulik, Timm Lampert, Rob Lewis, Daniel Li, Di Long Li, Theo Losekoot, Meng Luan, Johan Martensson, Takuya Matsuzaki, Bill McCune, Andreas Meier, Jia Meng, Frederic Mesnard, Esteban Morales, Daham Mohammed Mustafa, Cláudia Nalon, Juan Antonio Navarro Perez, Georg Neis, Jens Otten, Julian Parsert, Andrei Paskevich, Dominique Pastre, Adam Pease, Björn Pelzer, David Plaisted, Larry Paulson, Luca Pulina, Art Quaife, Pedro Quaresma, Florian Rabe, Daniel Ranalter, Silvio Ranise, Thomas Raths, Michael Rawson, Pace Reagan-Smith, Martin Riener, Philipp Rümmer, Teppei Saito, Happy Sariyanto, Alberto Segre, Renate Schmidt, Michael Schneider, Johannes Schoisswohl, Stephan Schulz, Martina Seidl, Ted Sider, John Slaney, Nick Smallbone, Pante Stanica, David Stanovsky, Graham Steel, Alexander Steen, Mark Stickel, Nik Sultana, Hans Svensson, Armando Tacchella, Tanel Tammet, Alwen Tiu, Steven Trac, Thaleia Tsioka, 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, Zsolt Zombori.

For helping with problems and/or pointing out errors: Geoff Alexander, Johan Belinfante, Alexander Bentkamp, Ahmed Bhayat, Nikolaj Bjorner, Woody Bledsoe, Maria Paola Bonacina, Julie Cailler, Heng Chu, Koen Claessen, Ingo Dahn, Morgan Deters, Damien Doligez, Marisol Fernandez, 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, Axel Polaczek, Petr Pudlak, Art Quaife, Dimitris Raptis, Michael Raskin, Thomas Raths, Piotr Rudnicki, Masahiro Sakai, Happy Sariyanto, Michael Schneider, Len Schubert, Stephan Schulz, Johannes Schuster, Simon Schwarz, 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, Martin Desharnais, 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.