Optimizing proof search in model elimination

DOI10.1007/3-540-61511-3_97zbMath1412.68231OpenAlexW1664582451MaRDI QIDQ4647531

No author found.

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

Related Items (8)

Mechanising Gödel-Löb provability logic in HOL light ⋮ Machine Learning for Inductive Theorem Proving ⋮ Subgoal alternation in model elimination ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ GRUNGE: a grand unified ATP challenge ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• Unnamed Item
• Unnamed Item
• Unnamed Item
• TPTP
• HOL

Cites Work

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

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