用代数消元法实现平面几何命题的全自动证明
Automated proving in planar geometry based on the complex number identity method and elimination
- 将复数恒等式法改进为完全自动化程序，基于消元理想
- 通过引入松弛变量消去所有点变量，得到可判断结论的代数理想
- 已集成至GeoGebra实验版，支持几何命题自动验证
我们改进了复数恒等式证明方法，使其成为基于消元理想的全自动程序。通过将每个实关系假设 $h_i$ 改写为 $h_i - r_i$，结论 $t$ 改写为 $t - r$，清除分母并引入含松弛变量的新表达式，消去所有自由和关系点变量。在所得理想 $I$（位于 $bQ[r, r_1, r_2, dots]$）中，若存在线性多项式 $p(r) rom I$，且 $r_1, r_2, dots$ 为实数，则 $r$ 必为实数（除非表达 $r$ 时发生除零）。结果已在 Mathematica、Maple 及 Giac 新版本中实现。最后，我们在动态几何软件 GeoGebra 的实验版本中展示了该方法的原型。
原文摘要 · Abstract (English)
We improve the complex number identity proving method to a fully automated procedure, based on elimination ideals. By using declarative equations or rewriting each real-relational hypothesis $h_i$ to $h_i-r_i$, and the thesis $t$ to $t-r$, clearing the denominators and introducing an extra expression with a slack variable, we eliminate all free and relational point variables. From the obtained ideal $I$ in $\mathbb{Q}[r,r_1,r_2,\ldots]$ we can find a conclusive result. It plays an important role that if $r_1,r_2,\ldots$ are real, $r$ must also be real if there is a linear polynomial $p(r)\in I$, unless division by zero occurs when expressing $r$. Our results are presented in Mathematica, Maple and in a new version of the Giac computer algebra system. Finally, we present a prototype of the automated procedure in an experimental version of the dynamic geometry software GeoGebra.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。