The TPTP (Thousands of Problems for Theorem Provers) problem library is a library of test problems for ATP systems. Since its first release in 1993, many researchers have used the TPTP as an appropriate and convenient basis for ATP system evaluation. The TPTP has also been the basis for further research activities, including problem and system rating, the CADE ATP System Competition (CASC), various meta-ATP systems, and most recently the TSTP (Thousands of Solutions for Theorem Provers).
The TSTP solution library is a library of solutions from ATP systems, expressed in a standard syntax. It is hoped that many researchers will use the TSTP as an approriate and convenient basis for ATP solution analysis. The TSTP is already the basis for further research activities, including proof presentation, the DV proof verifier, and theorem discovery.
This talk will provide an overview of these research projects.