Subsumption-linear Q-resolution for QBF theorem proving

DOI10.1007/978-3-031-39784-4_23OpenAlexW4386226285MaRDI QIDQ6199591

Allen van Gelder

Publication date: 28 February 2024

Published in: Logic, Language, Information, and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-39784-4_23

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An extension to linear resolution with selection function
• Controlled integration of the cut rule into connection tableau calculi
• The use of lemmas in the model elimination procedure
• Autarky pruning in propositional model elimination reduces failure redundancy
• Resolution for quantified Boolean formulas
• Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• New Resolution-Based QBF Calculi and Their Proof Complexity
• Mechanical Theorem-Proving by Model Elimination
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness

This page was built for publication: Subsumption-linear Q-resolution for QBF theorem proving