具有全局模态和角色层次的分级混合逻辑的终止表

通过翻译与表列法研究带递归的模态逻辑的复杂性结果

Complexity results for modal logic with recursion via translations and tableaux

本文通过逻辑间翻译迁移复杂性结果，为带递归的多智能体模态逻辑构建表列系统并将其可满足性归约为μ-演算可满足性，得到通用2EXP上界。

具有联结器、传递关系和关系层次的多模态混合逻辑的表格

Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies

在以前的文件中，已经提出了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作扩展了这样的演算多模态逻辑与传递关系和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。所考虑的逻辑的终止，声音和完整的演算的存在证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑产生可判定的逻辑。

ExpTime表，具有用于描述逻辑SHOQ的全局缓存

ExpTime Tableaux with Global Caching for the Description Logic SHOQ

我们给出了第一个ExpTime（复杂性最优）的tableau决策过程，用于检查描述逻辑SHOQ中知识库的可满足性，它扩展了基本描述逻辑ALC，具有传递角色，角色层次，名词和量化数量限制。复杂度是用一元数表示来衡量的。我们的程序是基于全局缓存和整数线性可行性检查。

Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction

A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of…

描述逻辑SHI中知识库可满足性检验的无割ExpTime表

Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI

我们给出了第一个无割ExpTime（最优）Tableau决策过程，用于检查描述逻辑SHI中的知识库的可满足性，它扩展了描述逻辑ALC的传递角色，逆角色和角色层次。

直觉主义模态逻辑：FIK与LIK的全新且更简洁的可判定性证明

Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK

本研究整合模态逻辑终止表方法与直觉主义模态逻辑IK的有穷框架性质，为FIK和LIK给出更简洁的全新可判定性证明。