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.
翻译:Buss、Kolodziejczyk和Thapen(JSL,2014年)定义的随机解析(随机解析 ), 是一个健全的假设证明系统, 扩展解析验证系统, 从而有可能通过一套随机选择的条款( 技术条件的模版) 来增加任何一套初始条款。 我们展示了如何应用通用可行的内插理论来随机解析克拉伊切克语义衍生( JSL,1997年) 。 因此, 我们获得的分色公式随机解析的下限 。