Automated Geometric Theorem Proving, Diagram Generation and Applications

Abstract

It is often said that "a picture is more than one thousand words." But in reality, it is still much more cumbersome or even difficult to generate pictures with computer software than to process words, especially when the pictures involve exact geometric relations in it. It is even more difficult to prove geometry theorems, which is considered as one of the hardest mental labor. In this presentation, we will introduce some effective methods for automated geometric theorem proving, discovering, and geometric diagram generation developed by us, including the the deductive database method, the c-tree decomposition method and the LIMd method. In particular, we will introduce the concept of intelligent dynamic geometry software, which can be used to manipulate geometric diagrams dynamically as dynamic geometry software, but does not has the limitation of ruler and compass constructions. Applications of the these methods to computer aided instruction, robotics, computer vision, and linkage design will also be discussed.