Single Step Tableaux for Modal Logics Computational Properties, Complexity and Methodology
Single Step Tableaux for Modal Logics Computational Properties, Complexity and Methodology
复制标题
模态逻辑的单步 Tableaux 计算属性、复杂性和方法
DOI：
--
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
F. Massacci
中科院分区：
文献类型：
--
作者：
F. Massacci
单步表（SST）是模态逻辑演算的基础，它将不同的特征和前缀表组合成一个简单的，模块化的，强分析的，有效的演算，适用于各种模态逻辑。本文给出了一些关于SST的计算结果（融合性、可判定性、空间复杂性、模块性等）并将SST与其他形式主义如翻译方法、模态分解和Gentzen型tableaux进行了比较。例如，它讨论了通过用更简单的终止检查代替循环检查技术来推导SST和基于预处理的方法的决策过程的可行性和不可行性。讨论了用SST等方法求有效性和逻辑结果的复杂性。SST搜索策略的最小条件被证明产生P空间（和NPTIME为S5和KD 45）的决策程序。本文还介绍了基本的正确性和完整性证明的建设方法。
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 P SPACE (and NPTIME for S5 and KD45) decision procedures. The paper also presents the methodology underlying the construction of the correctness and completeness proofs.