《几何定理的机器证明(定稿)6页》由会员分享，可在线阅读，更多相关《几何定理的机器证明(定稿)6页（6页珍藏版）》请在金锄头文库上搜索。
1、1559TELKOMNIKA e-ISSN: 2087-278XnMechanical Theorem Proving in GeometryGao Jun-yu*, Zhang Cheng-dongCangzhou Normal University Hebei province,Cangzhou city,College Road, 061001. 0317-2159865 e-mail: AbstractMechanical theorem proving in geometry plays an important role in the research of automated r
2、easoning. 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, Wus method, elimination poin
3、t method, lower dimension methodCopyright 2012 Universitas Ahmad Dahlan. All rights reserved.1. IntroductionMechanical 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
4、 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 s
5、tep, and provides a simple and clear method for the proof of geometrictheoremsmechanization.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 mathematicsmecha
6、nization. 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 Wus method thr
7、oughout 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 mature1-6.In 1992, Academician Zhang Jing-zhong visited the USA to research mathematics mechanization and cooperated with Zho
8、u Xian-qing and Gao Xiaos-han. The elimination point method is one that is based on area method. This brings readable Proof to be realized by computer for the first time. This result is significant for academic and mechanical theorem proving in geometry.In 1998,Yang Lu created lower dimension method
9、. He obtains the achievement in the mechanic proof of inequalities. The achievement of this method is as good as Wus method and elimination point method.It is a great achievement in the field of mechanical theorem proving in geometry by Chinese mathematicians3-8.Next, we will introduce the three met
10、hods respectly.2. Wus methodWu Wen-jun presents a method which is called Wus method. It is based on Quaternion of traditional mathematics. This method has been solves a series of actual problems in theoretical physics, computer science and other basic science fields. We can use Wus method to find a
11、proof for the geometric theorem in computer. We introduce three main steps of this method as follows4-10:Step 1 Choosing a good coordinate system, free variable and restrict variable.Let us denote the free variables as , and suppose they have nothing to do with the conditions of geometric problems.
12、Similarly, let us denote the restrict variables as which are restricted by the conditions of geometric problems. In this way, a geometric problems turns into a polynomial problem: （1）The conclusions of geometric problem can be expressed as a polynomial problem. （2）Or, it can be represented as a fami
13、ly of palynomial.Step 2 TriangulationAccording to the restrict variable, the rearrange of (1) is referred as triangulation. In another word, the systems of equation (1) is changed as: （3）Step 3 Gradual DivisionDenote the polynomial in (3) as , in (2)is divided by , and the remainder of division algo
14、rithm is denoted as .In order to avoid the fractional in quotient, we multiply to, that is, （4）The remainder is divided by (5)So, repeating this division, at last we get: （6）Then, let us interate all the equations above and replace the coefficient of of all equations above with , moreover, we obtain
15、:Dividing two cases to discus: with and .Case 1: If, then, under the condition of and the non-degenerate condition , there is , the required result follow.Case 2: If , then the proposition is not true. We present an example to show that how to use Wus Method in solving problem. Example 1 The problem is: The midline on the hypotenuse in a right-angle triangle equals to half of the hypotenuseUsing Wus Method to get the solution of the above problem is: as shown in Figure 1, first,
