Automation of Geometric Theorem Proving, Discovering and Diagram
Generation
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. 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 area method, the deductive
database method, the optimization method, and the c-tree decomposition
method. Implementation and applications of the these methods to intelligent
CAD/CAI, computer vision, robotics, and linkage design will also be
discussed.
|