A First Step Towards a Unified Proof Checker for QBF
From MaRDI portal
Publication:3612467
DOI10.1007/978-3-540-72788-0_21zbMATH Open1214.68334OpenAlexW2127982853MaRDI QIDQ3612467FDOQ3612467
Authors: Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kroening, Christoph M. Wintersteiger 
Publication date: 10 March 2009
Published in: Theory and Applications of Satisfiability Testing – SAT 2007 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-72788-0_21
Recommendations
Cited In (20)
- Title not available (Why is that?)
- A Compact Representation for Syntactic Dependencies in QBFs
- Towards Uniform Certification in QBF
- Hardness and optimality in QBF proof systems modulo NP
- Validating QBF Validity in HOL4
- Functional encryption for inner product with full function privacy
- Failed literal detection for QBF
- Formal correctness of a quadratic unification algorithm
- Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
- Unified QBF certification and its applications
- The Qu-Prolog unification algorithm: formalisation and correctness
- Ranking function synthesis for bit-vector relations
- On Unification of QBF Resolution-Based Calculi
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- A Unified Framework for Certificate and Compilation for QBF
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Solution validation and extraction for QBF preprocessing
- On QBF Proofs and Preprocessing
- First-order unification in the PVS proof assistant
- Proving Valid Quantified Boolean Formulas in HOL Light
Uses Software
This page was built for publication: A First Step Towards a Unified Proof Checker for QBF
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612467)
