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

Frege systemslower boundsproof complexityQBF

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Review text

The article is well organized, written, and clear. It combines strategy size with round-base strategy extraction algorithm in order to give a lower bound on any tree-like P+\(\forall\)red proof system, not only that, it is the only way to show such lower bound which does not require showing a lower bound for dag-like P+\(\forall\)red. On page 4, paragraph 1, there is a typo, instead of \(\forall\) reduction must be \(\forall\)-reduction. Finally, on page 4, Definition 5, it would be appropriate, in order to clarify, to give the explicit definition of \textit{range}, not only mention it, because the concept is used in the rest of the article many times.

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

• 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
• 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?)
• 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

(7)

• QBF as an alternative to Courcelle's theorem
• A game characterisation of tree-like Q-resolution size
• Understanding Gentzen and Frege Systems for QBF
• Frege systems for quantified Boolean logic
• Classes of hard formulas for QBF resolution
• Understanding the relative strength of QBF CDCL solvers and QBF resolution
• Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree

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)