箭更新综合
计算机科学中的逻辑
2021-11-30 v3
摘要
本文给出任意箭更新模型逻辑（AAUML）。这是一种动态认知逻辑或更新逻辑。在更新逻辑中，静态/基本模态在给定关系模型上解释，而动态/更新模态诱导关系模型的变换（更新）。在 AAUML 中，更新模态形式化了箭更新模型的执行，并且还存在一个对箭更新模型进行量化的模态。箭更新模型是众所周知的动作模型的替代方案。我们给出了 AAUML 的公理化。该公理化是一个重写系统，可从任意给定公式中消除箭更新模态，同时保持真值。因此，AAUML 是可判定的，且与基础多智能体模态逻辑具有相同的表达能力。我们的主要结果是确立箭更新综合：若存在某个箭更新模型使得其后 phi 成立，我们便能从 phi 构造（综合）出该模型。我们还指出了箭更新逻辑、动作模型逻辑与精化模态逻辑在更新表达能力上的一些显著区别。
引用
@article{arxiv.1802.00914,
title = {Arrow Update Synthesis},
author = {Hans van Ditmarsch and Wiebe van der Hoek and Barteld Kooi and Louwe B. Kuijer},
journal= {arXiv preprint arXiv:1802.00914},
year = {2021}
}