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

1、Mechanical Theorem Proving in GeometryGao Jun-yu*, Zhang Cheng-dongCangzhou Normal University Hebei province,Cangzhou city,College Road, 061001.e-mail: AbstractMechanical theorem proving in geometry plays an important role in the research of automated reasoning. In this paper, we intro

2、duce 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 point method, lower dimension methodC

3、opyright 2012 Universitas Ahmad Dahlan. All rights reserved.1. Introduction HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=Mechanical+Proving t _blank Mechanical Proving, that is, mechanization method, is to find a method which can be computed steep

4、ly 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 me

5、chanic mathematics. Today, the method of Cartesian coordination gives this direction a solid step, 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 mathemati

6、cs mechanization. In 1976, academician Wu Wen-jun began to enter the field of mathematicsmechanization. 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

7、 is unprecedented in our country. This is a machine proving method and known as Wus 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 mature1-6.In 1992, Academician

8、Zhang Jing-zhong visited the USA to research mathematics mechanization and cooperated with Zhou Xian-qing and Gao Xiaos-han. The HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+Elimination+Point+Method t _blank elimination point method is one that i

9、s 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 HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&sk

10、ey=+lower+Dimension+Method t _blank lower dimension method. He obtains the achievement in the mechanic proof of inequalities. The achievement of this method is as good as Wus method and HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+Elimination+Poi

11、nt+Method t _blank 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 methods respectly.2. Wus methodWu Wen-jun presents a method which is called Wus method. It is based on Quaternio

12、n 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 proof for the geometric theorem in computer. We introduce three main steps of this method as follows4-10:Step

13、 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. Similarly, let us denote the restrict variables as which are restricted by the conditions of geometric proble

14、ms. 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 family of palynomial.Step 2 TriangulationAccording to the restrict variable, the rearrange of (1) is referred as

15、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 algorithm is denoted as .In order to avoid the fractional in quotient, we multiply to, that is, （4）The remainder

16、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:Dividing two cases to discus: with and .Case 1: If, then, under the condition of and the non-degenerate cond

17、ition , 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 HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+Wu%e2%80%99s+Method t _blank Wus Method in solving problem. Ex

18、ample 1 The problem is: The midline on the hypotenuse in a right-angle triangle equals to half of the hypotenuseUsing HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+Wu%e2%80%99s+Method t _blank Wus Method to get the solution of the above problem is

19、: as shown in Figure 1, first, choose coordinates to right-angle triangle. The two right-angle sides of and are as axis and axis respectively. The vertex of the right angle is ,.We take as the midpoint of hypotenuse and set up their coordinates as ，and respectively.OOB (0,)A (,0)D (,)Figure 1Because

20、 are arbitrary, this indicate that coordinates of are free variables and the midpoint is restricted by the hypothesis, so the coordinates of are restrict variables.Applying Wus Method , we solve this problem as follows:Step 1 Choosing a good coordinate system, free variable and restrict variable.Sup

21、posing is the midpoint of the , by the midpoint formula we can get:Using step 1 in Wus Method , we only need to prove that the , by the distant formula: Step 2 TriangulationBecause just has the restrict variable , and just has the restrict variable , so , themselves have been trianglize. So, it can

22、be written as:Step 3 Gradual Division is divided by ,and the division is:That is, （7）where is divided by , so, （8）Where . Using (8) to express (7) ,we will receiveWhen , The proposition has been proved.3.Zhangs Elimination Point MethodWe introduce Zhangs Elimination Point Method as follows1-9.Zhang

23、Jing-zhong gives an effective method for what is called elimination point method, the method is based on the ancient area method, mainly used for deleting the constraint points. This idea of Zhangs Elimination Point Method is relative to the assumed conditions and area method, and the order of vanis

24、h point depends on the final constraint points. Then it is eliminated from back to front one by one. At last, the left point is total eliminated, if the number is equal to the right number, the proposition is permitted. To use Zhangs Elimination Point Method effectively, we repeat the public edge th

25、eorem in the following:Next, we give a commonly important theorem of elimination point method:Public edge theorem (1970,Zhang): If the line and line to , thenPublic edge have four cases are shown as (a)-(d) in Figure 2 respectively.PPQABM(a)PQABM(b)PABM(c)QPQABM(d)Figure 2We give an example to expre

26、ss the Public edge theorem of Zhangs theorem.Example 2: The problem is : Verify that the diagonal of a parallelogram is mutual divided.To solve this problem is the following:Put a parallelogram as a diagram in Figure 3.1、Do a parallelogram.2、Connecting the diagonals which intersect at .We only need

27、to verify ,. is the restriction point which finally made. So, firstly to remove the point . (Public edge theorem)AABCDEFigure 3Therefore, we can prove , and as the above similar way.4. HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+lower+Dimension+

28、Method t _blank Lower Dimension MethodWith the establishment of HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+Wu%e2%80%99s+Method t _blank Wus method and HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&

29、skey=+Elimination+Point+Method t _blank elimination point method, the Machine Proving of automated theorem proving of equation theorem has been solved ,but the Machine Proving of automated theorem proof of equation theorem has been difficult to achieve. Therefore, YangLu and many other scholars work

30、ed for the establishment of a new algorithm which we called HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+lower+Dimension+Method t _blank lower dimension method. The work in the field of machine theorem proving by Chinese mathematicians is a miles

31、tone2-12.The HYPERLINK /kcms/detail/%20%20%20%20%20%20%20%20%20%20%20%20search.aspx?dbcode=CJFQ&sfield=kw&skey=+lower+Dimension+Method t _blank lower dimension method can be divided into three courses:(1) Work out about boundary surface of inequality 、.(2) Using the boundary surface of the first ste

32、p the parameter space was divided into finite cell decompositions, we get many connected open sets: 、, then from the connected open sets we select checkpoint for at least one abbrevd . (3) using the finite number of checkpoints 、 to verify the correctness of inequality. If every established the prop

33、osition is true, otherwise, the proposition is false.5. ConclusionThe three methods present different ways to deal with different problems. All of them are important in automated reasoning fields, when someone discusses a problem in automated reasoning fields, the first he (or she) would consider wh

34、ich of the three methods is just best for the problem, and then, he (or she) will obtain the best consequences. We hope our introduction is good for him (or her) , now and in the future.References1 Wu Wen-jun. Elementary geometry truss proof and mechanization J. Chinese science, 1997, (6), (in chine

35、se).2 Wu Wen-jun. Geometric theorem machine the basic principle of proof M. Beijing: science press, 1984, (in chinese).3 Zhang Jing-zhong. Away on collocation method J. Mathematics teacher, 1995, (1), (in chinese).4 Zhang Jing-zhong.The computer how to work out geometric problem M. Beijing: tsinghua

36、 university press, 2000, (in chinese).5 Zhang Jing-zhong, Gao Xiao-shan, Zhou Xian-qing. Based on the geometry information before extrapolation search system J. Journal of computer, 1996, 38 (10), (in chinese).6 Yang Lu. Inequality proof dimension reduction algorithm of the machine and the general p

37、rogram J. High technology communication, 1998 (7), (in chinese).7 B. Liu and Y.K. Liu, Expected value of fuzzy variable and fuzzy expected value models, IEEE Transactions on Fuzzy Systems Vol.10, No.4 ,2002.8 J.A.Bondy and U.S.R.Murty. Graph Theory With ApplicationsM.New York: Elsevier Science Publi

38、shing Co.Inc,1976. 9 B.Korte and Vvgen. Combinatorial Optimization Theory and AlgorithmsM. Berlin:Springer，2000.10 Hua Mao, Sanyang Liu, Some Properties of the Closure Operator of a Pi-space, Kyungpook Mathematical Journal, 2011，51(3).11 Sandip Chanda Abhinandan De .Congestion Relief of Contingent P

39、ower Network with Evolutionery Optimisation Algorithm, TELKOMNIKA Indonesian Journal of Electrical Engeering ,Vol.10 No.1 March 2012,12 Hadi Arabshahi,Static Characterization of InAs/AlGaAs Broadband Self-Assembled Quantum Dot Lasers, TELKOMNIKA Indonesian Journal of Electrical Engeering, Vol.10 No.

40、1 March 2012,附录资料：不需要的可以自行删除设备大修规程1、目的消除设备存在的缺陷，保证生产设备恢复原有性能，有效延长设备的寿命、减小设备故障率、提高生产效益，减轻设备维修量。2、适用范围厂区主要生产设备3、职责 3.1设备经理（主管）根据生产情况，以及通过设备维修数据分析设备情况，制定设备大修计划，并且购置设备大修配件。3.2事务助理根据要大修的设备，编制设备大修记录单、设备大修验收记录单。3.3大修班班长根据要大修的设备，拟定大修计划，列出大修配件名单交设备主管，准备大修所有器具，做好大修安全防护措施。3.4操作人员极力配合大修人员的工作，顺利开展大修。4、工作规程4.1大修准

41、备工作4.1.1设备主管根据生产情况、设备情况提前一周制定大修计划，并落实到大修班和生产部门。4.1.2设备事物助理根据大修设备，编制设备大修记录单给大修班、大修验收记录单给设备主管。4.1.3大修班班长根据要大修的设备查阅资料，拟定大修安排计划，列大修配件清单交设备主管，落实大修人员，准备设备大修所需器具，做好大修安全防护措施。4.1.4设备主管购置设备大修所需配件，在大修前配齐。4.1.5操作人员在设备大修前，做好设备清洁卫生，清理设备场地，挪开生产加工物品，提前停止设备，进入待修状态。4.2设备大修实施 4.2.1大修班班长组织指导大修工作，大修班根据大修要求严格对设备进行大修。 4.2

42、.2填写设备大修单，记录在大修中更换的配件。 4.2.3设备主管在大修结束后，对大修设备进行验收，记录设备运行是否正常，运行参数是否合格，验收合格后投入运行。4.2.4设备事务助理在设备验收合格后，对大修记录、验收记录进行存档，并完善ERP平台数据记录。4.3设备大修规范4.2.1设备大修的周期为2年进行一次。4.2.2设备大修是以大修班为主、操作人员为辅，对设备有效的大修。 4.2.3根据设备秩序要求，结构要求，对设备全部或部分解体，把拆卸配件归类标记、存放。 4.2.4严格检查设备机械结构部分和配件，清理结构污垢，清洗机械配件，更换润滑油，更换老化配件。 4.2.5检查设备气动、油压系统，

43、清理气管、油管，清洗油箱、阀芯等，更换沉淀老化液压油。 4.2.6检查电气部分，更换老化线路、电器元件，更新设备配置，紧固各接线端子；检验电气设备绝缘、阻值等参数，更换检修参数不合格的电气设备；对配电箱、配电柜等进行清洁吹灰。 4.2.7没有允许，严禁改动设备原有结构，根据设备结构还原装配设备。4.2.8完成大修后，要清洁大修场所，保持设备环境的清洁卫生，对更换的配件统一规范放置。相关文件和记录 5.1设备大修单 5.2设备大修验收单附件: 设备维修及故障处理流程图1设备维修流程设备操作人员发现故障填设备保修单注明设备型号（序号）设备操作人员发现故障填设备保修单注明设备型号（序号）、简述故障情

44、况，生产班（组）长签字报机修班特殊情况可直接电话报修事后及时补写报修单机修班（组）长及时（15分钟内）安排检修或机修工接报修单直接检修维修机修人员主导，严格按照设备检修规程、安全操作、准确判断故障、按时保质完成，设备操作人员配合辅助设备配件在机修班库房或公司配件库领取（中夜班联系库房管理员）检修技术难点（问题）及时询问班（组）长和老员工，特殊辅助机具及时联系车间主任及班组长支援重大问题及时联系设备部经理（主管）直至向公司分管领导汇报一般情况当班必须检修完毕，如特殊情况必须与下班交接（故障情况、检修进度等）做好记录检修完毕操作人员进行试车验收，填写维修情况、维修时间（报修单）设备部主管（专项助理

45、）每周收集统计报修单，考评机修工检修时间及设备维修时间，周会通报设备部经理（主管）每月根据设备维修时间统计，分析（改进）设备维修状况、设备运行状况及操作与维修人员综合素质，形成月度总结上报公司2设备事故处理流程设备操作人员、车间主任、班组长或相关发现人员上报设备操作人员、车间主任、班组长或相关发现人员上报设备部、机修班维修人员或安全巡检人员提出设备部经理（主管）主导召集设备事故分析会，设备操作人员、所属车间主任班组长、机修班（组）长、相关维修人员参加，生产部、安环部有关人员列席（如发生人生伤害事故由安环部主导）由设备操作人员、车间主任、班组长或相关发现人员阐述事故经过，维修人员叙述维修经过、损