The TPTP problem library. CNF release v1. 2. 1
From MaRDI portal
Publication:1272614
DOI10.1023/A:1005806324129zbMath0910.68197OpenAlexW1646117648MaRDI QIDQ1272614
Geoff Sutcliffe, Christian Suttner
Publication date: 3 January 1999
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1005806324129
Related Items
Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, Controlled integration of the cut rule into connection tableau calculi, A Query Language for Formal Mathematical Libraries, Transitive Separation Logic, The model evolution calculus as a first-order DPLL method, Octopus: combining learning and parallel search, Predicting and detecting symmetries in FOL finite model search, Things to know when implementing KBO, Exploiting parallelism: highly competitive semantic tree theorem prover, Applying SAT solving in classification of finite algebras, \textit{Theorema}: Towards computer-aided mathematical theory exploration, Computer supported mathematics with \(\Omega\)MEGA, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, MPTP 0.2: Design, implementation, and initial experiments, The ILTP problem library for intuitionistic logic, Linear and unit-resulting refutations for Horn theories, A scalable module system, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Internal axioms for domain semirings, IeanCOP: lean connection-based theorem proving, On using ground joinable equations in equational theorem proving, Model evolution with equality -- revised and implemented, Automation for interactive proof: first prototype, Mathematical applications of inductive logic programming, Eliminating redundant search space on backtracking for forward chaining theorem proving, Conjecture synthesis for inductive theories, On Automating the Calculus of Relations, LogAnswer - A Deduction-Based Question Answering System (System Description), 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, THF0 – The Core of the TPTP Language for Higher-Order Logic, Combined reasoning by automated cooperation, The design of the CADE-13 ATP system competition, Optimizing proof search in model elimination, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, On the mechanization of the proof of Hessenberg's theorem in coherent logic, The Relative Power of Semantics and Unification, Citius altius fortius, MPTP 0.1 - System Description, Proof Search for the First-Order Connection Calculus in Maude, MPTP-motivation, implementation, first experiments, Constraint solving for proof planning, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method, Automated Inference of Finite Unsatisfiability, Hashing and canonicalizing Notation 3 graphs, Using First-Order Theorem Provers in the Jahob Data Structure Verification System, Lightweight relevance filtering for machine-generated resolution problems, Computing finite models by reduction to function-free clause logic, Solving the \$100 modal logic challenge, TPTP, Automated Puzzle Solving, Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving, Partial matching for analogy discovery in proofs and counter-examples, Building proofs or counterexamples by analogy in a resolution framework, Labelled splitting, Automated verification of refinement laws, Solving quantified verification conditions using satisfiability modulo theories, Combining Instance Generation and Resolution, First order Stålmarck. Universal lemmas through branch merges, α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic, Encoding First Order Proofs in SMT, Presenting and Explaining Mizar, An Interactive Derivation Viewer, Panoptes, Extended transitive separation logic, Evaluating general purpose automated theorem proving systems
Uses Software
