TPTP and TSTP Quick Guide

The TPTP and TSTP Libraries

The TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for ATP systems.
- Start at the WWW page http://www.tptp.org.
- For lots of details (the converse of this quick guide) read the technical manual.
- You can browse the TPTP problems online.
The TSTP (Thousands of Solutions from Theorem Provers) is a library of solutions to test problems for ATP systems.
- Start at the WWW page http://www.tptp.org/TSTP.
- There is no technical manual for the TSTP (yet).
- You can browse the TSTP solutions online.

How to use the TPTP language to write problems.
- Sample FOF problem: PUZ001+1
- Sample CNF problem: MGT031-1
How to use the TPTP language to record derivations.
- Sample derivation (a refutation): EP 0.99 on PUZ001+1
How to use the TPTP language to record finite interpretations.
- Sample finite interpretation: Darwin 1.31 on MGT031-1
The TPTP language grammar in BNF.
The SZS ontology of results that a system may establish for a problem.

These are easy test problems that should be solved with the given SZS result.

(As a cut-and-paste list: SYN075+1 MGT019+2 KRS063+1 KRS018+1 SYN075-1 MGT031-1 MGT041-2 NLP114-1 BOO003-4 BOO027-1)

These are hard test problems. If you solve any of these then either your system is very good, or your system is unsound.

(As a cut-and-paste list: GEO090+1 LDA014-1 ROB032-1)