On Unification of QBF Resolution-Based Calculi
From MaRDI portal
Recommendations
- New resolution-based QBF calculi and their proof complexity
- Proof complexity of resolution-based QBF calculi
- On sequent systems and resolution for QBFs
- A unified proof system for QBF preprocessing
- Lifting QBF resolution calculi to DQBF
- QBF Resolution Systems and Their Proof Complexities
- The Qu-Prolog unification algorithm: formalisation and correctness
- A First Step Towards a Unified Proof Checker for QBF
- On propositional QBF expansions and Q-resolution
Cited in
(34)- Q-resolution with generalized axioms
- Long distance Q-resolution with dependency schemes
- Solving QBF with counterexample guided refinement
- Lower bound techniques for QBF expansion
- scientific article; zbMATH DE number 7559123 (Why is no real title available?)
- The QBF Gallery: behind the scenes
- A First Step Towards a Unified Proof Checker for QBF
- Towards Uniform Certification in QBF
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- New resolution-based QBF calculi and their proof complexity
- Lifting QBF resolution calculi to DQBF
- Formal correctness of a quadratic unification algorithm
- A game characterisation of tree-like Q-resolution size
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Understanding cutting planes for QBFs
- The Qu-Prolog unification algorithm: formalisation and correctness
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Incremental determinization
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- Characterising tree-like Frege proofs for QBF
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- Models and counter-models of quantified Boolean formulas (invited talk)
- A game characterisation of tree-like Q-resolution size
- Feasible interpolation for QBF resolution calculi
- Size, cost and capacity: a semantic technique for hard random QBFs
- A Unified Framework for Certificate and Compilation for QBF
- A simple proof of QBF hardness
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- On Stronger Calculi for QBFs
- Lower bound techniques for QBF proof systems
- Long-distance Q-resolution with dependency schemes
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- scientific article; zbMATH DE number 7278086 (Why is no real title available?)
- Never trust your solver: certification for SAT and QBF
This page was built for publication: On Unification of QBF Resolution-Based Calculi
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2922598)
