TPTP

TPTP (Thousands of Problems for Theorem Provers)^[1] とは自由に利用可能な自動定理証明のための問題集である。これは自動推論アルゴリズムの効率の評価のために使用される^[2][3][4]。問題は一階述語論理や高階述語論理のためのシンプルなテキストベースの形式で表される^[5]。TPTPはCASCの中で問題の収集元として使われている。