A First Step Towards a Unified Proof Checker for QBF

DOI10.1007/978-3-540-72788-0_21MaRDI QIDQ3612467zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• On Unification of QBF Resolution-Based Calculi
• A unified proof system for QBF preprocessing
• New resolution-based QBF calculi and their proof complexity
• Unified QBF certification and its applications
• On propositional QBF expansions and Q-resolution

Cited in

(20)

• scientific article; zbMATH DE number 5542982 (Why is no real title available?)
• A Compact Representation for Syntactic Dependencies in QBFs
• Hardness and optimality in QBF proof systems modulo NP
• Towards Uniform Certification in QBF
• 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
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• On Unification of QBF Resolution-Based Calculi
• Solution validation and extraction for QBF preprocessing
• A Unified Framework for Certificate and Compilation for QBF
• On QBF Proofs and Preprocessing
• CAQE and QuAbS: Abstraction Based QBF Solvers
• First-order unification in the PVS proof assistant
• Proving Valid Quantified Boolean Formulas in HOL Light

Describes a project that uses

Uses Software

• QUBOS
• Quaffle

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)