paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Quantifying over Boolean announcements

对布尔公告的量化
LMCS vol.Volume 18, Issue 12022匹配度 1/10 · 该论文研究的是认知逻辑中的公开公告逻辑(APAL/BAPAL)的公理化与表达力问题,属于纯模态逻辑理论,与用户关注的静态分析、程序验证、浮点程序分析、贝叶斯程序分析及 LLM/Agent 交叉方向均无直接关联。用户虽偏好理论形式化工作,但本文的形式化对象是公告量化而非程序语义,缺少工程实现与落地场景。引用 21 inbox
Hans van Ditmarsch, Tim French
crossref: 2026-09-10

AI 速览

一句话:提出 BAPAL,将 APAL 的公告量化限制为布尔公式,给出有穷公理化并证明其表达力弱于 APAL。

公开公告逻辑 APAL 允许对任意公式的公开公告进行量化,但该逻辑不可判定且仅有无穷公理化。本文将量化范围限制为布尔公式,定义布尔任意公开公告逻辑 BAPAL,其中 Box φ 表示任意布尔公式公开公告后 φ 为真。工作给出 BAPAL 的有穷公理化,并证明 BAPAL 不至少与 APAL 一样有表达力,即其表达力弱于 APAL。可判定性结论则留待姊妹篇。该结果为公告量化提供了一种受布尔限制的折中,降低了公理化的复杂度。

问题
APAL 对任意公开公告进行量化,导致逻辑不可判定且只能无穷公理化;能否通过限制到布尔公告获得更易处理的逻辑?
方法
定义 BAPAL,其 Box 量词仅覆盖布尔公式的公开公告,并为该逻辑构造有穷公理化系统。
评估
通过逻辑证明与表达力比较,证明 BAPAL 具有有穷公理化,且其表达力弱于 APAL;可判定性留待伴随论文处理。
原文摘要(Abstract)

Various extensions of public announcement logic have been proposed with quantification over announcements. The best-known extension is called arbitrary public announcement logic, APAL. It contains a primitive language construct Box phi intuitively expressing that "after every public announcement of a formula, formula phi is true". The logic APAL is undecidable and it has an infinitary axiomatization. Now consider restricting the APAL quantification to public announcements of Boolean formulas only, such that Box phi intuitively expresses that "after every public announcement of a Boolean formula, formula phi is true". This logic can therefore called Boolean arbitrary public announcement logic, BAPAL. The logic BAPAL is the subject of this work. Unlike APAL it has a finitary axiomatization. Also, BAPAL is not at least as expressive as APAL. A further claim that BAPAL is decidable is deferred to a companion paper.

链接与引用

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

BibTeX
@article{paperbot1735,
  title = {Quantifying over Boolean announcements},
  author = {Hans van Ditmarsch and Tim French},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 1},
  year = {2022},
  doi = {10.46298/lmcs-18(1:20)2022}
}