将超序列嫁接到嵌套序列上
Grafting Hypersequents onto Nested Sequents
AI总结：
本文提出结合嵌套序列与超序列的嫁接超序列框架，为K5、KD5等模态逻辑提供具备语法切消和最优复杂度证明搜索的新型演算。
摘要：
我们引入了一种新的Gentzen风格的嫁接超序列（grafted hypersequents）框架，该框架将嵌套序列（nested sequents）的形式体系与超序列（hypersequents）相结合。为了说明该框架的潜力，我们为模态逻辑$\mathsf{K5}$和$\mathsf{KD5}$，以及带有移位自反性公理的模态逻辑$\mathsf{K}$和$\mathsf{KD}$的扩展提出了新的演算。在道义逻辑语境中，后一种扩展也被称为$\mathsf{SDL}^+$。我们所有的演算都享有语法切消（cut elimination），并且可用于最优复杂度的反向证明搜索过程。$\mathsf{K5}$和$\mathsf{KD5}$演算的表化（tableaufication）为这些逻辑产生了简化的前缀表推演算，让人联想到$\mathsf{S5}$的简化表系统，这可能具有独立的研究价值。
英文摘要：
We introduce a new Gentzen-style framework of grafted hypersequents that combines the formalism of nested sequents with that of hypersequents. To illustrate the potential of the framework, we present novel calculi for the modal logics $\mathsf{K5}$ and $\mathsf{KD5}$, as well as for extensions of the modal logics $\mathsf{K}$ and $\mathsf{KD}$ with the axiom for shift reflexivity. The latter of these extensions is also known as $\mathsf{SDL}^+$ in the context of deontic logic. All our calculi enjoy syntactic cut elimination and can be used in backwards proof search procedures of optimal complexity. The tableaufication of the calculi for $\mathsf{K5}$ and $\mathsf{KD5}$ yields simplified prefixed tableau calculi for these logic reminiscent of the simplified tableau system for $\mathsf{S5}$, which might be of independent interest.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
