A resolution-style proof system for DQBF

DOI10.1007/978-3-319-66263-3_20MaRDI QIDQ1680262zbMATH OpenOpenAlexFDO

Authors Markus Rabe

Publication date 15 November 2017

Full work available at URL https://doi.org/10.1007/978-3-319-66263-3_20

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Variable dependencies and Q-resolution
• Long distance Q-resolution with dependency schemes
• Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF

Cited in

(10)

• scientific article; zbMATH DE number 7559123 (Why is no real title available?)
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Certified DQBF solving by definition extraction
• Lifting QBF resolution calculi to DQBF
• Building strategies into QBF proofs
• Solving dependency quantified Boolean formulas using quantifier localization
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Fast DQBF Refutation
• QBF Resolution Systems and Their Proof Complexities

This page was built for publication: A resolution-style proof system for DQBF

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