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

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, 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

• OTTER
• TPTP

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