The TPTP problem library

DOI10.1007/3-540-58156-1_18zbMath1433.68569OpenAlexW1768790486MaRDI QIDQ5210777

Christian Suttner, Theodor Yemenis, Geoff Sutcliffe

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_18

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Digital mathematics libraries and repositories (68V35)

Related Items (30)

SAD as a mathematical assistant -- how should we go from here to there? ⋮ ILF-SETHEO ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ Computing answers with model elimination ⋮ MGTP: A model generation theorem prover — Its advanced features and applications — ⋮ Ordered tableaux: Extensions and applications ⋮ Subgoal alternation in model elimination ⋮ Efficient Well-Definedness Checking ⋮ Learning domain knowledge to improve theorem proving ⋮ The design of the CADE-13 ATP system competition ⋮ SiCoTHEO: Simple competitive parallel theorem provers ⋮ The tableau-based theorem prover 3 T A P Version 4.0 ⋮ On the practical value of different definitional translations to normal form ⋮ Efficient model generation through compilation ⋮ Experiments in the heuristic use of past proof experience ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ Model elimination without contrapositives ⋮ The applicability of logic program analysis and transformation to theorem proving ⋮ The TPTP problem library ⋮ Solving hard Mizar problems with instantiation and strategy invention ⋮ Handling transitive relations in first-order automated reasoning ⋮ Integration of automated and interactive theorem proving in ILF ⋮ CODE: A powerful prover for problems of condensed detachment ⋮ Evolving combinators ⋮ Hyper tableaux ⋮ Proofs as schemas and their heuristic use ⋮ Automatic acquisition of search control knowledge from multiple proof attempts. ⋮ Efficient model generation through compilation. ⋮ Practically useful variants of definitional translations to normal form ⋮ Subsumption algorithms based on search trees

Uses Software

• TPTP
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Challenge problems in elementary calculus
• Set theory in first-order logic: Clauses for Gödel's axioms
• Seventy-five problems for testing automatic theorem provers
• Schubert's steamroller problem: Formulations and solutions
• Non-Horn clause logic programming without contrapositives
• Automated deduction in von Neumann-Bernays-Gödel set theory
• Single axioms for groups and abelian groups with various operations
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• Problems and Experiments for and with Automated Theorem-Proving Programs
• The TPTP problem library

This page was built for publication: The TPTP problem library