论文标题
非正态模态和脱发逻辑的高词计算：反模型和最佳复杂性
Hypersequent calculi for non-normal modal and deontic logics: Countermodels and optimal complexity
论文作者
论文摘要
我们为所有经典立方体的系统及其扩展的Axioms $ t $，$ p $，$ d $以及每一个$ n \ geq 1 $，规则$ rd^+_ n $提供了一些超股式微积分。该结石是内部的，因为它们仅采用逻辑的语言以及其他结构连接。我们表明，通过裁切消除的句法证明，对相应的公理化相对于相应的公理化是完整的。然后，我们基于超平衡的计算来定义终止终止的根本优先搜索策略，并表明它对于conp-Complete逻辑是最佳的。此外，我们从失败的证据的每一个饱和叶中获得，可以在双性化语义中定义根超平等的反模型，以及在关系语义中的常规逻辑。我们通过在经典立方体标记的系统中进行超陈述规则应用和推导之间的翻译来完成论文。
We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms $T$, $P$, $D$, and, for every $n\geq 1$, rule $RD^+_n$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatisation by a syntactic proof of cut elimination. Then we define a terminating root-first proof search strategy based on the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we obtain that from every saturated leaf of a failed proof it is possible to define a countermodel of the root hypersequent in the bi-neighbourhood semantics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.
