Single Step Tableaux for Modal Logics
Single Step Tableaux for Modal Logics
复制标题
模态逻辑的单步 Tableaux
DOI：
--
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
F. Massacci
中科院分区：
文献类型：
--
作者：
F. Massacci
单步表AUX(Single Step Tableaux，简称SST)是模态逻辑演算的基础，它结合了顺序表演算和前缀表演算的不同特点，形成了一种简单的、模块化的、强解析的、有效的模态逻辑演算。本文给出了关于SST(合流性、可判断性、空间复杂性、模块化等)的一些计算结果。并将SST与其他形式化方法如翻译方法、情态分解、Gentzen型场面等进行了比较。例如，讨论了用更简单的终止检查代替循环检查技术来推导SST和基于翻译的方法的决策过程的可行性和不可行性；讨论了SST和其他方法搜索有效性和逻辑推理的复杂性。证明了SST搜索策略的最小条件可以产生Pspace(对于S5和KD45则是NPtime)决策过程。文中还给出了构造正确性和完备性证明的方法。
Single Step Tableaux (SST) are the basis of a calculus for modal logics that combines different features of sequent and prefixed tableaux into a simple, modular, strongly analytic, and effective calculus for a wide range of modal logics.The paper presents a number of the computational results about SST (confluence, decidability, space complexity, modularity, etc.) and compares SST with other formalisms such as translation methods, modal resolution, and Gentzen-type tableaux. For instance, it discusses the feasibility and infeasibility of deriving decision procedures for SST and translation-based methods by replacing loop checking techniques with simpler termination checks.The complexity of searching for validity and logical consequence with SST and other methods is discussed. Minimal conditions on SST search strategies are proven to yield Pspace (and NPtime for S5 and KD45) decision procedures. The paper also presents the methodology underlying the construction of the correctness and completeness proofs.