A unified proof system for QBF preprocessing

DOI10.1007/978-3-319-08587-6_7MaRDI QIDQ3192183zbMATH OpenOpenAlexFDO

Authors Marijn J. H. Heule, Martina Seidl, Armin Biere

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08587-6_7

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Solution validation and extraction for QBF preprocessing
• On QBF Proofs and Preprocessing
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• Bounded Universal Expansion for Preprocessing QBF
• Blocked clause elimination for QBF

Cited in

(29)

• The Qu-Prolog unification algorithm: formalisation and correctness
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• How QBF expansion makes strategy extraction hard
• Hardness and optimality in QBF proof systems modulo NP
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• Solution validation and extraction for QBF preprocessing
• Conformant planning as a case study of incremental QBF solving
• Long-distance Q-resolution with dependency schemes
• Quantified maximum satisfiability
• Incremental determinization
• Q-resolution with generalized axioms
• Lifting QBF resolution calculi to DQBF
• Long distance Q-resolution with dependency schemes
• The QBF Gallery: behind the scenes
• On QBF Proofs and Preprocessing
• On Unification of QBF Resolution-Based Calculi
• A First Step Towards a Unified Proof Checker for QBF
• Bounded Universal Expansion for Preprocessing QBF
• Local redundancy in SAT: generalizations of blocked clauses
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Inconsistency proofs for ASP: the ASP-DRUPE format
• SAT-Inspired Eliminations for Superposition
• Never trust your solver: certification for SAT and QBF
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
• Moving definition variables in quantified Boolean formulas
• Hard QBFs for merge resolution
• Formal correctness of a quadratic unification algorithm
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes

Describes a project that uses

Uses Software

• sQueezeBF
• Bloqqer
• DepQBF

This page was built for publication: A unified proof system for QBF preprocessing

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