发表机构
IRIT, CNRS – INP – University of Toulouse; IHPST UMR 8590, CNRS – University Paris 1 Pantheon Sorbonne（图卢兹大学; 巴黎第一大学潘特翁-索邦大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种基于动态超矢列的动态认知逻辑演算，以结构方式统一表示认知事件，其逻辑规则可逆，结构规则和切割规则可容许，是唯一兼具经典S5基础和内在动态性的证明论演算。
AI 中文摘要
本文提出了一种基于动态超矢列的动态认知逻辑（DEL）演算，这是一种以纯结构且自然的方式捕捉认知模型动态性的新框架。我们用智能体索引和事件存储来丰富动态超矢列，从而对认知事件进行统一表示。由此产生的演算拥有一组可证明可逆的逻辑规则。此外，所有结构规则（包括收缩规则）以及切割规则都被证明是可容许的。最后，据我们所知，该演算是唯一既基于经典S5框架又本质上是动态的DEL证明论演算。
英文摘要
This paper proposes a calculus for Dynamic Epistemic Logic (DEL) based on dynamic hypersequents, a new framework for capturing the dynamics of epistemic models in a purely structural and natural way. We enrich dynamic hypersequents with agent indices and an event store, yielding a uniform representation of epistemic events. The resulting calculus enjoys a set of logical rules that are provably invertible. Moreover, all structural rules, including the contraction rules, as well as the cut-rule, are shown to be admissible. Finally, the calculus constitutes, to the best of our knowledge, the only proof-theoretic calculus for DEL that is both grounded in a classical S5 framework and inherently dynamic.
