Are Short Proofs Narrow? QBF Resolution Is Not So Simple

DOI10.1145/3157053MaRDI QIDQ4608723zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil K. Shukla

Publication date 22 March 2018

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3157053

zbMATH Keywords

lower bound techniquesproof complexityQBFresolutionsimulations

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Recommendations

• Are Short Proofs Narrow? QBF Resolution is not Simple.
• Short proofs are narrow -- resolution made simple
• Short proofs in QBF expansion
• Short proofs are narrow—resolution made simple
• scientific article; zbMATH DE number 1361489
• Shortening QBF proofs with dependency schemes
• A simple proof of QBF hardness
• Shortening of proof length is elusive for theorem provers
• QBF Resolution Systems and Their Proof Complexities
• scientific article; zbMATH DE number 1324437

Cited in

(13)

• Relating size and width in variants of Q-resolution
• Lower bound techniques for QBF expansion
• Lower bounds for QCDCL via formula gauge
• Bounded-width QBF is PSPACE-complete
• Are Short Proofs Narrow? QBF Resolution is not Simple.
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• New resolution-based QBF calculi and their proof complexity
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
• Lower bounds for QCDCL via formula gauge
• Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree
• Proof complexity of modal resolution
• Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable

This page was built for publication: Are Short Proofs Narrow? QBF Resolution Is Not So Simple

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