TPTP

Abstract

The Thousands of Problems for Theorem Provers Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with a comprehensive library of the ATP test problems that are available today. The principal aim of this project is to move the evaluation of ATP systems from the previously ad hoc situation onto a firm footing. This became necessary, as results being published do not always accurately reflect the capabilities of the ATP system being considered.