| 模态逻辑D演绎过程的化简规则 |
| |
| 引用本文： | 程晓春,孙吉贵,刘叙华.模态逻辑D演绎过程的化简规则[J].吉林大学学报(理学版),1995(2). |
| |
| 作者姓名： | 程晓春 孙吉贵 刘叙华 |
| |
| 作者单位： | 吉林大学符号计算与知识工程开放实验室 |
| |
| 基金项目： | 国家自然科学基金，“863”计划和国家攀登计划资助课题 |
| |
| 摘 要： | 以分析模态逻辑中文字公式的极性为基础，将经典逻辑的Ｄａｖｉｓ－ｐｕｔｎａｍ纯文字化简规则推广到了命题模态逻辑Ｄ系统的自动演绎中，并给出了一些刻划Ｄ逻辑自动演绎特征的化简规则，这些化简规则通过对公式、子公式和公式集的有效性（或不可满足性）的有条件的判断，进行证明过程的剪枝和化简，以提高Ｄ逻辑自动演绎的效率；这些化简规则都是依据公式（集）本身的结构特征，可用于Ｄ逻辑的任意一种推理实现系统，在机器上是容易实现的。
|
| 关 键 词： | 模态逻辑D系统，化简规则，Tableau方法 |
The Reducing Rules of Deducing ProceduRe in Modal Logic D |
| |
| Cheng Xiaochun, Sun Jigui, Liu Xuhua.The Reducing Rules of Deducing ProceduRe in Modal Logic D[J].Journal of Jilin University: Sci Ed,1995(2). |
| |
| Authors: | Cheng Xiaochun Sun Jigui Liu Xuhua |
| |
| Abstract: | This paper generalizes the classical Davis-putnam pure literal rules to propositional modallogic D and presents some reducing rules that describe the characters of the deducing procedure inmodal logic D. These reducing rules simplify the proof search tree by checking up the validity(or un-satisfiability)of the formulae under certain conditions so as to improve the efficiency of the deductionin modal logic D. Based on the structure characters of the formulae,these reducing rules can be usedin any automatic reasoning system of modal logic D,and can be implemented easily. |
| |
| Keywords: | modal logic D reducing rules Tableau method |
| 本文献已被 CNKI 等数据库收录！ |
