In dynamic epistemic logic (Van Ditmarsch, Van Der Hoek, & Kooi, 2008) it is customary to use an action frame (Baltag & Moss, 2004; Baltag, Moss, & Solecki, 1998) to describe different views of a single action. In this article, action frames are extended to add or remove agents, we call these agent-update frames. This can be done selectively so that only some specified agents get information of the update, which can be used to model several interesting examples such as private update and deception, studied earlier by Baltag and Moss (2004); Sakama (2015); Van Ditmarsch, Van Eijck, Sietsma, and Wang (2012). The product update of a Kripke model by an action frame is an abbreviated way of describing the transformed Kripke model which is the result of performing the action. This is substantially extended to a sum-product update of a Kripke model by an agent-update frame in the new setting. These ideas are applied to an AI problem of modelling a story. We show that dynamic epistemic logics, with update modalities now based on agent-update frames, continue to have sound and complete proof systems. Decision procedures for model checking and satisfiability have expected complexity. For a sublanguage, there are polynomial space algorithms.
翻译:在动态认知逻辑(Van Ditmarsch, Van Der Hoek, & Kooi, 2008)中,通常使用动作框架(Baltag & Moss, 2004; Baltag, Moss, & Solecki, 1998)来描述单一动作的不同视角。本文将动作框架扩展为可添加或移除主体,称为主体更新框架。这种操作可选择性执行,使得仅特定主体获得更新信息,从而能够建模多个有趣案例,例如此前由Baltag与Moss(2004)、Sakama(2015)、Van Ditmarsch、Van Eijck、Sietsma与Wang(2012)研究的私有更新与欺骗行为。通过动作框架对克里普克模型进行乘积更新,是一种描述动作执行后变换所得克里普克模型的简化方式。本文在新框架下将其实质性地扩展为通过主体更新框架对克里普克模型进行和积更新。这些思想被应用于建模故事的人工智能问题。研究表明,基于主体更新框架的更新模态的动态认知逻辑仍具备可靠且完备的证明系统,模型检测与可满足性的判定算法具有预期复杂度,对于子语言存在多项式空间算法。