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

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

• Isabelle
• SETHEO
• ML
• 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