The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for Automated Theorem Proving (ATP) systems for 1st order classical logic. Since the first release of the TPTP in 1993, many researchers have used the TPTP as an appropriate and convenient basis for testing their ATP systems. The TPTP is now the de facto standard for testing and evaluating ATP systems. The TSTP Solution Library is the flip-side of the TPTP. The TSTP will maintain solutions to all the problems in the TPTP, from all currently available state-of-the-art ATP systems. The solutions output by the systems will be translated and stored in a common format, so that the TSTP can be consistently interrogated and analysed. It is expected that the TSTP will immediately contribute to the development of ATP systems, by allowing system developers to easily access and analyse other systems' solutions to TPTP problems. In a broader context the TSTP will provide a basis for understanding and comparing proof structures, will be used for certification of ATP systems, and will form a framework within which problems will be formulated and solved using ATP tools and techniques.
This talk describes the work in progress towards the TSTP, including motivations, requirements, design decisions, and the various projects that are contributing to and using the TSTP.