The TPTP Problem Library and BSTP Benchmark Suite
Appeared in Volume 6/4, November 1993
Keywords: benchmarks.
The TPTP (Thousands of Problems for Theorem Provers) problem library is a
library of test problems for first order Automated Theorem Proving (ATP)
systems.
The BSTP (Benchmark Suite for Theorem Provers) will be a selection of problems
from the TPTP, to be used for evaluating ATP systems.
The aim of developing the TPTP problem library and the BSTP benchmark suite is
to provide the ATP community with:
- A comprehensive library of ATP test problems available at present, in order
to provide an overview and a simple, unambiguous reference mechanism.
- A comprehensive list of references for the problems. The references appear in
the problem files, and are collated in an associated technical report.
- A collection of further information regarding individual problems and the
library as a whole.
- A rating of the difficulty for each problem, based on the state-of-the-art in
ATP.
- A selection of the problems as a benchmark suite for evaluating general
purpose ATP systems.
- An evaluation guideline such that ATP systems can be meaningfully compared.
If you would like to be kept informed of the status and availability of the
TPTP problem library and the BSTP benchmark suite, then please contact:
Geoff Sutcliffe
Dept. of Computer Science
James Cook Univ., Australia
Email: geoff@cs.jcu.edu.au
