paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Corrigendum: Unrealizability Logic

更正：Unrealizability Logic
POPL 10(POPL)2026匹配度 1/10 · 该论文是程序逻辑 Unrealizability Logic 的勘误，仅澄清健全性假设并修正完备性证明缺陷，属于纯形式逻辑/程序语言理论。它与用户关注的 PL↔AI、LLM/Agent 改进静态分析与形式化验证、浮点程序分析或贝叶斯程序分析等方向没有直接关联。引用 0 inbox
Jinwoo Kim, Loris D'Antoni, Thomas Reps
逻辑与自动机
crossref: 2026-09-10

AI 速览

一句话：澄清原文健全性陈述中的隐含假设，并修正其完备性证明中的缺陷。

本文是对发表于 POPL 2023 的论文《Unrealizability Logic》的更正。原文在陈述健全性（soundness）时隐含了一个未明确说明的假设，并且其完备性（completeness）证明存在一个缺陷。作者在 Shaan Nagy 的协助下发现了这两个问题。本更正澄清了健全性陈述中所做的假设，使该假设显式化，并修正了完备性证明中的错误。通过这一更正，原文的健全性与完备性结果得以在更严谨的基础上成立。该更正不改变原文的核心逻辑框架，仅对证明细节和前提条件进行必要的补充与修正。

问题
原文《Unrealizability Logic》的健全性陈述隐含了一个未声明的假设，且完备性证明存在缺陷，导致其理论结果的严谨性受到影响。
方法
作者识别并明确了健全性陈述中隐含的假设，并重新修正了完备性证明的缺陷部分。
评估
通过理论分析指出并修正原文证明中的问题，以更正形式呈现修正后的健全性陈述与完备性证明。
原文摘要（Abstract）

This is a corrigendum for the article "Unrealizability Logic" by Jinwoo Kim, Loris D’Antoni, and Thomas Reps, published in Proc. ACM Program. Lang. 7, POPL, Article 23 (January 2023), https://doi.org/10.1145/3571216. The authors, with the help of Shaan Nagy, discovered that there was an implicitly made assumption when stating soundness, and a flaw in the completeness proof of the original paper. This corrigendum clarifies the assumption made in the soundness statement and rectifies the completeness proof.

链接与引用

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

BibTeX 
@article{paperbot3865,
  title = {Corrigendum: Unrealizability Logic},
  author = {Jinwoo Kim and Loris D'Antoni and Thomas Reps},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3771762}
}