A Unified Proof System for QBF Preprocessing
From MaRDI portal
Publication:3192183
DOI10.1007/978-3-319-08587-6_7zbMATH Open1409.68257OpenAlexW88271430MaRDI QIDQ3192183FDOQ3192183
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
Cited In (24)
- The QBF Gallery: behind the scenes
- Conformant planning as a case study of incremental QBF solving
- Quantified maximum satisfiability
- Hardness and optimality in QBF proof systems modulo NP
- Long Distance Q-Resolution with Dependency Schemes
- Q-Resolution with Generalized Axioms
- Inconsistency Proofs for ASP: The ASP - DRUPE Format
- How QBF expansion makes strategy extraction hard
- Formal correctness of a quadratic unification algorithm
- Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
- The Qu-Prolog unification algorithm: formalisation and correctness
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Lifting QBF Resolution Calculi to DQBF
- On Unification of QBF Resolution-Based Calculi
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- Title not available (Why is that?)
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Solution validation and extraction for QBF preprocessing
- On QBF Proofs and Preprocessing
- Incremental Determinization
- Long-distance Q-resolution with dependency schemes
- SAT-Inspired Eliminations for Superposition
- Moving definition variables in quantified Boolean formulas
- Never trust your solver: certification for SAT and QBF
Uses Software
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)
