基于广义归结的定理机器证明系统

本文使用Ｃ—ＰＲＯＬＯＧ语言在ＳＵＮ工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统ＧＲＭ，ＲＭ，证明了《数学原理》中Ｐａｒｔ１：ｍａｔｈｅｍａｔｉｃａｌｌｏｇｉｃ中ＳｅｃｔｉｏｎＡ与ＳｅｃｔｉｏｎＢ中全部定理（３５０个）．讨论ＧＲＭ和ＲＭ的时、空复杂性，并在实现设计中提出新的全局调度策略及归结式的化简、排序策略，以单子句恒真、恒假的判断代替了广义归结中的自归结，实现了带ＯＣＣＵＲ检查的模式匹配