几何定理机器证明的类型

网上有关“几何定理机器证明的类型”话题很是火热，小编也是针对几何定理机器证明的类型寻找了一些与之相关的一些信息进行分析，如果能碰巧解决你现在面临的问题，希望能够帮助到您。

几何定理机器证明的代数方法又包含多种不同的方法，如吴方法、Grobner 基方法、单点例证法、数值并行法等。其中，吴方法是代数方法的代表，其它几种方法都是在吴方法之后，受其思想的影响提出来的。吴方法是我国著名数学家吴文俊先生1977年提出来的一种用代数的方法来证明几何定理的新的方法。该方法适用于证明“等式型”的几何定理，而且证明的效率很高，一般可以用几分钟甚至几秒钟就可以证出不简单的定理。其中，等式型几何定理是指：将几何问题引进坐标化为代数问题后，问题的条件和结论都可以化为若干个等式的形式。

吴方法进行几何定理机器证明的第一步是几何问题代数化，建立坐标系，并将命题涉及的几何图形的点选取适当的坐标，然后把命题的条件和结论表示为坐标的多项式方程组。最后判断条件方程组的解是否满足结论方程。通常的几何命题涉及的多项式方程组都是非线形的，一般无法将约束变元求出。吴方法是利用伪除法判定条件方程组的解是否是结论方程组的解。而且利用吴方法不仅可以判断定理的正确与否，还可以自动找出定理赖以成立的非退化条件，这是传统的做法无法做到的。多项式的伪余除法可以通过计算机做符号计算进行。此外，单点例证法和数值并行法，这两种方法与吴方法进行大量符号计算不同，主要利用数值计算的方法进行定理的证明，所以有时也被单独列为一类方法，即几何定理证明的数值方法。数值方法与其它方法相比，具有效率高的优点。几何不变量的方法虽然实现了一大类几何定理的机器的可读证明，但是这种方法得到的证明过程常常不符合人的思维习惯。而利用演绎数据库的方法，根据几何命题所给的条件、已知的公理、定理及公式等推理规则，通过大量的试验匹配的方法进行证明似乎更符合人的思维习惯。这种方法也被誉为“大英博物馆式的推理方法”，最早有这种设想的是H.Gelernter,J.R.Hanson和D.W.Loveland。它们于1960年联合发表一篇文章中提出了从结论出发进行搜索的后推链方法。

关于“几何定理机器证明的类型”这个话题的介绍，今天小编就给大家分享完了，如果对你有所帮助请保持对本站的关注！

本文来自作者[liuzea]投稿，不代表六泽号立场，如若转载，请注明出处：https://liuzea.cn/cshi/202508-16449.html