Strategies for modal resolution: Results and problems
Strategies for modal resolution: Results and problems
复制标题
模态解决策略：结果和问题
DOI：
--
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
Jean
中科院分区：
文献类型：
--
作者：
Y. Auffray;P. Enjalbert;Jean
本文讨论模态逻辑中归结策略的定义问题。我们提出了以下策略：删除所包含的子句，基于静态约束的经典策略的扩展，负分辨率，输入和线性分辨率。证明了一类基于静态约束的策略和线性策略是完备的。对于输入策略和否定策略，我们得到了完备性结果，并对所考虑的子句的类提供了一些限制。一些问题，如删除包含条款的完全性，是悬而未决的，我们的陈述和讨论的文件。
This paper is concerned with the definition of strategies for resolution in modal logic. We propose the following strategies: deletion of subsumed clauses, extensions of classical strategies based on a static constraint, negative resolution, input and linear resolution. A class of strategies based on static constraints and the linear strategy are proved to be complete. For input and negative strategy we have completeness results provided some restrictions on the class of considered clauses. Some problems such as completeness of deletion of subsumed clauses are left open; we state and discuss them in the paper.