Thousands of Problems for Theorem Provers

TPTP (Thousands of Problems for Theorem Provers)[1] is a freely available collection of problems for automated theorem proving.

It is used to evaluate the efficacy of automated reasoning algorithms.

[2][3][4] Problems are expressed in a simple text-based format for first order logic or higher-order logic.

[5] TPTP is used as the source of some problems in CASC.

This mathematical logic-related article is a stub.