Automated Reducible Geometric Theorem Proving and Discovery by Gröbner Basis Method
Automated Reducible Geometric Theorem Proving and Discovery by Gröbner Basis Method
复制标题
DOI：
10.1007/s10817-016-9395-z
复制
发表时间：
2017-10
期刊：
影响因子：
--
通讯作者：
Jie Zhou;Dingkang Wang;Yao Sun
中科院分区：
文献类型：
--
作者：
Jie Zhou;Dingkang Wang;Yao Sun
本文研究了关于几何命题的假设的某些分支的结论为真的问题。在这种情况下，与假设相关联的仿射簇是可约的。一个多项式在一个簇的某些但不是所有的分量上为零当且仅当它是关于该簇定义的根理想的商环中的零因子。基于这一事实，我们提出了一个算法，以确定是否几何陈述是一般真或一般真的组件的Gröbner基方法。该方法也可用于几何定理发现，给出几何命题为真或在分支上为真的补充条件。给出了一些可约几何陈述来说明我们的方法。
In this paper, we investigate the problem that the conclusion is true on some components of the hypotheses for a geometric statement. In that case, the affine variety associated with the hypotheses is reducible. A polynomial vanishes on some but not all the components of a variety if and only if it is a zero divisor in a quotient ring with respect to the radical ideal defined by the variety. Based on this fact, we present an algorithm to decide if a geometric statement is generally true or generally true on components by the Gröbner basis method. This method can also be used in geometric theorem discovery, which can give the complementary conditions such that the geometric statement becomes true or true on components. Some reducible geometric statements are given to illustrate our method.