paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A feasible interpolation for random resolution

随机归结的可行插值
LMCS vol.Volume 13, Issue 12017匹配度 1/10 · 该论文研究随机归结系统的可行插值与证明复杂度下界，属于逻辑与证明复杂度理论，未涉及程序静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析，与用户研究方向基本无关。引用 1 inbox
Jan Krajicek
定理证明与证明工程逻辑与自动机
crossref: 2026-09-10

AI 速览

一句话：将语义推导的可行插值定理应用于随机归结，并由此得到团-着色公式随机归结反驳的下界。

随机归结是 Buss、Kołodziejczyk 和 Thapen 提出的一种可靠命题证明系统：它在归结基础上允许把随机选取的子句（在特定技术条件下）加入初始子句集。本文研究如何为该系统建立可行插值，即把 Krajíček 关于语义推导的一般可行插值定理应用到随机归结。作为推论，作者证明了团-着色公式不存在短的随机归结反驳，给出了该类公式随机归结复杂度的下界。

问题
随机归结是否具有可行插值性质，以及能否借此获得具体公式类（如团-着色公式）的证明复杂度下界。
方法
将 Krajíček (1997) 对语义推导的一般可行插值定理专门化并应用于随机归结。
评估
通过理论推导给出团-着色公式随机归结反驳的复杂度下界，属于证明复杂度结果而非实验评估。
原文摘要（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.Comment: Preprint April 2016, revised September and October 2016

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot208,
  title = {A feasible interpolation for random resolution},
  author = {Jan Krajicek},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 1},
  year = {2017},
  doi = {10.23638/lmcs-13(1:5)2017}
}