Using the TPTP World

In order to use an ATP system it is necessary to prepare the problem for the ATP system, execute the ATP system, and postprocess the system's output as required. The details of these steps are described in the ATP process.

Using the `SystemOnTPTP` Interface

SystemOnTPTP is a meta-tool that is used to submit problems in TPTP syntax to ATP systems and other processing tools. It deals with the steps of:

Checking the problem file syntax
Adding axioms of equality if necessary.
Converting from TPTP syntax to the syntax of the system.
Running the system with a time limit.
Extracting the result and output from the system
Converting the output to the TPTP syntax

The command line version of SystemOnTPTP is available in the SystemExecution directory of the TPTPWorld. The command line format is

     SystemOnTPTP [-qN] SystemName---Version TimeLimit [-S] ProblemFile

e.g., SystemOnTPTP -q1 EP---0.999 30 -S MyProblem.p. The optional -qN controls the debug level, with -q0 being most verbose and -q3 least. The optional -S flag causes the system output to be converted to a TPTP format proof, if possible. The ProblemFile must be in TPTP format. If a TPTP library problem name is specified then SystemOnTPTP will find it, e.g., SystemOnTPTP SPASS---3.0 30 PUZ001+1. To get a list of the available systems do SystemOnTPTP -w.

SystemOnTPTP is also available online at:

    http://www.tptp.org/cgi-bin/SystemOnTPTP

The file to be processed may be an existing TPTP problem file, a file uploaded from your computer, a file at a URL, or pasted into the text box. To process a problem file:

Specify the file in one of the four ways.
Select the system with which to process the file. Please use only one system at a time, so everyone has a chance.
Select the output mode. The radio buttons determine how much progress/debug output you get, while the check boxes determine what form of output you get.
Use RunSelectedSystems.

The SystemB4TPTP and SystemOnTSTP interfaces provide access to tools for preparing problems and processing solutions. There are links to these interfaces from the SystemOnTPTP page.

Preparing a Problem File

Convert the problem from it's domain language to (first-order) logic. For example ...
Two squared plus something that is zero is an even number. Two square equals four. For anything that is zero, four minus that thing equals four plus that thing. There exists something that is zero. Therefore there exists something such that two squared minus that thing is even.
... may be expressed as:
```
A = { ∀X (zero(X) => even(sum(two_squared,X)))
      two_squared = four
      ∀X (zero(X) => difference(four,X) = sum(four,X))
      ∃X zero(X) }

C = ∃X even(difference(two_squared,X)) 
```

Create a file of the the axioms and conjecture, in a machine readable syntax (using the TPTP syntax). For example ...

fof(sum_is_even,axiom,
    ! [X] : (zero(X) => even(sum(two_squared,X)))   ).

fof(square_is_four,axiom,
    two_squared = four   ).

fof(zero_is_idempotent,axiom,
    ! [X] : (zero(X) => difference(four,X) = sum(four,X))   ).

fof(something_zero,axiom,
    ? [X] : zero(X)   ).

fof(difference_even,conjecture,
    ? [X] : even(difference(two_squared,X))   ).

Checking the Syntax of the formulae and the Consistency of the axioms

Check the syntax of the (machine readable) formulae.
The TPTP syntax can be checked using the tptp4X utility. The command line version of tptp4X is available in the ServiceTools directory of the TPTPWorld. The command line format is
```
     tptp4X ProblemFile
```
e.g., tptp4X MyProblem.p.
tptp4X has some other options, which can be explored with tptp4X -h.
tptp4X is also available online in the SystemB4TPTP interface. The BNFParser and BNFParserDrill, also available in the SystemB4TPTP interface, can also be used to check the syntax (precisely against the TPTP BNF), and give the parse tree as output.
Check the consistency of axioms.
- Try to establish that the axioms are satisfiable
  The satisfiability of the axioms can be checked by deleting/commenting out the conjecture, and submitting the file to a model finding program, via SystemOnTPTP. For example
```
    SystemOnTPTP -q1 Mace2---2.2 30 MyProblem.p 
```
  SystemOnTPTP should report Satisfiable. If it does not, then either the axioms are too complicated for the model finder, or the axioms are Unsatisfiable (not what you want).
- Try to establish that the axioms are unsatisfiable
  To check for unsatisfiability, submit the file (with the conjecture still commented out) to a theorem prover that establishes logical consequence via unsatisfiability - if such a system is given a file of axioms it will try to establish that the axioms are unsatisfiable. For example
```
    SystemOnTPTP -q1 Otter--- 30 MyProblem.p 
```
  If SystemOnTPTP reports Unsatisfiable then the axioms need to be fixed.

Establishing Logical Consequence

Try to prove logical consequence
The conjecture can be proved to be a logical consequence of the axioms by submitting the file (axioms and conjecture) to a theorem prover via SystemOnTPTP. For example
```
    SystemOnTPTP -q1 Otter--- 30 MyProblem.p 
```
If SystemOnTPTP reports Theorem then the conjecture is a logical consequence of the axioms. If it does not, then either the problem is too hard for the theorem prover, or the conjecture is not a logical consequence of the axioms.
Try to prove non-logical consequence The conjecture can be proved to be a non-logical consequence of the axioms by submitting the file (axioms and conjecture) to a model finder. For example
```
    SystemOnTPTP -q1 Mace2---2.2 30 MyProblem.p 
```
If SystemOnTPTP reports CounterSatisfiable then the axioms or conjecture need to be fixed.

Generating a Derivation and Derivation Tree Image

A derivation for a provable conjecture can be generated by submitting the file (axioms and conjecture) to a theorem prover that can output a derivation. For example

    SystemOnTPTP -q1 EP---0.999 30 -S MyProblem.p

A derivation tree for a derivation can be generated by submitting a derivation file to IDV. The command line version of IDV is available in the ServiceTools directory of the TPTPWorld. The command line format is

     IDV SolutionFile

e.g., IDV MySolution.s.

Preprocessing a Problem File

SystemOnTPTP deals with all the necessary steps of preprocessing a problem file before giving it to the selected system. In some situations it is desirable to perform these steps individually. The tptp2X (and for some things, tptp4X) utility can be used for most individual steps. These are available in the TPTP2X directory of the TPTP problem library, and the ServiceTools directory of the TPTPWorld, respectively. Running these with a -h flag will provide usage instructions.

To add all axioms of equality, set the transform field to add_equality.
To convert to CNF, set the transform field to clausify:otter.
To convert to CNF and simplify the clauses in obvious ways, set the transform field to cnf:otter.
To save the formulae in another syntax, set the format field to the syntax name, e.g., dfg, otter.

Exercise

Convert this problem to FOL ...
If someone is wise, then either their father or mother is wise. Jim's father is Bob. Jim's mother is Maggie. Prove: If Jim is wise then either Bob or Maggie is wise.
Convert the FOL to TPTP syntax. Check the syntax and format.
Check that the axioms are consistent.
Prove the theorem.
Generate a TPTP format solution.
Generate an image of the derivation.