paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Relevant S is Undecidable

相关逻辑 S 是不可判定的
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 2/10 · 论文是纯数学逻辑结果,证明半格相关逻辑 S 的不可判定性,与用户关注的静态分析、Agentic 程序、LLM 与形式化验证结合等方向没有直接关联。虽属逻辑与自动机理论,但不涉及程序分析、浮点/贝叶斯或工程落地。引用 4 inbox
Søren Brinck Knudstorp
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:证明半格相关逻辑 S 的判定问题不可判定,推翻其可判定猜想。

半格相关逻辑 S 由 Urquhart 于 1972/1973 年提出,其判定问题长期开放。尽管 Urquhart 1984 证明了许多相关逻辑不可判定,但这些技术未能处理 S,因而包括 Urquhart 2016 在内的专家猜测 S 可判定。本文通过将铺砖问题解释到 S 中,构造出从铺砖问题到 S 的归约,从而证明 S 的判定问题是不可判定的。这一结果否定了先前的可判定性猜想,表明 S 与许多相关逻辑一样不可判定,并为该类逻辑的判定性边界提供了新的反例。

问题
半格相关逻辑 S 自提出以来,其判定问题一直悬而未决;许多相关逻辑已被证明不可判定,但 S 未被既有技术覆盖,甚至被猜测可判定。
方法
作者通过将铺砖问题(tiling problem)解释/归约到 S 中,来证明 S 的不可判定性。
评估
该证明推翻了 S 可判定的猜想,表明 S 的判定问题是不可判定的。
原文摘要(Abstract)

Since the introduction of the semilattice relevant logic S by [Urquhart 1972, 1973], its decision problem has persisted as an open problem. [Urquhart 1984] showed that many relevant logics are undecidable, yet S eluded these techniques. Eventually, this led experts, including [Urquhart 2016], to conjecture that S is decidable. Contrary to this conjecture, by interpreting a tiling problem, we show that S is undecidable.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@inproceedings{Knudstorp24,
  title = {Relevant S is Undecidable},
  author = {Søren Brinck Knudstorp},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662128}
}