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:
- ReadMe-v9.0.0
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-v9.0.0
file).
There also might be a file called
BuggedProblems-v9.0.0
,
containing a list of files that have been found to contain errors, in
the current release (bugs that have been discovered after the release has
been distributed).
These files are available online.
Installing the TPTP
prompt> tar xzf TPTP-v9.0.0
.tgz
prompt> cd TPTP-v9.0.0
prompt> ./Scripts/tptp2T_install
... the script will then ask for required information
prompt> ./TPTP2X/tptp2X_install
... the script will then ask for required information
If you don't have any Prolog installed, you need to get one first.
Both utilities can be installed in a default configuration by appending a
-default flag to the install command.
Important: Using the TPTP
Appropriate use of the TPTP allows developers and users to meaningfully
evaluate ATP systems.
To that end, the following guidelines for using the TPTP and presenting
results should be followed.
- 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 unambigous identification of the
problem, the formulae used, and further input to the ATP system.
If you follow the rules, please make it clear in any presentation of your
results, by an explicit statement.
We propose that you state
"These results were obtained in compliance with the guidelines for
use of the TPTP".
By making this clear statement, ATP researchers are assured of your
awareness of our guidelines.
Conversely, it will become clear when the guidelines might have been ignored.
- 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.