Lower bound techniques for QBF proof systems

DOI10.4230/LIPICS.STACS.2018.2MaRDI QIDQ3304096zbMATH OpenOpenAlexFDO

Authors Meena Mahajan

Publication date 5 August 2020

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2018/8536/pdf/LIPIcs-STACS-2018-2.pdf/

zbMATH Keywords

lower bound techniquesproof complexityquantified Boolean formulasresolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Lower bounds: from circuits to QBF proof systems
• Reasons for hardness in QBF proof systems
• Proof complexity of resolution-based QBF calculi
• scientific article; zbMATH DE number 7278086
• Lower bound techniques for QBF expansion

Cites work

• A combinatorial characterization of resolution width
• A non-prenex, non-clausal QBF solver with game-state learning
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Contributions to the theory of practical quantified Boolean formula solving
• Counterexample-guided abstraction refinement for symbolic model checking
• Expansion-based QBF solving versus Q-resolution
• Feasible interpolation for QBF resolution calculi
• Formal Methods in Computer-Aided Design
• scientific article; zbMATH DE number 7228403 (Why is no real title available?)
• scientific article; zbMATH DE number 1008380 (Why is no real title available?)
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Lower bounds: from circuits to QBF proof systems
• On Unification of QBF Resolution-Based Calculi
• Proof complexity of resolution-based QBF calculi
• QBF Resolution Systems and Their Proof Complexities
• Resolution for quantified Boolean formulas
• Short proofs are narrow—resolution made simple
• Solving QBF with counterexample guided refinement
• Understanding Gentzen and Frege Systems for QBF
• Unified QBF certification and its applications

Cited in

(12)

• Shortening QBF proofs with dependency schemes
• Lower bound techniques for QBF expansion
• Building strategies into QBF proofs
• Lower bounds: from circuits to QBF proof systems
• Proof complexity of resolution-based QBF calculi
• A quasi-lower bound on the consistency strength of PFA
• scientific article; zbMATH DE number 7228403 (Why is no real title available?)
• Feasible interpolation for QBF resolution calculi
• Reasons for hardness in QBF proof systems
• Frege systems for quantified Boolean logic
• Feasible interpolation for QBF resolution calculi
• Proof Complexity of Quantified Boolean Logic — A Survey

Describes a project that uses

Uses Software

• QuBE++
• Quaffle
• QUBE
• CAQE
• RAReQS

This page was built for publication: Lower bound techniques for QBF proof systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3304096)