TPTP World

The Community Agrees

• There is a well established infrastructure that supports research, development, and deployment of Automated Reasoning 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 the CADE ATP System Competition (CASC) has been a catalyst for the impressive progress that has taken place since then in the development of the current high-performance provers.

An Octopus

• Standards and Data sets
• Tools and Services
• Events
• Documentation
• Proposals