再开一个坑：吴方法 Wu's method

cancan123456 · 2023-09-10 16:53:24 · 个人记录

Automated Geometric Theorem Proving: Wu’s Method 的翻译。

摘要：吴方法是证明几何问题的一个广为人知的方法。我们研究了相关的底层算法，包括伪除法（pseudodivision），Ritt 原理与 Ritt 分解算法。我们还提供了 Maple 中这些算法的实现，并用其证明一些简单的几何定理来说明这个方法。

I Introduction

本文将讨论自动化几何定理证明中的代数方法，特别是吴方法。用算法证明几何命题是一个研究领域，在机器人与人工智能领域具有特别的重要性。虽然一个实现了吴方法的计算机在人类的视角中很难说是“思考”几何，但是可以使计算机能够以一种相当复杂和独立的方式与物理环境交互（参见 [4] 中对机械臂的讨论）。

总的来说，我们会遵循 [1] 中表述的主题。首先，我们会讨论如何将几何描述翻译为代数。在考虑完一些例子后我们会转向记录一些基本代数结果，贯穿本文的剩余部分。接下来，我们通过使用 Groebner 基的几何定理证明的简略的讨论来引出吴方法。第三，我们介绍了吴方法的剩余部分，包括伪除法的概念、上升链、特征组与 Ritt 分解算法。接下来，我们会说明吴方法如何被用于证明几何定理。最后一节包括一些 Maple 中的非常基本的吴方法的实现和其在一些例子中的应用。

在次，我们简略地介绍一下吴方法：

将几何定理翻译为一个代数方程组，得到一组假设等式 f_1,\dots,f_r 和一个结论 g（第 2 节）。
用伪除法将我们的假设等式组翻译为三角形式（第 4.1 节）。关于三角形式，我们指的是假设等式可以写作：

\begin{aligned}f_1&\quad=\quad f_1(u_1,\dots,u_d,x_1)\\f_2&\quad=\quad f_2(u_1,\dots,u_d,x_1,x_2)\\\vdots\\f_r&\quad=\quad f_r(u_1,\dots,u_d,x_1,\dots,x_r)\end{aligned}

和 variety V(f_1,\dots,f_r)，包含由假设方程定义的原始 variety 的不可约分量（关于这种特殊三角形式的详细信息，请参见第 4.2 节）。

在翻译后的三角形式与结论等式连续执行伪除法（第 4.1.1 节），生成一个最终余式。如果最终余式是 0，那么我们会说结论 g 可由假设 f_1,\dots,f_r 得出。
检查在三角化假设时出现的非退化条件（第 5 节）。特别地，假定非退化条件成立，我们得出 g 可以从 f_1,\dots,f_r 得出。这些条件是 p=0 的形式，其中 p 是一个多项式，在我们的三角化过程中自然产生。

2 Algebraic Formulation of Geometric Theorems

为了说明将几何陈述翻译为合适的代数等式组，我们考虑几个例子。开始的最简单的方式是说明平行四边形的对角线在平面上的交点将对角线平分（这个定理在 [1] 与 [4] 中重复地用作例子）。我们想到的情况如下所示。

例子 1 基本思想是将上图放置于坐标系中，且将定理的假设解释为坐标中的陈述，而不是欧几里得的几何陈述。所以我们从坐标化平行四边形开始，将 A 放置于原点，所以 A=(0,0)。现在我们可以说点 B 与 (u_1,0) 相对应，并且 C 对应于 (u_2,u_3)。最后的顶点，D，完全由其他三个点决定。我们通过用坐标 (x_1,x_2) 标记 D 来在其坐标中指明这种区别。一些坐标永远会取决于我们如何选择其它的点。换句话说，一些点是任意的，另一些点是完全任意的。我们会用 u_i 来表示任意的坐标，x_i 来表示完全确定的点的坐标，以此区分这些点。最终，对角线交点，O 的坐标也由前面的点完全确定，所以我们令 O=(x_3,x_4)。

占位符