TPTP, aka Thousands of Problems for Theorem Provers, is a mathematics created in 1993 by Geoff Sutcliffe.
| #1913on PLDB | 33Years Old |
TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for automated theorem proving systems, expressed in a standardized text-based format supporting first-order logic (FOF), typed first-order form (TFF), typed higher-order form (THF), and clause normal form (CNF). It serves as a benchmark for evaluating automated reasoning algorithms and supports the CADE ATP System Competition (CASC).