| Cialdea一阶模态归结系统的不完备性及其改进 |
| |
| 引用本文： | 孙吉贵,刘叙华.Cialdea一阶模态归结系统的不完备性及其改进[J].计算机学报,1995,18(6):401-408. |
| |
| 作者姓名： | 孙吉贵 刘叙华 |
| |
| 作者单位： | 吉林大学计算机科学系 |
| |
| 基金项目： | 国家自然科学基金,863计划资助,国家攀登计划资助 |
| |
| 摘 要： | Ｃｉａｌｄｅａ的－阶模态Ｄ逻辑归结系统具有符号冗余较少和机器上较容易实现等优点，但它是不完备的。本文中，我们改进了Ｃｉａｌｄｅａ归结系统，引入了两个可能算子约束的公式间的归结规则，得到了一种新的一阶模态Ｄ逻辑的归结系统，记为ＦＭＲＤ．ＦＭＲＤ很好地保持了Ｃｉａｌｄｅａ归结系统的优点，同时，我们证明了ＦＭＲＤ的可靠性与完备性。
|
| 关 键 词： | FMRD归结 自动推理 模态归结系统 不完备性 |
THE INCOMPLETENESS AND AN IMPROVEMENT OF CIALDEA'S RESOLUTION SYSTEM FOR FIRST-ORDER MODAL LOGIC |
| |
| Sun Jigui,and Liu Xuhua.THE INCOMPLETENESS AND AN IMPROVEMENT OF CIALDEA''''S RESOLUTION SYSTEM FOR FIRST-ORDER MODAL LOGIC[J].Chinese Journal of Computers,1995,18(6):401-408. |
| |
| Authors: | Sun Jigui and Liu Xuhua |
| |
| Abstract: | Cialdea's resolution system for first-order modal logic D is incomplete, although it has less notational redundancy and is easier in implementation.We improve Cialdea's resolution system, lead into a resolution rule between two formulas which bound by possible operator, and obtain a new resolution system for first-order medal logic D, denoted as FMRD. FMRD retain the advantages of Cialdea's resolution system good enough. At the same time, we prove the soundness and the completeness of FMRD. |
| |
| Keywords: | First-order modal system D FMRD resolution method automated reasoning |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
