Optimizing proof search in model elimination

DOI10.1007/3-540-61511-3_97MaRDI QIDQ4647531zbMATH OpenOpenAlexFDO

Authors

Publication date 15 January 2019

Published in Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61511-3_97

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 517000
• An Implementation of the Model Elimination Proof Procedure
• Lemma and cut strategies for propositional model elimination
• Model elimination without contrapositives
• Subgoal alternation in model elimination

Cites work

• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• A sequent-style model elimination strategy and a positive refinement
• An examination of the prolog technology theorem-prover
• Controlled integration of the cut rule into connection tableau calculi
• Depth-first iterative-deepening: An optimal admissible tree search
• scientific article; zbMATH DE number 3985190 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Isabelle. A generic theorem prover
• lean\(T^ AP\): Lean tableau-based deduction
• Mechanical Theorem-Proving by Model Elimination
• Model elimination without contrapositives
• Obvious inferences
• SETHEO: A high-performance theorem prover
• The TPTP problem library. CNF release v1. 2. 1

Cited in

(19)

• HOL(y)Hammer: online ATP service for HOL Light
• GRUNGE: a grand unified ATP challenge
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• scientific article; zbMATH DE number 517000 (Why is no real title available?)
• Subgoal alternation in model elimination
• An Implementation of the Model Elimination Proof Procedure
• Learning-assisted theorem proving with millions of lemmas
• scientific article; zbMATH DE number 834572 (Why is no real title available?)
• Loop Elimination, a Sound Optimisation Technique for PTTP Related Theorem Proving
• Controlled use of clausal lemmas in connection tableau calculi
• Mechanising Gödel-Löb provability logic in HOL light
• Machine Learning for Inductive Theorem Proving
• A Mizar mode for HOL
• Iterative monomorphisation
• Duper: a proof-producing superposition theorem prover for dependent type theory
• Proof optimization for partial redundancy elimination

Describes a project that uses

Uses Software

• Isabelle
• SETHEO
• TPTP
• ML
• HOL

This page was built for publication: Optimizing proof search in model elimination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647531)