TPTP World

There is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems, stemming from the Thousands of Problems for Theorem Provers (TPTP) problem library.

The TPTP syntax ... has become a de facto standard for formulating and exchanging logical problems for automated theorem provers.

The SZS ontology provides a fine grained ontology of result and output forms that are used to specify what has been established about a given ATP problem.

Evaluating ATP problems is important as it simplifies problem selection according to a user's intentions, and over the years, changes in problem ratings provide a quantitative indicator of advancement in ATP.

It is widely accepted that CASC has been a catalyst for the impressive progress that has taken place since then in the development of the current high-performance provers.