Using Resolution for Testing Modal Satisfiability and Building Models
Using Resolution for Testing Modal Satisfiability and Building Models
复制标题
使用分辨率测试模态可满足性和构建模型
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
R. Schmidt
中科院分区：
文献类型：
--
作者：
U. Hustadt;R. Schmidt
针对定义在交、并、逆闭合关系族上的多峰逻辑K(M)(∩，∪，⌣)，提出了一种基于翻译的归结决策过程。这些关系可以满足某些附加的框架性质。不同于以往基于排序求精的归结决策过程，我们的过程是基于选择求精的，其派生对应于表或序列证明系统的派生。这个过程的优点是，它既可以用作可满足性检查器，也可以用作模型构建器。我们证明了用我们的方法可以多项式地模拟表式和序列式证明系统。此外，有限模型属性还适用于许多扩展的模式逻辑。
This paper presents a translation-based resolution decision procedure for the multimodal logic K(m)(∩,∪,⌣) defined over families of relations closed under intersection, union, and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures that are based on ordering refinements, our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and as a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.