论文标题
认识论行动的逻辑：完整性，可决定性，表现力
Logics for Epistemic Actions: Completeness, Decidability, Expressivity
论文作者
论文摘要
我们考虑了Baltag和Moss“认识论计划的逻辑”（2004）中所述的认知逻辑的动态版本。该论文提出了一种逻辑语言（实际上是由动作签名参数化的语言家族），以动态认知逻辑。已经表明，语言中的有效性为PI-1-1算法，因此没有递归的公理化完整逻辑系统。相比之下，本文证明了碎片无动作迭代的完整性结果，而没有动作迭代和常识的碎片的完整性结果。我们的工作涉及绕行术语重写理论。该参数使用模态过滤，因此我们获得了有限的模型属性，因此可以确定性。我们还将最大语言翻译成PDL，从而获得了第二个可决定性证明。纸张以表达能力的一些结果结束。这些主要关注的是将无动作的语言与传递闭合操作员增强的模态逻辑进行比较。我们通过改变动作签名来回答有关我们获得的语言的一个自然问题：我们证明，与操作员一起进行私人公告的逻辑语言比公开公告更有表现力。
We consider dynamic versions of epistemic logic as formulated in Baltag and Moss "Logics for epistemic programs" (2004). That paper proposed a logical language (actually families of languages parameterized by action signatures) for dynamic epistemic logic. It had been shown that validity in the language is Pi-1-1-complete, so there are no recursively axiomatized complete logical systems for it. In contrast, this paper proves a weak completeness result for the fragment without action iteration, and a strong completeness result for the fragment without action iteration and common knowledge. Our work involves a detour into term rewriting theory. The argument uses modal filtration, and thus we obtain the finite model property and hence decidability. We also give a translation of our largest language into PDL, thereby obtaining a second proof of decidability. The paper closes with some results on expressive power. These are mostly concerned with comparing the action-iteration-free language with modal logic augmented by transitive closure operators. We answer a natural question about the languages we obtain by varying the action signature: we prove that a logical language with operators for private announcements is more expressive than one for public announcements.
