Maths in the TPTP
Abstract
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.
A large portion of the TPTP is concerned with problems in mathematics.
This talk describes the mathematical domains now in the TPTP, and provides
some insight into the performance of state-of-the-art ATP systems on the
problems in these domains.
For those new to the eld this information provides an established starting
point for research.
For those already involved, this talk summarizes what has been achieved so far.