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