A First Step Towards a Unified Proof Checker for QBF
From MaRDI portal
Publication:3612467
DOI10.1007/978-3-540-72788-0_21zbMath1214.68334OpenAlexW2127982853MaRDI QIDQ3612467
Christoph M. Wintersteiger, Daniel Kroening, Toni Jussila, Armin Biere, Carsten Sinz
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
Related Items
Solution validation and extraction for QBF preprocessing, Towards Uniform Certification in QBF, Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification, Unified QBF certification and its applications, Failed Literal Detection for QBF, Ranking function synthesis for bit-vector relations, A Unified Framework for Certificate and Compilation for QBF, Functional Encryption for Inner Product with Full Function Privacy, Validating QBF Validity in HOL4, Proving Valid Quantified Boolean Formulas in HOL Light, Dual proof generation for quantified Boolean formulas with a BDD-based solver, A Compact Representation for Syntactic Dependencies in QBFs, CAQE and QuAbS: Abstraction Based QBF Solvers, Hardness and optimality in QBF proof systems modulo NP
Uses Software
