A complexity gap for tree resolution

DOI10.1007/S00037-001-8194-YMaRDI QIDQ1601038zbMATH OpenOpenAlexFDO

Authors Søren Riis

Publication date 17 June 2002

Published in Computational Complexity (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00037-001-8194-y

zbMATH Keywords

combinatorial principlesgap phenomenonhard propositional tautologiesinfinite mathematical theoriespropositional proof complexitysatisfiabilitytree-resolution proofs

Mathematics Subject Classification ID

Classical propositional logic (03B05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Model theory of finite structures (03C13) Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Computer Science Logic
• The intractability of resolution
• Short proofs are narrow -- resolution made simple
• Finding a tree structure in a resolution proof is NP-complete
• Short proofs are narrow—resolution made simple

Cited in

(25)

• Finding a tree structure in a resolution proof is NP-complete
• On the Chvátal rank of the pigeonhole principle
• A lower bound for tree resolution
• Towards a unified complexity theory of total functions
• Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems
• The treewidth of proofs
• Partially definable forcing and bounded arithmetic
• A combinatorial characterization of resolution width
• Computing Resolution-Path Dependencies in Linear Time ,
• A formal proof of Borodin-Trakhtenbrot's gap theorem
• Parameterized bounded-depth Frege is not optimal
• Cutting planes and the parameter cutwidth
• Resolution Width and Cutting Plane Rank Are Incomparable
• Relativization makes contradictions harder for resolution
• The limits of tractability in resolution-based propositional proof systems
• Parameterized proof complexity
• scientific article; zbMATH DE number 1522926 (Why is no real title available?)
• Resolution and the binary encoding of combinatorial principles
• scientific article; zbMATH DE number 7238987 (Why is no real title available?)
• Computer Science Logic
• Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
• Near optimal seperation of tree-like and general resolution
• Proof complexity and the binary encoding of combinatorial principles
• Cutting planes and the parameter cutwidth
• Resolution over linear equations: combinatorial games for tree-like size and space

This page was built for publication: A complexity gap for tree resolution

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