TPTP
Abstract
The TPTP (Thousands of Problems for Theorem Provers) 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.
This talk describes the TPTP and associated infrastructure,
from its use of Clause Normal Form (CNF), via the First-Order Form (FOF) and
Typed First-order Forms (TF0 and TF1), through to the Typed Higher-order
Forms (TH0 and TH1).
The talk summarizes the aims and history of the TPTP,
reviews the structure and contents of TPTP problems,
documents its growth up to v7.3.0,
gives an overview of TPTP-related infrastructure,
and
describes current work extending
the TPTP to include boolean terms and modalities.