The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

DOI10.1007/s10817-017-9407-7zbMath1425.68381OpenAlexW2588018425MaRDI QIDQ1694574

Geoff Sutcliffe

Publication date: 2 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9407-7

zbMATH Keywords

ATP standards and toolsATP system evaluationTPTP

Mathematics Subject Classification ID

Related Items (49)

Heterogeneous heuristic optimisation and scheduling for first-order theorem proving ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Implementing Superposition in iProver (System Description) ⋮ Towards Verifying Logic Programs in the Input Language of clingo ⋮ Towards finding longer proofs ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Extensional higher-order paramodulation in Leo-III ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ The MET: The Art of Flexible Reasoning with Modalities ⋮ FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets ⋮ SAT-Inspired Higher-Order Eliminations ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Superposition for higher-order logic ⋮ Relaxed weighted path order in theorem proving ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Verifying Tight Logic Programs with anthem and vampire ⋮ Automated deduction and knowledge management in geometry ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Superposition with lambdas ⋮ A prover dealing with nominals, binders, transitivity and relation hierarchies ⋮ A unifying splitting framework ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Superposition for full higher-order logic ⋮ Neural precedence recommender ⋮ Restricted combinatory unification ⋮ GRUNGE: a grand unified ATP challenge ⋮ Names are not just sound and smoke: word embeddings for axiom selection ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Old or heavy? Decaying gracefully with age/weight shapes ⋮ Faster, higher, stronger: E 2.3 ⋮ Formal Qualitative Spatial Augmentation of the Simple Feature Access Model ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Subsumption demodulation in first-order theorem proving ⋮ SGGS decision procedures ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Ground joinability and connectedness in the superposition calculus ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Lash 1.0 (system description) ⋮ \textsf{Goéland}: a concurrent tableau-based theorem prover (system description) ⋮ Bayesian ranking for strategy scheduling in automated theorem provers ⋮ Vampire getting noisy: Will random bits help conquer chaos? (system description) ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• ILTP
• SATLIB
• MPTP 0.2
• OTTER
• SMT-LIB
• TPTP
• CSPLib
• Sledgehammer
• leanCoP
• ileanCoP
• SAD
• Flyspeck
• MaLARea
• SMTtoTPTP
• FOOL
• IDV
• QBFEVAL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A learning-based fact selector for Isabelle/HOL
• MPTP 0.2: Design, implementation, and initial experiments
• The ILTP problem library for intuitionistic logic
• Combined reasoning by automated cooperation
• Seventy-five problems for testing automatic theorem provers
• Non-Horn clause logic programming without contrapositives
• Automated deduction in von Neumann-Bernays-Gödel set theory
• The TPTP problem library. CNF release v1. 2. 1
• Evaluating general purpose automated theorem proving systems
• The IJCAR ATP system competition
• Quantified multimodal logics in simple type theory
• ATP and presentation service for Mizar formalizations
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• An Interactive Derivation Viewer
• The TPTP Typed First-Order Form with Arithmetic
• The TPTP World – Infrastructure for Automated Reasoning
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• SMTtoTPTP – A Converter for Theorem Proving Formats
• TPTP, TSTP, CASC, etc.
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Automated Reasoning in Kleene Algebra
• System for Automated Deduction (SAD): A Tool for Proof Verification
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
• Problems and Experiments for and with Automated Theorem-Proving Programs
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• Automated Reasoning
• Sledgehammer: Judgement Day

This page was built for publication: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0