Automated Reasoning in Geometry and Mechanics

这个项目的目标是研究初等几何、微分几何和力学中的自动推理，作为我们以前和现在工作的扩展。它不仅包括定理证明，还包括公式推导。在这三个方面，将分别进行以下研究：(1)改进现有的证明技术；(2)进一步研究公式的机械推导；(3)收集大量的实例；(4)改进Ritt-Wu分解算法和其他关键算法；(5)将Ritt-Wu方法与初等几何中的Collins方法相结合；(6)发布自动推理系统；(7)研究我们的技术在连杆机构运动综合、CAD/CAM等领域的实际应用；(8)研究与我们的技术相关的理论问题。

The goal of this project is to study automated reasoning in elementary geometry, differential geometry, and mechanics as an extension of our previous and current work. It covers not only theorem proving, but also formula derivation. In each of these three areas, the following research will be conducted: (1) to improve existing proving techniques; (2) To further study mechanical formula derivation; (3) to collect a significant number of worked examples; (4) to improve Ritt- Wu's decomposition algorithm and other key algorithms; (5) to combine Ritt-Wu's method with Collins' method in elementary geometry; (6) to release an automated reasoning system; (7) to study practical applications of our techniques to areas such as kinematic synthesis of linkages and mechanisms, CAD/CAM, etc; (8) to study theoretical issues related to our techniques.