Characterising tree-like Frege proofs for QBF

DOI10.1016/J.IC.2019.05.002MaRDI QIDQ2272983zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

lower boundsQBFproof complexityFrege systems

Mathematics Subject Classification ID

Complexity of proofs (03F20)

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

Cites work

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

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)