几何定理的机器证明(定稿).docxVIP

Mechanical Theorem Proving in Geometry Gao Jun-yu*, Zhang Cheng-dong Cangzhou Normal University Hebei province,Cangzhou city,College Road, 061001. 0317-2159865 e-mail: gaojunyu8818@126.com Abstract Mechanical theorem proving in geometry plays an important role in the research of automated reasoning. In this paper, we introduce three kinds of computerized methods for geometrical theorem proving: the first is Wu’ s method in the international community, the second is elimination point method and the third is lower dimension method.? Keywords： geometric theorem, Wu’s method, elimination point method, lower dimension method ? Copyright ? 2012 Universitas Ahmad Dahlan. All rights reserved. 1. Introduction Mechanical Proving, that is, mechanization method, is to find a method which can be computed steeply step according to a certain rules. Today we usually refer it as algorithm. The algorithm is applied in the computer programming, mathematical mechanization, and mathematical theorems, This realizes mathematical theorem to be proved with computer. Mathematics in ancient China is nearly a kind of mechanic mathematics. Today, the method of Cartesian coordination gives this direction a solid step, and provides a simple and clear method for the proof of geometric?theorems?mechanization. The mechanical thought of mathematics in ancient China made a deeply influence in Wu Wen-juns work about mathematics mechanization. In 1976, academician Wu Wen-jun began to enter the field of mathematics?mechanization. Since then , he forwards to the mechanization method which establish theoretical basis for the mechanization of mental work. He proves a large class of elementary geometry problems by computer. It is unprecedented in our country. This is a machine proving method and known as Wu’s method throughout the world. It is the first system for mechanic proving method and it can give the proof for nontrivial theorem. He makes the Study of Theorem Proving in Geometry more mature[