主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
程晓春,孙吉贵,刘叙华.基于广义归结的定理机器证明系统.软件学报,1995,6(7):425-428
基于广义归结的定理机器证明系统
A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION
投稿时间:1994-01-24  修订日期:1994-03-14
DOI:
中文关键词:  广义归结,NC归结,OCCUR检查,调度策略
英文关键词:Generalized resolution, NC resolution, OCCUR check, schedule strategy.
基金项目:本研究受国家自然科学基金、863计划和国家攀登计划的支持.
作者单位
程晓春 吉林大学计算机科学系,长春,130023
吉林大学符号计算与知识工程开放实验室,长春,130023 
孙吉贵 吉林大学计算机科学系,长春,130023
吉林大学符号计算与知识工程开放实验室,长春,130023 
刘叙华 吉林大学计算机科学系,长春,130023
吉林大学符号计算与知识工程开放实验室,长春,130023 
摘要点击次数: 2829
全文下载次数: 3059
中文摘要:
      本文使用C—PROLOG语言在SUN工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统GRM,RM,证明了《数学原理》中Part1:mathematicallogic中SectionA与SectionB中全部定理(350个).讨论GRM和RM的时、空复杂性,并在实现设计中提出新的全局调度策略及归结式的化简、排序策略,以单子句恒真、恒假的判断代替了广义归结中的自归结,实现了带OCCUR检查的模式匹配.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利