Subsumption-linear Q-resolution for QBF theorem proving
From MaRDI portal
Publication:6199591
DOI10.1007/978-3-031-39784-4_23OpenAlexW4386226285MaRDI QIDQ6199591FDOQ6199591
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
Cites Work
- Title not available (Why is that?)
- Resolution for quantified Boolean formulas
- Title not available (Why is that?)
- Contributions to the theory of practical quantified Boolean formula solving
- A non-prenex, non-clausal QBF solver with game-state learning
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- Title not available (Why is that?)
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- Autarky pruning in propositional model elimination reduces failure redundancy
- Mechanical Theorem-Proving by Model Elimination
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
- Title not available (Why is that?)
- New resolution-based QBF calculi and their proof complexity
- Controlled integration of the cut rule into connection tableau calculi
- An extension to linear resolution with selection function
- 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)
