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.
翻译：以对公告进行量化的方式提出了各种公开宣布逻辑的扩展。 最著名的扩展被称为任意公开宣布逻辑, APAL。 它包含一种原始语言构建 Box phi 直观地表达“ 每次公开宣布公式后, 公式是真实的 。 ” 逻辑 APAL 是不可改变的, 它具有无限的分解性。 现在考虑将APAL 量化限制在仅公开宣布布尔兰公式时, 以便Box fi 直截了当地表示, “ 在每次公开宣布布尔兰公式后, 公式就是真实的 。 ” 因此, 这个逻辑可以称为 Boolean 任意公开宣布逻辑, BAPAL 。 逻辑 BAPAL 是这项工作的主题 。 不同于 APAL 的逻辑有鳍分解法化 。 另外, BAPAL 至少没有像 APAL 那样表达 。 另一个关于BAPAL 是可裁量的主张被推迟到配套文件 。
相关内容
微信扫码咨询专知VIP会员