paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the consistency of stronger lower bounds for NEXP

论 NEXP 更强下界的一致性
LMCS vol.Volume 21, Issue 42025匹配度 1/10 · 论文研究计算复杂性下界与有界算术中的一致性证明，属于逻辑/证明论方向，与用户关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无明显交叉。引用 1 inbox
Neil Thapen
逻辑与自动机定理证明与证明工程
crossref: 2026-09-10

AI 速览

一句话：将 Atserias 等人的方法推广，证明 NEXP ⊄ EXP/poly 与 NEXP ⊄ coNEXP 在更强有界算术理论中一致。

本文关注复杂性理论中的非包含猜想能否在有界算术中保持一致性。此前 Atserias、Buss 和 Mueller 证明了标准猜想 NEXP ⊄ P/poly 与较强有界算术理论 V^0_2 一致，而 V^0_2 已能形式化相当一部分复杂性理论。作者观察到他们的方法可以推广：在一个更强的理论中，该理论包含所有为真的全称数排序句子，可以证明更强的猜想 NEXP ⊄ EXP/poly 和 NEXP ⊄ coNEXP 同样与该理论一致。这表明这些更强的 NEXP 下界假设不会被该有界算术理论反驳，从而扩展了强下界猜想与形式化复杂性理论之间相对一致性的范围。

问题
研究更强的 NEXP 下界猜想（NEXP ⊄ EXP/poly 和 NEXP ⊄ coNEXP）能否与包含所有真全称数排序句子的强有界算术理论一致。
方法
沿用并推广 Atserias、Buss 和 Mueller 的一致性证明方法，在更强的有界算术理论中进行论证。
评估
这是理论证明工作：通过证明上述两个猜想相对于更强有界算术理论的一致性来评估原方法的可扩展性，不涉及实验。
原文摘要（Abstract）

It was recently shown by Atserias, Buss and Mueller that the standard complexity-theoretic conjecture NEXP not in P / poly is consistent with the relatively strong bounded arithmetic theory V^0_2, which can prove a substantial part of complexity theory. We observe that their approach can be extended to show that the stronger conjectures NEXP not in EXP / poly and NEXP not in coNEXP are consistent with a stronger theory, which includes every true universal number-sort sentence.

链接与引用

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

BibTeX 
@article{Thapen25,
  title = {On the consistency of stronger lower bounds for NEXP},
  author = {Neil Thapen},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 4},
  year = {2025},
  doi = {10.46298/lmcs-21(4:23)2025}
}