【摘要】 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.更多还原