Theorem-proving is an extremely important topic in the study of Artificial Intelligence,its basis is the deductive reasoning---a basic method for human being to understand the would.The finite inductive reasoning is another basic method for human being to understand the world,but neither precise nor reliable.For example,when n=1,2,3,…,39 n2 +n + 41 always is a prime.By using inductive reasoning people may get the conclusion that:"for any n∈N-{4lk:k∈N},n2 + n + 41 is a prime".That is wrong,because 402 + 40 + 41=412 is not a prime.But,for the elementary plane geometry propositions,we have shown that:to determine whether a proposition is true,we need only to verify a special case of this proposition.In other words,given an elementary plane geometry proposition,we can give a concrete example by our method.The given proposition is true iff it is true for this concrete example.This concrete example depends only on the length n and the freedom degree s of the proposition.In order to de termine whether this concrete numerical example is true on the given proposition,we need only to calculate C (a concrete integer that we can get from the given proposition) significant digits.For instance,if we want to prove"the three meadian lines of any triangle intersect at one point".By our method,we need only to verify a special triangle whose coordinates of three points are (0,0),(0,1),(10,0).The process of verifing is to calculate X,Y,Z to 6 significantdigits from three equations 3X-10=0,10Y-X=0 and Z+20Y+X-10=0,if Z＜10-1 then the proposition is true,otherwise the proposition is false.This paper is a summary of some papers,it present a new Mechanical Theorem Proving Method in elementary plane geometry----"Proving by Example"method,it also includes some deep and important mathematical results.
展开▼
