全局与局部宣告的逻辑

在本文中，我们引入了“全局与局部宣告逻辑”（GLAL），这是一种动态认知逻辑，具有两个不同的宣告算子——$[\phi]^+_A$ 和 $[\phi]^-_A$，它们以所有代理的集合 $Ag$ 的子集 $A$ 为索引——分别用于全局和局部宣告。边界情况 $[\phi]^+_{Ag}$ 对应于文献中已知的 $\phi$ 的公开宣告。与作为“模型转换器”的标准公开宣告不同，全局和局部宣告是“点态模型转换器”。特别是，由宣告引起的更新在模型的不同状态中可能是不同的。因此，由此产生的计算是模型的树，而不是典型的序列。我们语义的一个结果是，模态互模拟的状态在我们的逻辑中可能被区分。然后，我们提供了一个更强的互模拟概念，并证明它在 GLAL 中保持了模态等价性。此外，我们表明 GLAL 比带有公共知识的公开宣告逻辑严格更具表达能力。我们证明了 GLAL 中涉及动态与知识之间交互的广泛有效式，并表明 GLAL 的可满足性问题是可判定的。我们通过详细的认知场景来说明这一形式化机制。