Resolution lower bounds for the weak functional pigeonhole principle.

DOI10.1016/S0304-3975(02)00453-XzbMath1050.03039MaRDI QIDQ1401365

Alexander A. Razborov

Publication date: 17 August 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

complexity of proofs; resolution method

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03F20: Complexity of proofs

Related Items

Unnamed Item, Resolution and the binary encoding of combinatorial principles, Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs, Towards NP-P via proof complexity and search, Resolution lower bounds for perfect matching principles, The treewidth of proofs, Bounded-depth Frege complexity of Tseitin formulas for all graphs, Width versus size in resolution proofs, A combinatorial characterization of resolution width

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resolution proofs of generalized pigeonhole principles
• The intractability of resolution
• Resolution lower bounds for perfect matching principles
• Many hard examples for resolution
• Hard examples for resolution
• Short proofs are narrow—resolution made simple
• Pseudorandom Generators in Propositional Proof Complexity
• Regular resolution lower bounds for the weak pigeonhole principle
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory