Automated Geometry Reasoning and Diagram Constructing

本课题研究的是几何图形的自动构造或几何约束求解，即自动绘制一个声明性描述的图形或工程图。 这类工作是当前开发智能化和参数化CAD系统以及交互式基于约束的图形系统的中心工作，近年来发展起来的成功的几何定理自动证明和发现方法将被扩展到几何图形自动构造方法，并将其应用于智能CAD领域（计算机辅助设计）与CAI几何约束求解的新技术将被开发，以推进CAD研究的最新水平，并提供更好的CAI系统。 将探索新的自动推理技术，通过使用更多的几何谓词，引入新的绘图工具，并将2D方法扩展到3D，以开发更快，更强大的自动化图表构建方法。 所提出的研究的基础是自动生成人类可读的几何证明的工作。 全局传播方法自动生成的几何图的施工步骤表明，所提出的工作是可行的，可能会导致显着提高CAD系统的性能。 各种优化技术，如全局优化方法和多目标优化方法，将用于开发更稳定，灵活和强大的几何约束求解的数值方法。新的符号计算技术将用于增强约束求解系统在某些特殊情况下的能力。 这些技术包括块三角剖分和基于矢量和几何不变量的消元理论。最后，将研究和应用集成技术，将上述方法结合起来，建立更加实用和智能化的CAD和CAI系统。

This project is concerned with automated geometry diagram constructing or geometric constraint solving, which is to draw a declaratively-described diagram or an engineering drawing automatically. This kind of work is central to much of the current work of developing intelligent and parametric CAD systems and interactive constraint-based graphic systems.Successful methods of automated geometry theorem proving and discovering which have been developed in recent years will be extended to methods of automated geometry diagram constructing, which in turn will be applied to the areas of intelligent CAD (computer aided design) and CAI (computer aided instruction).New techniques for geometry constraint solving will be developed to advance the state of the art for CAD research and to provide better CAI systems. New automated reasoning techniques will be explored for developing faster and more powerful automated diagram constructing methods by using more geometry predicates, introducing new drawing tools, and extending the 2D method to 3D. The basis of the proposed research is the work on automated generation of human-readable proofs in geometry. The global propagation method for automated generation of construction steps of geometry diagrams shows that the proposed work is feasible and may lead to significant improvement of the performance of CAD systems. Various optimization techniques, such as global optimization methods and multi-objective optimization methods will be used to develop more stable, flexible, and powerful numerical methods of geometric constraint solving.New symbolic computation techniques will be used to enhance the power of constraint solving systems in certain special cases. These techniques include block triangulation and elimination theories based on vector and geometric invariants.Finally, integration techniques will be studied and used to build more practical and intelligent CAD and CAI systems by incorporation all the above methods.