Stepping Stones in the TPTP World
Abstract
The TPTP World is a well established infrastructure that supports research, development, and
deployment of Automated Theorem Proving (ATP) systems.
There are key components that help make the TPTP World a success:
the TPTP problem library was first released in 1993,
the CADE ATP System Competition (CASC) was conceived after CADE-12 in 1994,
problem difficulty ratings were added in 1997,
the current TPTP language was adopted in 2003,
the SZS ontologies were specified in 2004,
the TSTP solution library was built starting around 2005,
the Specialist Problem Classes (SPCs) have been used to classify problems since 2010,
the SystemOnTPTP service has been offered from 2011,
the StarExec service was started in 2013,
and
a world of TPTP users have helped all along.
This talk reviews these "stepping stones" in the TPTP World.