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. It is decidable and it has a finitary axiomatization. These results may be considered of interest, as for various applications quantification over Booleans is sufficient in formal specifications.
翻译：以对公告进行量化的方式提出了各种公开宣布逻辑的扩展。 最著名的扩展称为任意公开宣布逻辑, APAL。 它包含一种原始语言构建 Box phi 直观表达“ 每次公开宣布公式后, 公式是真实的 。 ” 逻辑 APAL 是不可改变的, 它具有无限的分解性。 现在考虑将 APAL 量化限于仅公开宣布布尔兰公式, 这样Box fi 直截了当地表示 : “ 每次公开宣布布尔兰公式后, 公式就是真实的 。 因此, 这个逻辑可以称为布尔兰任意公开宣布逻辑, BAPAL 。 逻辑 BAPAL 是这项工作的主题 。 它是分解的, 它具有一种有鳍分解法的分解性。 这些结果可能被认为是值得注意的, 因为对布洛伦人的各种应用的量化在正式的规格中已经足够了 。
相关内容
微信扫码咨询专知VIP会员