Automated Geometry Reasoning and Methods for Diagram Generation

在过去的二十年里，自动化几何推理是一个非常成功的领域。自70年代末以来，已经引入了非常成功的自动化几何定理证明和发现方法。利用这些方法，人们不仅可以在几秒钟内证明大多数的几何定理，而且还可以发现许多新的定理。人们也可以证明和发现微分几何和力学中的定理。在90年代早期，开发了生成人类可读证明、多重证明和最短几何证明的方法。自动生成几何图（AGDG）的方法是近年来发展起来的。AGDG的目的是自动绘制声明性描述的图。与自动化定理证明相比，AGDG具有更广泛的应用范围，包括智能CAD、机器人、连杆设计、计算机视觉、纳米技术和化学分子建模、基于约束的交互式图形系统、数控机床和计算机辅助指令。

ABSTRACT0201253Shang-Ching CouWichita State UAutomated geometry reasoning has been a very successful area in the past twenty years. Highlysuccessful methods for automated geometry theorem proving and discovering have been introducedsince the late 70s. With these methods, one can not only prove most of the geometry theoremswithin seconds, but also discover many new theorems. One may also prove and discover theoremsin differential geometries and mechanics. In the early 90s, methods were developed to generatehuman-readable proofs, multiple proofs, and the shortest proofs in geometry.Methods for automated geometry diagram generation (AGDG) have been developed recently.The purpose of AGDG is to draw a declaratively described diagram automatically. Compared toautomated theorem proving, AGDG has a wider range of applications, including intelligent CAD,robotics, linkage design, computer vision, nanotechnology and chemical molecular modeling,interactive constraint-based graphic systems, numerically controlled machines, and computer aidedinstruction.