Abstract:
The IGTP(Intelligent Geometry Theorem Prover)is a CAI system for teaching plane geometry.This system consists of two parts:One is program PROVER,another one is program AUTOBASE.The PROVER is a program to prove plane geometry theorem.Its algorithm and implementation is given in2.The program AUTOBASE automatically establishes and modifies geometry knowledge base.Its algorithm and implementation is given in this paper.The system AUTOBASE could learn proving rules from text of proofs given by the user,modify and merge them by comparing with axioms,theorems,and proving rules that have been put in the base before,and establish a suitable knowledge base used in proving geometry problems.The system(PROVER and AUTOBASE)has been implemented in the computer CROMEMCO.Some examples given by the AUTOBASE are listed in the appendixes.