Mechanical Geometry Theorem Proving Based on Groebner Bases

A new method for the mechanical elementary geometry theorem proving is presented by using Groebner bases of polynomial ideals. It has two main advantages over the approach proposed in literature: (i) It is complete and not a refutational procedure; (ii) The subcases of the geometry statements which are not generally true can be differentiated clearly.

Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving

This paper discusses two problems:one is some important theories and algorithms of affine bracket algebra;the other is about their applications in mechanical theorem proving.First we give some efficient algorithms including the boundary expanding algorithm which is a key feature in application.We analyze the characteristics of the boundary operator and this is the base for the implementation of the system.We also give some new theories or methods about the exact division,the representations and structure of affine geometry and so on.In practice,we implement the mechanical auto-proving system in Maple 10 based on the above algorithms and theories.Also we test about more than 100 examples and compare the results with the methods before.

Mechanical theorem proving in the surfaces using the characteristic set method and Wronskian determinant

In this paper, we generalize the method of mechanical theorem proving in curves to prove theorems about surfaces in differential geometry with a mechanical procedure. We improve the classical result on Wronskian determinant, which can be used to decide whether the elements in a partial differential field are linearly dependent over its constant field. Based on Wronskian determinant, we can describe the geometry statements in the surfaces by an algebraic language and then prove them by the characteristic set method.

A REVIEW AND PROSPECT OF READABLE MACHINE PROOFS FOR GEOMETRY THEOREMS

After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.

Complex brackets and balanced complex 1st-order difference polynomials in 4-dimensional Minkowski space

This paper investigates complex brackets and balanced complex 1st-order difference (BCD) polynomials. Then we propose an algorithm of O(n log n) complexity to check the equality of brackets. It substitutes exponential algorithms before. Also, BCD polynomials have some usages in geometric calculation.

AN APPLICATION OF RITT-WU＇S ZERO DECOMPOSITION ALGORITHM TO THE PSEUDO NULL BERTRAND TYPE CURVES IN MINKOWSKI 3-SPACE

The Bertrand curves were first studied using a computer by Wu （1987）. The same problem was studied using an improved version of Ritt-Wu＇s decomposition algorithm by Chou and Gao （1993）. This paper investigates the same problem for pseudo null Bertrand curves in Minkowski 3-space E3 1.