论文标题
参数root查找，用于支撑遗传和发现地球上的几何不平等现象
Parametric Root Finding for Supporting Proving and Discovering Geometric Inequalities in GeoGebra
论文作者
论文摘要
我们向地理布拉介绍了软件包/子系统地理布拉的发现，该发现支持了自动化的基本几何不等式的自动化证明或发现。在此案例研究中，对于与等同镜和直角三角子类有关的不平等探索问题，我们证明了如何通过参数词根发现（PRF）算法代替我们的一般实际量化器消除（RQE）方法。一般RQE需要高维空间的完整单元格分解，而新方法可以避免这种昂贵的计算，并且可以导致实际加速。为了获得1D探索问题的解决方案，我们为一维参数系统的判别种类计算了一个基础，并解决了有限的许多非线性真实（NRA）满意度（SAT）问题。我们通过示例说明了所需的计算。由于GIAC（Geogebra中的基础免费计算机代数系统）可用，并且可以将这种方法链接到Geogebra，因此我们希望该方法可以轻松地添加到现有的理性工具中，以使其链接到Geogebra。
We introduced the package/subsystem GeoGebra Discovery to GeoGebra which supports the automated proving or discovering of elementary geometry inequalities. In this case study, for inequality exploration problems related to isosceles and right angle triangle subclasses, we demonstrate how our general real quantifier elimination (RQE) approach could be replaced by a parametric root finding (PRF) algorithm. The general RQE requires the full cell decomposition of a high dimensional space, while the new method can avoid this expensive computation and can lead to practical speedups. To obtain a solution for a 1D-exploration problem, we compute a Groebner basis for the discriminant variety of the 1-dimensional parametric system and solve finitely many nonlinear real (NRA) satisfiability (SAT) problems. We illustrate the needed computations by examples. Since Groebner basis algorithms are available in Giac (the underlying free computer algebra system in GeoGebra) and freely available efficient NRA-SAT solvers (SMT-RAT, Tarski, Z3, etc.) can be linked to GeoGebra, we hope that the method could be easily added to the existing reasoning tool set for educational purposes.
