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.