Logics for Epistemic Programs
Logics for Epistemic Programs
复制标题
DOI：
10.1023/b:synt.0000024912.56773.5e
复制
发表时间：
2004-03
期刊：
影响因子：
1.5
通讯作者：
A. Baltag;L. Moss
中科院分区：
文献类型：
--
作者：
A. Baltag;L. Moss
我们构造了逻辑语言，允许人们表示影响多智能体设置中智能体信息状态的各种可能类型的变化。我们通过定义认知程序的概念来形式化这些变化。语言是两个排序的集合，其中不仅包含句子，还包含动作或程序。这就像在动态逻辑中一样，事实上，我们的语言并不比动态逻辑复杂得多。但语义要复杂得多。一般而言，认知程序的语义就是我们所说的程序模型。这是一个“动作”的Kriske模型，表示代理对当前操作的不确定性，类似于认知逻辑中通常使用的“状态”的Krigke模型表示代理对系统当前状态的不确定性。程序模型导致影响代理信息的变化，我们将其表示为状态模型的变化，称为动态更新。形式上，更新由两个操作组成：第一个操作称为更新映射，它将每个状态模型带到另一个状态模型，称为更新模型；第二个操作为每个输入状态模型，给出该模型的状态和更新模型的状态之间的转换关系。每种认知动作，如公开声明或完全私密的对组的声明，都给出了我们所说的动作签名，然后每个动作签名家族给出了一种逻辑语言。这些语言的构建是本文的主要议题。我们还提到了捕获我们的逻辑的有效句子的系统。但我们对完备性的证明另有规定，语义中使用的基本运算称为更新乘积。Baltag等人提出了这一观点的一个版本。(1998)，这里的演示文稿比前一篇有所改进。更新产品用于从任何程序模型获得相应的认知更新，从而允许我们计算信息或信念的变化。这一点与我们的逻辑语言无关。我们在整篇文章中用许多例子来说明更新产品和我们的逻辑语言。
We construct logical languages which allow one to represent a variety of possible types of changes affecting the information states of agents in a multi-agent setting. We formalize these changes by defining a notion ofepistemic program. The languages are two-sorted sets that contain not only sentences but also actions or programs. This is as in dynamic logic, and indeed our languages are not significantly more complicated than dynamic logics. But the semantics is more complicated. In general, the semantics of an epistemic program is what we call aprogram model. This is a Kripke model of ‘actions’,representing the agents'uncertainty about the current actionin a similar way that Kripke models of ‘states’ are commonly used in epistemic logic to represent the agents'uncertainty about the current stateof the system. Program models induce changes affecting agents' information, which we represent as changes of the state model, calledepistemic updates. Formally, an update consists of two operations: the first is called the update map, and it takes every state model to another state model, called theupdated model; the second gives, for each input state model, a transition relation between the states of that model and the states of the updated model.Each variety of epistemic actions, such as public announcements or completely private announcements to groups, gives what we call anaction signature, and then each family of action signatures gives a logical language. The construction of these languages is the main topic of this paper. We also mention the systems that capture the valid sentences of our logics. But we defer to a separate paper the completeness proof.The basic operation used in the semantics is called theupdate product. A version of this was introduced in Baltag et al. (1998), and the presentation here improves on the earlier one. The update product is used to obtain from any program model the corresponding epistemic update, thus allowing us tocomputechanges of information or belief. This point is of interest independently of our logical languages. We illustrate the update product and our logical languages with many examples throughout the paper.