| 基于广义归结的定理机器证明系统 |
| |
| 引用本文： | 程晓春,孙吉贵,刘叙华.基于广义归结的定理机器证明系统[J].软件学报,1995,6(7):425-428. |
| |
| 作者姓名： | 程晓春 孙吉贵 刘叙华 |
| |
| 作者单位： | 吉林大学计算机科学系,长春,130023;吉林大学符号计算与知识工程开放实验室,长春,130023;吉林大学计算机科学系,长春,130023;吉林大学符号计算与知识工程开放实验室,长春,130023;吉林大学计算机科学系,长春,130023;吉林大学符号计算与知识工程开放实验室,长春,130023 |
| |
| 基金项目： | 本研究受国家自然科学基金、863计划和国家攀登计划的支持. |
| |
| 摘 要： | 本文使用Ｃ—ＰＲＯＬＯＧ语言在ＳＵＮ工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统ＧＲＭ,ＲＭ,证明了《数学原理》中Ｐａｒｔ１：ｍａｔｈｅｍａｔｉｃａｌｌｏｇｉｃ中ＳｅｃｔｉｏｎＡ与ＳｅｃｔｉｏｎＢ中全部定理（３５０个）．讨论ＧＲＭ和ＲＭ的时、空复杂性,并在实现设计中提出新的全局调度策略及归结式的化简、排序策略,以单子句恒真、恒假的判断代替了广义归结中的自归结,实现了带ＯＣＣＵＲ检查的模式匹配．
|
| 关 键 词： | 广义归结 NC归结 OCCUR检查 调度策略 |
| 收稿时间： | 1994/1/24 0:00:00 |
| 修稿时间： | 1994/3/14 0:00:00 |
A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION |
| |
| Cheng Xiaochun,Sun Jigui and Liu Xuhua.A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION[J].Journal of Software,1995,6(7):425-428. |
| |
| Authors: | Cheng Xiaochun Sun Jigui and Liu Xuhua |
| |
| Abstract: | The authors prove 350 theorems of "Principia Mathematica" by a theorem proving system based on generalized resolution. Compared it with traditional resolution,they complement new strategy, avoid self-resolution, and discuss its time and space complexity. |
| |
| Keywords: | Generalized resolution NC resolution OCCUR check schedule strategy |
| 本文献已被 CNKI 维普 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
