| 本文已被：浏览 4429次 下载 6063次 |
码上扫一扫！ |
|
|
| 基于广义归结的定理机器证明系统 |
|
程晓春1,2, 孙吉贵1,2, 刘叙华1,2
|
|
1.吉林大学计算机科学系,长春,130023;2.吉林大学符号计算与知识工程开放实验室,长春,130023
|
|
| 摘要: |
| 本文使用Ｃ—ＰＲＯＬＯＧ语言在ＳＵＮ工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统ＧＲＭ，ＲＭ，证明了《数学原理》中Ｐａｒｔ１：ｍａｔｈｅｍａｔｉｃａｌｌｏｇｉｃ中ＳｅｃｔｉｏｎＡ与ＳｅｃｔｉｏｎＢ中全部定理（３５０个）．讨论ＧＲＭ和ＲＭ的时、空复杂性，并在实现设计中提出新的全局调度策略及归结式的化简、排序策略，以单子句恒真、恒假的判断代替了广义归结中的自归结，实现了带ＯＣＣＵＲ检查的模式匹配． |
| 关键词: 广义归结，NC归结，OCCUR检查，调度策略 |
| DOI： |
| 分类号: |
| 基金项目:本研究受国家自然科学基金、863计划和国家攀登计划的支持. |
|
| A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION |
|
Cheng Xiaochun,Sun Jigui,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. |
| Key words: Generalized resolution, NC resolution, OCCUR check, schedule strategy. |
