%0 Journal Article
%T 模拟boyer-moore定理证明器
%A 马素霞？
%A 郑人杰？
%J 软件学报
%P 39-45
%D 1990
%X sbmtp(simulateboyer-mooretheoremprover)系统是在ibm-pc-386微机上用gclisp语言实现的一个定理证明系统。该系统采用的思想方法和理论基础是boyer-moore的计算逻辑理论.sbmtp主要由三部分组成:知识库管理部分、定理证明部分及中断恢复部分。知识库管理部分包括一个基本知识库和一系列知识库构造工具。用户可根据具体问题灵活地组织自己所需要的知识库,定理证明部分采用启发式方法逐步推演,完成证明。中断恢复部分在证明产生中断的情况下提供了较强的恢复能力,提高了证明效率。
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=19900105&flag=1