A complexity gap for tree resolution

DOI10.1007/s00037-001-8194-yzbMath0994.03005MaRDI QIDQ1601038

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

satisfiability; propositional proof complexity; combinatorial principles; gap phenomenon; hard propositional tautologies; infinite mathematical theories; tree-resolution proofs

Mathematics Subject Classification ID

03B25: Decidability of theories and sets of sentences

03B35: Mechanization of proofs and logical operations

03B05: Classical propositional logic

68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)

03C13: Model theory of finite structures

03F20: Complexity of proofs

Related Items

Resolution and the binary encoding of combinatorial principles, LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE, Relativization makes contradictions harder for resolution, The limits of tractability in resolution-based propositional proof systems, Parameterized proof complexity, Cutting planes and the parameter cutwidth, On the Chvátal rank of the pigeonhole principle, 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, Parameterized Bounded-Depth Frege Is Not Optimal, Cutting Planes and the Parameter Cutwidth, Resolution Width and Cutting Plane Rank Are Incomparable