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量化限制在仅公开宣布Boulean公式时,例如Box fi 直观地表示“在每次公开宣布布尔兰公式后,公式是真实的”。因此,这一逻辑可以称为Boolean任意公开宣布逻辑,BAPAL。BAPAL逻辑是这项工作的主题。与APAL的逻辑不同,BAPAL具有一条有鳍的分解性。此外,BAPAL至少没有像APAL那样表达出来。另一个关于BAPAL可裁量的主张被推迟到一份配套文件。
相关内容
微信扫码咨询专知VIP会员