Thousands of Problems for Theorem Provers

{{Short description|Collection of problems for Automated Theorem Proving}}

TPTP (Thousands of Problems for Theorem Provers){{cite web|title=The TPTP Problem Library for Automated Theorem Proving|url=http://www.tptp.org/}} is a freely available collection of problems for automated theorem proving. It is used to evaluate the efficacy of automated reasoning algorithms.{{cite book |chapter=Comparing Unification Algorithms in First-Order Theorem Proving| year=2009| last1=Hoder |first1=Kryštof |last2=Voronkov |first2=Andrei | title=KI 2009: Advances in Artificial Intelligence| series=Lecture Notes in Computer Science| volume=5803| pages=435–443|doi=10.1007/978-3-642-04617-9_55 | isbn=978-3-642-04616-2|chapter-url=https://www.researchgate.net/publication/221562903|citeseerx=10.1.1.329.1809 }}{{cite conference |contribution=First-Order Proof Tactics in Higher-Order Logic Theorem Provers |title=Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS Experiences|url=https://ntrs.nasa.gov/api/citations/20030067561/downloads/20030067561.pdf|editor1-first=Myla|editor1-last=Archer|editor2-first=Ben|editor2-last=De Vito|editor3-first=César|editor3-last=Muñoz|pages=56–68|date=September 2003|publisher=NASA Scientific and Technical Information Program Office|series=Conference Publications|volume=NASA/CP-2003-212448|last1=Hurd |first1=Joe |s2cid=11201048 }}{{cite journal |title=Using Hundreds of Workstations to Solve First-Order Logic Problems |year=1994 |last1=Segre |first1=Alberto Maria| last2=Sturgill |first2=David B. |url=https://www.aaai.org/Papers/AAAI/1994/AAAI94-029.pdf |journal=AAAI-94 Proceedings.}} Problems are expressed in a simple text-based format for first order logic or higher-order logic.{{cite book |chapter= THF0 – The Core of the TPTP Language for Higher-Order Logic |year=2008 |last1=Benzmüller |first1=Christoph |last2=Rabe |first2=Florian |last3=Sutcliffe |first3=Geoff |title=Automated Reasoning |series=Lecture Notes in Computer Science |volume=5195 |pages=491–506 |doi=10.1007/978-3-540-71070-7_41|isbn=978-3-540-71069-1 }} TPTP is used as the source of some problems in CASC.