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 via WWW

ReadMe-v2.7.0 (7.6 kByte) contains an overview of the TPTP.
TPTP-v2.7.0 .tar.gz (8.5 MByte, 370.5 MByte unpacked) contains the library (including a copy of the ReadMe-v2.7.0 file).

There also might be a file called BuggedProblems-v2.7.0, containing a list of files that have been found to contain errors, in the current release (bugs that have been discovered after the release has been distributed).

These files are available on the WWW.

Installing the TPTP

prompt> gunzip -c TPTP-v2.7.0 .tar.gz | tar xvf -

prompt> TPTP-v2.7.0 /Scripts/tptp1T_install ... the script will then ask for required information

prompt> TPTP-v2.7.0 /TPTP2X/tptp2X_install ... the script will then ask for required information

If you don't have any Prolog installed, you need to get one first.

Converting Problems to Other Syntax

prompt> TPTP-v2.7.0
/TPTP2X/tptp2X <desired_syntax>

As <desired_syntax>, choose any one of those listed in Section Using tptp2X.

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.

Important: Using the TPTP

By providing this library of ATP problems, and a specification of how these problems should be presented to ATP systems, it is our intention to place the testing, evaluation, and comparison of ATP systems onto a firm footing. For this reason, you should abide by the following conditions when using TPTP problems and presenting your results:

The TPTP release number must be stated.

Each problem must be referenced by its unambiguous syntactic name.

No formulae may be changed, added, or removed without explicit notice (this holds also for removing equality axioms when built-in equality is provided by the prover).

The formulae may not be reordered without explicit notice. If any reordering is done using the tptp2X utility, (see Section The tptp2X Utility), the reordering must be explicitly noted.
The header information in each problem may not be used by the ATP system without explicit notice. Any information that is given to the ATP system, other than that in the input_formulas and input_clauses, must be explicitly noted.
All system switches and default settings must be recorded.

Abiding by these rules will allow unambigous identification of the problem, the formulae, and further input to the ATP system. If you follow these rules, please make this 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 ...

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 (in the Documents directory - see Section Physical Organization). 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.

Our contact addresses are given on in the title.