paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A limitation on the KPT interpolation

KPT 插值的一个局限性
LMCS vol.Volume 16, Issue 32020匹配度 1/10 · 该论文属于命题证明复杂性与插值定理的理论研究，讨论 KPT 插值变体的局限性，与用户关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关联。虽然涉及逻辑与形式化证明，但研究目标不是程序分析或验证工具，也未结合 LLM。引用 2 inbox
Jan Krajíček
逻辑与自动机
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：证明 Pich 和 Santhanam 提出的 KPT 插值变体对一类能证明难以区分的 NP 集合不相交的命题证明系统存在局限。

本文研究命题证明系统中 KPT 插值定理的一个变体。Pich 和 Santhanam（2020）曾针对命题证明系统提出该变体。Krajíček 证明：对于所有能够证明两个难以区分的 NP 集合不相交（disjointness）的证明系统，该 KPT 插值变体都存在局限。该结果给出了一般性的否定性结论，表明这一 KPT 型插值方法不能适用于此类证明系统，从而限制了其在证明复杂度与插值方法中的适用范围。

问题
研究 Pich 和 Santhanam（2020）为命题证明系统提出的 KPT 插值变体是否普遍适用。
方法
通过证明复杂度与逻辑方法，分析该插值变体在能够证明两个难以区分的 NP 集合不相交的证明系统中的表现。
评估
理论证明：对所有此类证明系统给出 KPT 插值变体的局限性结果。
原文摘要（Abstract）

We prove a limitation on a variant of the KPT theorem proposed for propositional proof systems by Pich and Santhanam (2020), for all proof systems that prove the disjointness of two NP sets that are hard to distinguish.

链接与引用

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

BibTeX 
@article{abs-2004-02448,
  title = {A limitation on the KPT interpolation},
  author = {Jan Krajíček},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:9)2020}
}