• 马素霞

  马素霞

  清华大学
  在期刊界中查找
  在百度中查找
  在本站中查找
  
• 郑人杰

  郑人杰

  清华大学
  在期刊界中查找
  在百度中查找
  在本站中查找
  

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.