Subsumption-linear Q-resolution for QBF theorem proving

DOI10.1007/978-3-031-39784-4_23MaRDI QIDQ6199591zbMATH OpenOpenAlexFDO

Authors 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

• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A non-prenex, non-clausal QBF solver with game-state learning
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• An extension to linear resolution with selection function
• Autarky pruning in propositional model elimination reduces failure redundancy
• Contributions to the theory of practical quantified Boolean formula solving
• Controlled integration of the cut rule into connection tableau calculi
• Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1950260 (Why is no real title available?)
• scientific article; zbMATH DE number 1461245 (Why is no real title available?)
• scientific article; zbMATH DE number 1470716 (Why is no real title available?)
• Mechanical Theorem-Proving by Model Elimination
• New resolution-based QBF calculi and their proof complexity
• Resolution for quantified Boolean formulas
• The use of lemmas in the model elimination procedure

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

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