Soundness of Q-resolution with dependency schemes

DOI10.1016/J.TCS.2015.10.020MaRDI QIDQ896919zbMATH OpenOpenAlexFDO

Authors Friedrich Slivovsky, Stefan Szeider

Publication date 15 December 2015

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2015.10.020

zbMATH Keywords

quantified Boolean formulas\(\mathcal{Q}\)-resolutiondependency schemesqbf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Variable dependencies and Q-resolution
• Long-distance Q-resolution with dependency schemes
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Long distance Q-resolution with dependency schemes
• A resolution-style proof system for DQBF

Cites work

• scientific article; zbMATH DE number 5719280 (Why is no real title available?)
• scientific article; zbMATH DE number 1798189 (Why is no real title available?)
• A machine program for theorem-proving
• A unified proof system for QBF preprocessing
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Backdoor sets of quantified Boolean formulas
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• Computing Resolution-Path Dependencies in Linear Time ,
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
• Integrating dependency schemes in search-based QBF solvers
• Lower bounds for multiplayer noncooperative games of incomplete information
• On Unification of QBF Resolution-Based Calculi
• On propositional QBF expansions and Q-resolution
• Resolution for quantified Boolean formulas
• Unified QBF certification and its applications
• Variable Dependencies of Quantified CSPs
• Variable independence and resolution paths for quantified Boolean formulas

Cited in

(17)

• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• Solution validation and extraction for QBF preprocessing
• Dependency schemes for DQBF
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• Certified DQBF solving by definition extraction
• Strong (D)QBF dependency schemes via tautology-free resolution paths
• Should Decisions in QCDCL Follow Prefix Order?
• Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
• Small resolution proofs for QBF using dependency treewidth
• Long distance Q-resolution with dependency schemes
• Variable dependencies and Q-resolution
• A resolution-style proof system for DQBF
• Long-distance Q-resolution with dependency schemes
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution

This page was built for publication: Soundness of \(\mathcal{Q}\)-resolution with dependency schemes

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