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)
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
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 the six CASCs held so far (since 1996) have been
a catalyst for the impressive progress that has taken place since then in
the development of the current high-performance provers.