模拟Boyer-Moore定理证明器
基金项目:

SBMTP (Simulate Boyer-Moore Theorem Prover) system is a theorem proving system which is implemented on microcomputer IBM-PC-386 by GCLISP language. The concepts and theoretical basis of the system are computational logic by Boyer and Moore. SBMTP is made up of three parts mainly: knowledge base management subsystem, theorem proving subsystem and interrupt recovery subsystem. Knowledge base management subsystem includes a fundamental knowledge base and a series of knowledge base construction tools. User can organize fiexibly his knowledge base in accordance with specific requirements.Theorem proving subsystem employs a heuristic method for reasoning to complete proof.Interrupt recovery subsystem provides Powerful recovery ability when proof process gets interrupted.This subsystem imporoves proof efficiency of the system.


A SIMULATE BOYER-MOORE THEOREM PROVER
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [1]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    SBMTP(Simulate Boyer-Moore Theorem Prover)系统是在IBM-PC-386微机上用GCLISP语言实现的一个定理证明系统。该系统采用的思想方法和理论基础是Boyer-Moore的计算逻辑理论. SBMTP主要由三部分组成:知识库管理部分、定理证明部分及中断恢复部分。 知识库管理部分包括一个基本知识库和一系列知识库构造工具。用户可根据具体问题 灵活地组织自己所需要的知识库,定理证明部分采用启发式方法逐步推演,完成证明。中断恢复部分在证明产生中断的情况下提供了较强的恢复能力,提高了证明效率。

    Abstract:

    SBMTP(Simulate Boyer-Moore Theorem Prover) system is a theorem proving system which is implemented on microcomputer IBM-PC-386 by GCLISP language. The concepts and theoretical basis of the system are computational logic by Boyer and Moore. SBMTP is made up of three parts mainly: knowledge base management subsystem, theorem proving subsystem and interrupt recovery subsystem. Knowledge base management subsystem includes a fundamental knowledge base and a series of knowledge base construction tools. User can organize flexibly his knowledge base in accordance with specific requirements. Theorem proving subsystem employs a heuristic method for reasoning to complete proof. Interrupt recovery subsystem provides powerful recovery ability when proof process gets interrupted. This subsystem improves proof efficiency of the system.

    参考文献
    [l] 李卫华译。"计算逻辑",《计算机工程与应用》。1982,4-5.1983,7. [2] 李卫华。"定理证明与程序验证",《计算机科学》。1982.1. [3] D.I.Good,"Mechanical Proof About Computer Programs", Institute of Computing Science,The University of Texas at Austin, Austin,Texas 78712,U.S.A.,1984. [4] R.S.Boyer and J.S.Moore,"Proving Theorems About Lisp Functions",Journal of the Association for Computing M achinery, 1975. [5] Shmuel Kate,"PARIS:A System for Reusing Partially—Interpreted Schemas",MCC Software Technology Program,"Austin。Texas。1987. [6] D.I.Good,"An Interactive Program Verification System", IEEE Transaction on Software.Engincering, Vol.se-l,No.1,March 1975. [7] 李卫华译,"计算机科学中的正确性问题",《计算机工程与应用》。1984,10一11.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

马素霞,郑人杰.模拟Boyer-Moore定理证明器.软件学报,1990,1(1):39-45

复制
分享
文章指标
  • 点击次数:4866
  • 下载次数: 5413
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:1989-07-14
文章二维码
您是第19794055位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号