Resolution lower bounds for refutation statements

DOI10.4230/LIPICS.MFCS.2019.37MaRDI QIDQ5092398zbMATH OpenFDO

Authors Michal Garlík

Publication date 21 July 2022

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

zbMATH Keywords

proof complexityreflection principlesrefutation statementsresolution

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Random resolution refutations
• On the relative complexity of resolution refinements and cutting planes proof systems
• Random resolution refutations
• Monotone circuit lower bounds from resolution
• Lower bounds for k-DNF resolution on random 3-CNFs

Cites work

• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• A tradeoff between length and width in resolution
• NP search problems in low fragments of bounded arithmetic
• On Interpolation and Automatization for Frege Systems
• On reducibility and symmetry of disjoint NP pairs.
• On the automatizability of resolution and related propositional proof systems
• Proofs as Games
• The intractability of resolution
• The relative efficiency of propositional proof systems

Cited in

(6)

• Random resolution refutations
• Lower bounds and recursive methods for the problem of adjudicating conflicting claims
• Verifying Refutations with Extended Resolution
• Resolution Lower Bounds for Refutation Statements
• Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it
• Depth-d Frege systems are not automatable unless P\,=\,NP

This page was built for publication: Resolution lower bounds for refutation statements

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