| 一种新的模态归结 |
| |
| 引用本文： | 潘维民 陈图云. 一种新的模态归结[J]. 计算机学报, 1997, 20(8): 711-717 |
| |
| 作者姓名： | 潘维民 陈图云 |
| |
| 作者单位： | [1]中国科学院计算技术研究所 [2]辽宁师范大学数学系 |
| |
| 摘 要： | 本文首先给出了一种标准子句的定义，在其基础上定义了命题模态逻辑系统Ｓ５的子句集的可归结形式。证明了任意模态Ｓ５子句集不可满足的充要条件为在其可归结形式上可归结出空子句。
|
| 关 键 词： | 模态归结 可归结形式 二元归结式 逻辑设计 |
A NEW STRATEGY OF MODAL RESOLUTION |
| |
| PAN Weimin. A NEW STRATEGY OF MODAL RESOLUTION[J]. Chinese Journal of Computers, 1997, 20(8): 711-717 |
| |
| Authors: | PAN Weimin |
| |
| Abstract: | This paper gives the concept of standard clauses set and defines resolvable form of a clauses set. The soundness and completeness of modal resolution onresolvable form with respect to propositional modal logic system S5 is proved. |
| |
| Keywords: | Modal resolution resolvable form binary resolvent. |
| 本文献已被 CNKI 维普 等数据库收录！ |
