###
DOI:
:1995.6(7):425-428

基于广义归结的定理机器证明系统
程晓春,孙吉贵,刘叙华
(吉林大学计算机科学系,长春,130023;吉林大学符号计算与知识工程开放实验室,长春,130023)
A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION
Cheng Xiaochun,Sun Jigui,Liu Xuhua
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 2563   Download 2893
Received:January 24, 1994    Revised:March 14, 1994
> 中文摘要: 本文使用C—PROLOG语言在SUN工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统GRM,RM,证明了《数学原理》中Part1:mathematicallogic中SectionA与SectionB中全部定理(350个).讨论GRM和RM的时、空复杂性,并在实现设计中提出新的全局调度策略及归结式的化简、排序策略,以单子句恒真、恒假的判断代替了广义归结中的自归结,实现了带OCCUR检查的模式匹配.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:本研究受国家自然科学基金、863计划和国家攀登计划的支持. 本研究受国家自然科学基金、863计划和国家攀登计划的支持.
Foundation items:
Reference text:

程晓春,孙吉贵,刘叙华.基于广义归结的定理机器证明系统.软件学报,1995,6(7):425-428

Cheng Xiaochun,Sun Jigui,Liu Xuhua.A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION.Journal of Software,1995,6(7):425-428