pith. sign in

arxiv: 1604.06560 · v5 · pith:K7WJWDCBnew · submitted 2016-04-22 · 🧮 math.LO · cs.CC

A feasible interpolation for random resolution

classification 🧮 math.LO cs.CC
keywords resolutionrandomclausesfeasibleinterpolationproofsystemapply
0
0 comments X
read the original abstract

Random resolution, defined by Buss, Kolodziejczyk and Thapen (JSL, 2014), is a sound propositional proof system that extends the resolution proof system by the possibility to augment any set of initial clauses by a set of randomly chosen clauses (modulo a technical condition). We show how to apply the general feasible interpolation theorem for semantic derivations of Krajicek (JSL, 1997) to random resolution. As a consequence we get a lower bound for random resolution refutations of the clique-coloring formulas.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.