Relativization makes contradictions harder for resolution

DOI10.1016/j.apal.2013.10.009zbMath1277.68093arXiv1304.4287OpenAlexW2089789793MaRDI QIDQ386151

Barnaby Martin, Stefan S. Dantchev

Publication date: 16 December 2013

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1304.4287

zbMATH Keywords

lower boundsproof complexityparameterized proof complexityresolution-with-bounded-conjunction

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Analysis of algorithms (68W40) Complexity of proofs (03F20)

Related Items

Narrow Proofs May Be Maximally Long, Tight size-degree bounds for sums-of-squares proofs, The treewidth of proofs

Cites Work

• Parameterized proof complexity
• Combinatorics of first order structures and propositional proof systems
• The intractability of resolution
• A complexity gap for tree resolution
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• A characterization of tree-like resolution size
• Parametrized complexity theory.
• Proofs as Games
• Parameterized Bounded-Depth Frege Is not Optimal
• Relativisation Provides Natural Separations for Resolution-Based Proof Systems
• The relative efficiency of propositional proof systems
• Generating hard tautologies using predicate logic and the symmetric group
• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• Parameterized Resolution with Bounded Conjunction
• Computer Science Logic
• LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE
• Parameterized Complexity of DPLL Search Procedures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item