模拟boyer-moore定理证明器

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