A resolution-style proof system for DQBF

DOI10.1007/978-3-319-66263-3_20zbMATH Open1496.03050OpenAlexW2743440074MaRDI QIDQ1680262FDOQ1680262

Authors: Markus Rabe 

Publication date: 15 November 2017

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

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

Mathematics Subject Classification ID

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

Cited In (10)

• 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
• Title not available (Why is that?)

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)