Characterising tree-like Frege proofs for QBF

DOI10.1016/J.IC.2019.05.002zbMATH Open1459.03087OpenAlexW2944255969WikidataQ113872844 ScholiaQ113872844MaRDI QIDQ2272983FDOQ2272983

Authors: Olaf Beyersdorff, Luke Hinde 

Publication date: 17 September 2019

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2019.05.002

Recommendations

• Frege systems for quantified Boolean logic
• A game characterisation of tree-like Q-resolution size
• A game characterisation of tree-like Q-resolution size
• Lower bounds: from circuits to QBF proof systems
• Reasons for hardness in QBF proof systems

zbMATH Keywords

lower boundsQBFproof complexityFrege systems

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Cites Work

• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• On Unification of QBF Resolution-Based Calculi
• Proof complexity of resolution-based QBF calculi
• Title not available (Why is that?)
• Contributions to the theory of practical quantified Boolean formula solving
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The relative efficiency of propositional proof systems
• Short proofs are narrow—resolution made simple
• Towards NP-P via proof complexity and search
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Lower bounds: from circuits to QBF proof systems
• Understanding Gentzen and Frege Systems for QBF
• Title not available (Why is that?)
• Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness

Cited In (5)

• Understanding Gentzen and Frege Systems for QBF
• Frege systems for quantified Boolean logic
• Classes of hard formulas for QBF resolution
• QBF as an alternative to Courcelle's theorem
• A game characterisation of tree-like Q-resolution size

This page was built for publication: Characterising tree-like Frege proofs for QBF

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