Tysiące problemów dla dowódców twierdzeń

TPTP (Thousands of Problems for Theorem Provers) to ogólnodostępny zbiór problemów do automatycznego dowodzenia twierdzeń . Służy do oceny skuteczności zautomatyzowanych algorytmów wnioskowania. Problemy są wyrażane w prostym formacie tekstowym dla logiki pierwszego rzędu lub logiki wyższego rzędu. TPTP jest używany jako źródło niektórych problemów w CASC .