Research And Development Of Machine Proving System On Geometry Theorem

Generally, the proving of geometry theorem is based on the axiom system, and is deducted according to certain logic rules. Different theorem has different proving method, and no common ways or ideas can be used for all theorems or even for a certain class. So it can't be comprehended by analogy for proving, and can only be put into reality by experience and precise logical judgment capability.With the foundation of Mr. Wu wenjun's method of mathematical mechanization, the mechanical proving and calculating are put into reality in many fields of math. This mechanical method, called Wu's method, is especially well applied into the Mechanical Geometry Theorem Proving, which is a proving method based on the structural geometry algebra theorem, and breaks a new path for the proving of geometry theorem.This paper mainly discusses the mechanical proving of elementary geometry based on the Wu' s method, including:developing a software system using this method to prove theorem based on the Maple and Matlab.validating the system using large amount of theorems. making deep researches on the key problems during the process of proving.