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.