| Department of Computer Science University of Miami geoff@cs.miami.edu |
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 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 is such a library. 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.
| A Quick Installation Guide for the TPTP is given in Section Getting and Using the TPTP. Please be sure to read the guidelines for using TPTP problems and presenting results, given in Section Using the TPTP. |
What's New in TPTP v4.0.0 :
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 may 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 may 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.
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 current release of the TPTP library is limited to problems expressed in 1st
order logic.
There are no problems for induction, or for non-classical theorem proving.
However, see Sections Current Activities
and Further Plans for upcoming and planned extensions.
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, and others. The domains are presented and discussed in Section The TPTP Domain Structure.
Sources
The problems have been collected from various sources.
The two principal sources have been 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; smaller numbers of problems have been provided by a
number of further contributors (see the
Acknowledgements).
Releases
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.
Five main fields are defined:
logic, mathematics, computer science, engineering, 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
(see Section
Problem and Axiomatization Naming).
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
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:
Different Axiomatizations
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 may 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 may 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 may be formed by modifying a standard
axiomatization:
the standard axiomatization may be reduced (i.e., axioms are removed) and
the result is an incomplete axiomatization, or it may 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 may 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.
In the TPTP, for each incomplete, redundant, and biased problem, a new version
of the problem with a standard axiomatization is usually created.
Finally, an axiomatization may 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
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 may 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, and a full
description of their use is given in
Section The tptp2X Utility.
For convenience, the TPTP still contains, where they exist, a theorem and
a non-theorem size instance of each generic problem.
The TPTP sizes chosen are non-trivial,
unless the problem remains easy up to sizes that have very large files.
In the latter situation the TPTP size is that used in TPTP v1.2.0.
The statistics in the TPTP documents
Overall synopsis,
FOF synopsis, and
CNF synopsis
take into account these instances of generic problems.
Problem file naming scheme.
The abstract problem numbers within each domain are not always successive.
This is because some numbers have already been allocated to problems that
will be part of a future TPTP release (see
Section The Present).
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.
Axiom file naming scheme.
If a file is ever removed from or renamed in the TPTP, then the 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 full
BNF specification of the problem and axiom file formats is provided
in the Documents directory of the TPTP (see
Section Physical Organization).
The tptp2X utility can be used to convert TPTP files to other known ATP system
formats (see
Section The tptp2X Utility).
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.
The % File field.
The % Domain field.
The % Problem field.
The % Version field.
The second possible differentiation is the status of the axiomatization,
as discussed in Section Problem Versions.
There are 12 possiblities:
The % English field.
The % Refs field.
The % Source field.
The % Status field.
The % Syntax field.
The % Comments field.
The % Bugfixes field.
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 results of parsing the named file are filtered
to retain only those formulae (thus this filter applies to formulae that
may 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 Figure Example include section 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 utility (see
Section The tptp2X Utility).
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 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 start with a $, a ", or a digit.
The defined predicates recognized so far are $true and
$false, with the obvious interpretations, and infix = and
!= for equality and inequality.
The defined functors recognized so far are "distinct object"s,
written in double quotes, and numbers.
A "distinct object" is interpreted as the domain element
in the double quotes.
Numbers are interpreted as themselves (as domain elements).
A consequence of the predefined interpretations is that all different
"distinct object"s and numbers are known to be unequal,
e.g., "Apple" != "Microsoft" and 1 != 2 are implicit axioms.
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 short
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 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.
Types can be constants, the defined type $tType (the type of all
types), or built from types using the type mapping connective >,
which is right associative.
Non-variable symbols can be given a type globally in the formula with
role type, in the same format.
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 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 may be different from the name of the annotated
formula itself, e.g., if an ATP systems reads in 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 FOF formula section, extracted from the problem file
GRP194+1.p, is shown in Figure
Example FOF formulae.
An example of a clause section, extracted from the problem file
GRP039-7.p, is shown in Figure
Example CNF clauses.
An example of a THF formula section, extracted from the problem file
LCL633^1.p, is shown in Figure
Example THF formulae.
Hint: If your command shell complains about too many arguments as a
result of expanding the <TPTPFiles> argument to a too large number
of files, e.g., ~/TPTP/Problems/S*/*.p, place the
<TPTPFiles> argument in 'single quotes', and
tptp2X will do the expansion internally.
Finally an extension to indicate the output format is appended to the file
name. The suffixes for the output formats are:
To record how a tptp2X output file has been formed, the tptp2X parameters
are given in a % Comments field entry of the output file.
Example
Example
Example
?-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.
See Section Using tptp2X for parameter
options.
Note that the TPTP file name is quoted in the query, to form a Prolog atom.
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 Geoff Sutcliffe.
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 Geoff Sutcliffe.
The tptp2T script is written in perl.
tptp2T [-f FileName] [-q1 or -q2 or -q3] [-pp or -ps or -pps] {[-]Constraint {[and/or] [-]Constraint}}
A problem Constraint is selected from:
These files are available online.
prompt> tar xzf TPTP-v4.0.0
.tgz
prompt> cd TPTP-v4.0.0
prompt> ./Scripts/tptp2T_install
prompt> ./TPTP2X/tptp2X_install
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.
Some of the formats cannot cope with certain types of problems, e.g.,
dimacs format is for only propositional CNF problems.
The tptp format simply expands include directives (see
Section Problem Presentation)
in problems, producing files in the TPTP Prolog-style syntax.
tptp2X offers much more than this.
See Section The tptp2X Utility for
a detailed description of the utility, including information on how to
produce output in your own syntax.
Our contact addresses are given on in the title.
Current proposals for extensions to the TPTP include
the TFF syntax for typed FOF problems,
the TPTP format for interpreted integer arithmetic,
and
TPTP standards for answer extraction.
Details of the prosals are online at
http://www.tptp.org, and comments are welcome.
For contributing problems:
Alessandro Armando,
Argonne National Laboratory,
AR Research Group at TU München,
Jaroslav Barta,
Peter Baumgartner,
Bjoern Pelzer,
Dan Benanav,
Christoph Benzmueller,
Marc Bezem,
Woody Bledsoe,
Conrad Bock,
Johan Bos,
Marc Boule,
Chad Brown,
Koen Claessen,
Simon Colton,
Gerard de Melo,
Louise Dennis,
Alexander Dvorsky,
Christian Fermüller,
Bernd Fischer,
Deepak Garg,
Tim Geisler,
Keith Goolsbey,
Jay Halcomb,
John Harrison,
Lifeng He,
Stefan Hetzl,
Thomas Hillenbrand,
Tim Hinrichs,
Peter Hoefner,
Arjen Hommersom,
Ullrich Hustadt,
Thomas Jech,
Mark Kaminski,
Boris Konev,
Laura Kovacs,
Ivan Kossey,
Tobias Kuhn,
Lars Kulik,
Bill McCune,
Andreas Meier,
Jia Meng,
Johan Martensson,
Juan Antonio Navarro Perez,
Georg Neis,
Jens Otten,
Andrei Paskevich,
Dominique Pastre,
Adam Pease,
David Plaisted,
Larry Paulson,
Art Quaife,
Florian Rabe,
Thomas Raths,
Pace Reagan-Smith,
Alberto Segre,
Renate Schmidt,
Stefan Schulz,
Ted Sider,
John Slaney,
David Stanovsky,
Graham Steel,
Mark Stickel,
Hans Svensson,
Tanel Tammet,
Steven Trac,
Josef Urban,
Bob Veroff,
Christoph Weidenbach,
Christoph Wernhard,
Bruno Woltzenlogel Paleo,
Aparna Yerikalapudi,
Jian Zhang.
For helping with problems and/or pointing out errors:
Geoff Alexander,
Johan Belinfante,
Woody Bledsoe,
Maria Poala Bonacina,
Heng Chu,
Koen Claessen,
Ingo Dahn,
Damien Doligez,
Alexander Fuchs,
Matthias Fuchs,
Tim Geisler,
John Harrison,
Thomas Jech,
Konstantin Korovin,
Ivan Kossey,
Harald Ganzinger,
Reinhold Letz,
Ann Lilliestrom,
Thomas Ludwig,
Klaus Mayr,
Bill McCune,
Monty Newborn,
Xumin Nie,
Dominique Pastre,
Jeff Pelletier,
Petr Pudlak,
Art Quaife,
Dimitris Raptis,
Thomas Raths,
Piotr Rudnicki,
Len Schubert,
Alberto Segre,
Guy Shefner,
Andrés Sicard-Ramírez,
Nick Siegel,
John Slaney,
Mark Stickel,
Martin Suda,
Bob Veroff,
Russell Wallace,
TC Wang,
Christoph Weidenbach,
Hantao Zhang.
For support regarding the utilities:
Stefan Berghofer,
Lucas Dixon,
Bernd Fischer,
Alexander Fuchs,
Kal Hodgson,
Max Moser,
Gerd Neugebauer,
Petr Pudlak,
Alex Roederer,
Paul Tarau,
Frank Theiss,
Abdul Sattar,
Andrei Tchaltsev,
Christoph Weidenbach,
Makarius Wenzel,
Jürgen Zimmer.
For general advice and comments:
Serge Autexier,
Reiner Hähnle,
Joe Hurd,
Reinhold Letz,
Selene Makarios,
Jeff Pelletier,
Florian Rabe,
Stephan Schulz,
Mark Stickel,
Allen van Gelder,
Russell Wallace.
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.
The Domain Structure of the TPTP.
Logic
Combinatory logic
COL
Logic calculi
LCL
Henkin models
HEN
Mathematics
Set theory
SET, SEU, and SEV
Graph theory
GRA
Algebra
Relation algebra
REL
Boolean algebra
BOO
Robbins algebra
ROB
Left distributive
LDA
Lattices
LAT
Kleene algebra
KLE
Groups
GRP
Rings
RNG
Fields
FLD
Homological algebra
HAL
General algebra
ALG
Number theory
NUM
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
Software creation
SWC
Software verification
SWV
Science and Engineering
Hardware creation
HWC
Hardware verification
HWV
Medicine
MED
Processes
PRO
Social sciences
Management
MGT
Geography
GEG
Other
Syntactic
SYN and SYO
Puzzles
PUZ
Miscellaneous
MSC
An agent is an autonomous software component of a computer program,
typicallly designed to act intelligently and communicate with other
agents.
Indices: DDC ???; MSC 68T35.
References:
General
[RN95];
ATP --.
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 --.
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].
A Boolean algebra is a set of elements with two binary operations
which 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 --.
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].
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].
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 --.
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]
A field is 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].
Geometry is the study of the Earth and its lands, features, inhabitants,
and phenomena.
Indices: DDC 910; MSC 91C99.
References:
General
[NGS99];
ATP --.
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].
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 --.
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].
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 --.
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 --.
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].
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].
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].
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 --.
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].
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].
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].
The science of diagnosing and treating illness, disease, and injury.
Indices: DDC 610; MSC --.
References:
General
[LH+01];
ATP
[HLB05].
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].
A collection of problems which do not fit well into any
other domain.
Natural language processing considers the automated generation and
comprehension of languages used by humans.
Indices: DDC 006.3; MSC 68T50
References:
General
[Obe89i,
GWS86];
ATP
[Bos00].
Number theory is the study of integers and their properties.
Indices: DDC 512.7; MSC 11YXX.
References:
General
[HW92];
ATP
[Qua92].
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].
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].
Puzzles are designed to test the ingenuity of humans.
Indices: DDC 510, 793.73; MSC --.
References:
General
[Car86,
Smu78,
Smu85];
ATP --.
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].
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 13XX, 16XX.
References:
General
[Bou89,
BB70];
ATP
[MOW76].
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].
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].
Software creation is used to form a computer program that meets given
specifications.
Indices: DDC ???.?; MSC 68N30.
References:
General --;
ATP --.
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].
Syntactic problems have no obvious semantic interpretation.
Indices: DDC --; MSC --.
References:
General
[Chu56];
ATP
[Pel86].
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 46AXX.
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 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 theorem to be proven,
e.g., different clausal forms of a FOF problem.
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 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 utility
(see Section The 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 (see
Section Using the TPTP).
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 satisfiability may depend on the problem size.
Problem, Generator, 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
Sections 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.
DDD
NNN
F
V
.SSS
.T
DDD - Domain name abbreviation.
The domain names and their abbreviations are listed in
Section
The Domain Structure of the TPTP.
NNN - Abstract problem number.
It is unique within the domain.
F - Form.
- for CNF, + for FOF, and ^ for THF.
V - Version number.
It differentiates between different versions of the abstract
problem, as discussed in
Section Problem Versions.
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.
DDD
NNN
F
V
.TT
DDD - Domain name abbreviation.
The domain names and their abbreviations
are listed in
Section
The Domain Structure of the TPTP.
NNN - Axiomatization number.
It is unique within the domain.
F - Form.
- for CNF, + for FOF, and ^ for THF.
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 ax denotes a file containing axioms
specific to a theory.
An extension eq denotes a file containing equality
substitution axioms for the corresponding theory specific axioms.
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 (see
Section Using the TPTP).
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 given in
Section
Writing your own Problem Generators.
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 v2.2.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.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 unit)
% Number of atoms : 21 ( 4 equality)
% Maximal formula depth : 8 ( 4 average)
% Number of connectives : 13 ( 0 ~ ; 0 |; 6 &)
% ( 1 <=>; 6 =>; 0 <=)
% ( 0 <~>; 0 ~|; 0 ~&)
% Number of predicates : 3 ( 0 propositional; 2-2 arity)
% Number of functors : 5 ( 3 constant; 0-3 arity)
% Number of variables : 15 ( 0 singleton; 14 !; 1 ?)
% Maximal term depth : 3 ( 1 average)
% Comments :
%--------------------------------------------------------------------------
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 identifies the domain, and possibly a subdomain, from which
the problem is drawn (see Section
The TPTP Domain Structure).
The domain corresponds to the first three letters of the problem name.
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.
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 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.
This field provides a full description of the problem, if the one-line
description in the % Problem field is too terse.
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 problems in the TPTP have been
(physically) obtained from a variety of sources, both hardcopy and
electronic. In this field the source of the problem is acknowledged,
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 which have appeared in other problem collections or the literature,
often have names which are known in the ATP community.
This field lists all such names known to us 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 which 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 (see
Section Physical Organization).
This field gives the ATP status of the problem, according to the
SZS problem status ontology.
For THF 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.
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.
This field lists various syntactic measures of the problem's clauses.
The measures for CNF problems are:
the number of clauses,
the number of non-Horn clauses,
the number of unit clauses,
the number of range restricted clauses,
the number of literals,
the number of equality literals,
the maximal and average clause size (measured by number of literals),
the number of distinct predicate symbols,
the number of distinct propositional symbols,
the minimal and maximal predicate symbol arities,
the number of distinct function symbols,
the number of distinct constants,
the minimal and maximal functor arities,
the number of distinct variables,
the number of singleton variables
(variables that appear only once in a clause),
and the maximal and average term depth (with constants and variables having
depth 1).
The measures for FOF problems are:
the number of formulae,
the number if unit formulae,
the number of atoms,
the number of equality atoms,
the maximal and average formula depth,
the number of connectives,
the numbers of each type of connective,
the number of distinct propositional symbols,
the minimal and maximal predicate symbol arities,
the number of distinct function symbols,
the number of distinct constants,
the minimal and maximal functor arities,
the number of distinct variables,
the number of singleton variables,
the numbers of universally and existentially quantified variables,
and the maximal and average term depth.
See Section Inside the TPTP
for a summary of this information over the entire TPTP.
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 (see
Section The tptp2X Utility) then the
tptp2X parameters are given.
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 is shown in
Figure Example include section,
extracted from the problem file GEO146+1.p.
%--------------------------------------------------------------------------
%----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]).
%--------------------------------------------------------------------------
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 fof - formulae in
full 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, conjecture,
negated_conjecture, plain, type, and
unknown.
axioms are accepted, without proof, as a basis for proving
conjectures in FOF and THF problems.
In CNF problems axioms are accepted as part of the set whose
satisfiability has to be established.
There is no guarantee that the axioms of a problem are consistent.
hypothesiss are assumed to be true for a particular problem,
and are used like axioms.
definitions are used to define symbols, and are used like
axioms.
assumptions can be used like axioms, but must be discharged before a
derivation is complete.
lemmas and theorems have been proven from the
axioms, can be used like axioms, but are redundant
wrt the axioms.
theorem is used as the role of proven conjectures,
in output.
A problem containing a lemma or theorem that is not
redundant wrt the axioms is ill-formed.
theorems are more important than lemmas from the
user perspective.
conjectures occur in only FOF and THF problems, and are to all
be proven from the axiom(-like) formulae.
A problem is solved only when all conjectures are proven.
negated_conjectures are formed from negation of a
conjecture, typically in FOF to CNF conversion.
plains have no special user semantics, and can be used like
axioms.
type formulae define the types of symbols globally.
unknowns have unknown role, and this is an error situation.
%--------------------------------------------------------------------------
%----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)) )).
%--------------------------------------------------------------------------
%--------------------------------------------------------------------------
%----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) )).
%--------------------------------------------------------------------------
%------------------------------------------------------------------------------
%----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 ) )).
%------------------------------------------------------------------------------
Physical Organization
The TPTP is physically organized into six subdirectories, as follows:
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).
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.
It is known to run on current versions of
Eclipse,
SICStus,
SWI,
and
YAP
Prolog.
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.
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
-s<Size> is ignored for problem (.p) files.
The transformations are:
The default <Transform> is none.
Details of these algorithms can found in
[SM96].
Note that these transformations do not simplify the resultant
clause set; see the next two transformations for this.
For example, -t rm_equality:stfp would remove symmetry,
transitivity, function substitution, and predicate substitution.
This transformation works only if the equality axiomatization is
complete (i.e., including the axioms of reflexivity, symmetry,
transitivity, function substitution for all functors, and predicate
substitution for all predicate symbols).
The default <Format> is tptp.
'<Otter options>' is a quoted (to avoid
UNIX shell errors), comma separated list of Otter options, which
will be output before the formula lists.
See the Otter Reference Manual and Guide
[McC94]
for details of the available options.
For example,
-f otter:none:'set(auto),assign(max_seconds,5)'
would configure Otter to use its auto mode with a
time limit of 5 seconds.
As the auto mode is commonly used with Otter, the tptp2X
script allows the abbreviation -f otter to specify
-f otter:none:'set(auto),set(tptp_eq),clear(print_given)'.
If no -t parameter is specified then -f otter also
sets -t equality:stfp.
<Cardinality> is the required cardinailty of the model.
<Style> specifies the style of SETHEO clauses to write. It
can be one of:
The default style is sign, i.e., the abbreviation
-f setheo means -f setheo:sign.
A common first use of tptp2X is to convert TPTP problems to another format.
To convert all TPTP problems to another format, the use is
tptp2X -f<Format>, e.g., tptp2X -f otter.
To limit the conversion to one or more domains, the domain names are
specified after the <Format>, e.g.,
tptp2X -f leantap ALG GRP LDA.
If you are a new TPTP user, these are probably the uses that you want
to start with.
The tptp2X Output Files
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.
The suffixes for the transformations are:
Transformation
Suffix
stdfof
+stdfof
clausify:<Algorithm>
+cls_<Algorithm>
simplify
+simp
cnf:<Algorithm>
+cnf_<Algorithm>
propify
+prop
lr
+lr
cr
+cr
clr
+clr
fr
+fr
random
+ran
er
+er
ran_er
+ran_er
add_equality:<Add>
+eq_<Add>
rm_equality:<Remove>
+rm_eq_<Remove>
set_equality:<Set>
+seq_<Set>
to_equality
+2eq
magic
+nhms
shorten
+short
none
Format
Extension
Format
Extension
bliksem
.blk
carine
.car
dedam
.dedam
dfg
.dfg
dimacs
.dimacs
eqp
.eqp
finder
.fin
geo
.geo
kif
.kif
leancop
.leancop
lf
.lf
oscar
.oscar
otter
.in
protein
.tme
prover9
.in
sem
.sem
setheo
.lop
smt
.smt
thinker
.thinker
oldtptp
.oldtptp
tptp
.tptp
waldmeister
.pr
~/TPTP/TPTP2X> tptp2X -tlr,cr,clr -fkif ../Problems/ALG/ALG001-1.p
---------------------------------------------------------------------
TPTP2X directory = /home/graph/tptp/TPTP/TPTP2X
TPTP directory = /home/graph/tptp/TPTP
Prolog interpreter = /usr/local/bin/eclipse
Files to convert = ../Problems/ALG/ALG001-1.p
Size =
Transformation = lr,cr,clr
Format to convert to = kif
Output directory = /home/graph/tptp/TPTP/TPTP2X/kif
---------------------------------------------------------------------
Made the directory /home/graph/tptp/TPTP/TPTP2X/kif/ALG
ALG001-1 -> /home/graph/tptp/TPTP/TPTP2X/kif/ALG/ALG001-1+lr.kif
ALG001-1 -> /home/graph/tptp/TPTP/TPTP2X/kif/ALG/ALG001-1+cr.kif
ALG001-1 -> /home/graph/tptp/TPTP/TPTP2X/kif/ALG/ALG001-1+clr.kif
~/TPTP/TPTP2X>
This run applies three separate transformations to the problem
ALG001-1.
The transformations are literal order reversal, clause order reversal, and
reversal of both literal and clause order.
The transformed problems are output in kif format, in the directory
kif/ALG below the TPTP2X directory.
The file names are ALG001-1+lr.kif, ALG001-1+cr.kif, and
ALG001-1+clr.kif.
~/TPTP/TPTP2X> tptp2X -q2 -s3..5 -fotter -d~tptp/tmp SYN001-1.g
SYN001-1 -> /home/tptp/tmp/SYN/SYN001-1.003+rm_eq_stfp.in
SYN001-1 -> /home/tptp/tmp/SYN/SYN001-1.004+rm_eq_stfp.in
SYN001-1 -> /home/tptp/tmp/SYN/SYN001-1.005+rm_eq_stfp.in
~/TPTP/TPTP2X>
This run 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
---------------------------------------------------------------------
TPTP2X directory = /home/tptp/TPTP/TPTP2X
TPTP directory = /home/tptp/TPTP
Prolog interpreter = /usr/local/bin/sicstus
Files to convert = -
Size =
Transformation = magic+shorten
Format to convert to = tptp
Output directory = -
---------------------------------------------------------------------
%--------------------------------------------------------------------------
% File : Shortened file, so there is no header
%--------------------------------------------------------------------------
input_clause(clause_1,axiom,
[++equal(X1,X1)]).
... Lots of output omitted here for brevity
input_clause(clause_41,theorem,
[--p2(c8,c7,c9)]).
%--------------------------------------------------------------------------
~/TPTP/TPTP2X>
This run 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 may 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.
Example
~/TPTP/TPTP2X> tptp2X -q0 -d~tptp/tmp -i
---- Interactive mode -----------------------------------------------
Files to convert [Problems/*/*.p] : ../Problems/GRP/GRP001-1.p
Files to convert [../Problems/GRP/GRP001-1.p] :
Size [] :
Transformation [none] : lr+rm_equality:stfp
Transformation [lr+rm_equality:stfp] :
Format to convert to [tptp] : setheo
Format to convert to [setheo] :
Output directory [/home/tptp/tmp] :
---- End of Interactive mode ----------------------------------------
---------------------------------------------------------------------
TPTP2X directory = /home/2/tptp/TPTP/TPTP2X
TPTP directory = /home/2/tptp/TPTP
Prolog interpreter = /usr/local/bin/sicstus
Files to convert = ../Problems/GRP/GRP001-1.p
Size =
Transformation = lr+rm_equality:stfp
Format to convert to = setheo:sign
Output directory = /home/tptp/tmp
---------------------------------------------------------------------
Made the directory /home/tptp/tmp/GRP
SICStus 3 #6: Mon Nov 3 18:32:08 MET 1997
... Lots of informational output omitted here for brevity
{/home/2/tptp/TPTP/TPTP2X/tptp2X.main compiled, 12080 msec 785600 bytes}
yes
yes
GRP001-1 -> /home/tptp/tmp/GRP/GRP001-1+lr+rm_eq_stfp.lop
~/TPTP/TPTP2X>
This run converts the problem GRP001-1 to a SETHEO format file.
The literals are reversed and all equality clauses except reflexivity
are removed.
The top level output directory is specified as \verb/~/tptp/tmp, below
which the subdirectory GRP is made.
The output file is named GRP001-1+lr+eq_stfp.lop.
Verbose mode is used, so all informational output is given.
The following subsections are only of interest to real Prolog users.
If you do not want to use Prolog directly, skip to the next section.
Running tptp2X from within Prolog
The tptp2X utility may 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:
Example
~/TPTP/TPTP2X> sicstus
SICStus 3 #6: Mon Nov 3 18:32:08 MET 1997
| ?- ['tptp2X.main'].
{consulting /home/2/tptp/TPTP/TPTP2X/tptp2X.main...}
... Lots of informational output omitted here for brevity
{/home/tptp/TPTP/TPTP2X/tptp2X.main consulted, 10750 msec 773088 bytes}
yes
| ?- tptp2X('Generators/SYN010-1.g',3:[2,4],[lr,cr]+magic,kif,'.').
{compiling /home/tptp/TPTP/Generators/SYN010-1.g...}
{/home/tptp/TPTP/Generators/SYN010-1.g compiled, 90 msec 4288 bytes}
SYN010-1 -> ./SYN010-1.003:002+lr+nhms.kif
SYN010-1 -> ./SYN010-1.003:002+cr+nhms.kif
SYN010-1 -> ./SYN010-1.003:004+lr+nhms.kif
SYN010-1 -> ./SYN010-1.003:004+cr+nhms.kif
yes
| ?- ^D
~/TPTP/TPTP2X>
This run generates two sizes of the generic problem SYN010-1, and
does two transformation sequences on each of the two sets of clauses, to
produce four output files.
The sizes are 3:2 and 3:4. The first transformation sequence is literal
order reversal followed by the non-Horn magic set transformation, and
the second transformation sequence is clause order reversal followed by
the non-Horn magic set transformation.
The files are output in KIF format in the current directory. The file
names are
SYN010-1.003:002+lr+nhms.kif, SYN010-1.003:002+cr+nhms.kif,
SYN010-1.003:004+lr+nhms.kif, and SYN010-1.003:004+cr+nhms.kif.
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.
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 tptp2T Script
The tptp2T script selects lines from either the
ProblemAndSolutionStatistics
file, by problem and solution characteristics.
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:
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 may be applied to different systems
individually.
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-v4.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).
Installing the TPTP
... the script will then ask for required information
... the script will then ask for required information
Converting Problems to Other Syntax
prompt> ./TPTP2X/tptp2X <desired_syntax>
As <desired_syntax>, choose any one of those listed in
Section Using tptp2X.
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 may have been ignored.
Please contact us if ...
Conclusion
Current Activities
The collection of more problems is continuing.
Everybody is invited to submit problems for inclusion.
Please contact us for details if you would like to contribute.
Further Plans
We have several short and long term plans for further development of the TPTP.
The main ideas are listed here.
General guidelines outlining the requirements for ATP system evaluation
will be produced.
A benchmark suite (the BSTP) will be selected from the TPTP.
The BSTP will be a small collection of problems, and will be a
minimal set of problems on which an ATP system evaluation can be based.
The BSTP will be accompanied by specific guidelines for computing a
performance index for an ATP system.
The TPTP may be extended to include problems expressed in non-classical
logics.
Acknowledgements
We are indebted to the following people and organizations who have
helped with the construction of the TPTP.