Mechanization theorems of (ordinary) ordered geometries

Abstract

The geometries, such as unordered Pascalian geometry and orthogonal geometry, which were considered in Chaps. 3 and 4 do not assume any relation of order. In geometries of this kind the statement of theorems, after fixing the coordinate system, involves only some equality relations. We have proposed a mechanical method which usually is quite efficient and can be used to prove rather difficult theorems. Practice will show the extent of efficiency of our method for unordered geometries. In the book “Theory, Method and Practice of Mechanical Theorem Proving in Geometries” (under preparation), we shall explain in detail the algorithmic procedure, implementation and computer experiments of this method and give more examples. This book is restricted only to the basic principles. If a geometry assumes an order relation and the statement — especially the conclusion part — of a theorem involves such an order relation, then the situation becomes not only much more complicated but also different in essence. In this case, there are methods for mechanical proving in theory, but their efficiency is not high. It still seems difficult to prove non-trivial theorems by using these methods.