代数闭域量子消元在计算机辅助证明中的应用 - 理论计算机科学电子笔记57-73 (2006)

理论计算机科学电子笔记151（2006）57-73www.elsevier.com/locate/entcs代数闭域上的量子消元在计算机代数辅助证明中的应用David Delahaye1CPR（ CEDRIC）CNAM法国巴黎Micaela Mayero2LCR（ LIPN）Université Paris Nord（Paris 13）Villetaneuse，France摘要我们提出了一个决策过程的代数闭域的基础上的量化消除方法。 该程序的目的是建立证明系统的多项式方程和不等式。我们描述了这个过程可以进行证明助理使用计算机代数系统在一个纯粹的怀疑的方式。我们提出了一个实现在特定的框架工作的Coq和Maple提供一些细节，这两个工具之间的接口这使我们能够表明，计算机代数系统不仅可以用于为证明助理带来额外的计算能力，而且还可以提高这些工具的自动化程度关键词：定理证明，计算机代数，代数闭域，Coq，Maple1介绍一个代数闭域（ACF）K是一个没有适当代数扩张的域，即每个代数扩张都是K本身。这意味着每个1David. D elahaye@cnam. fr，htt p：//ce d ric. cnam. fr/~ d elahaye/2个月前，我在@lipn。联合国13. 李鹏说，联合国志愿人员组织13.fr/~ma y er o/1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.02358D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）57K[X]的非常数多项式在K中有根。关于场的通常性质，这增加了以下条件：（1）<$P∈K[X]. deg（P）>0x∈K.P（x）=0其中deg（P）表示P的度数。作为ACF的例子，我们可以取复数域，即代数闭包（algebraic closure）代数扩张是代数封闭的）实数域，或代数数域，它是有理数域的代数封闭。可以证明，方程（1）等价于所谓的代数基本定理（FTA），也称为从数学的观点来看，这个定理有一个很好的直接的结果，即K[X]上的多项式可以因式分解，从而可以求解多项式以下形式的方程和不等式系统：⎧⎨P1（X）= 0，.，Pn（X）=0（二）Q1（X）= 0，.，Q m（X）=0为了求解这类方程组，我们只需分解所有多项式，并选择所有Pi的一个公共根，该公共根不是任何Qj的根。然而，从计算的角度来看，这种因式分解的过程通常不是完全自动的。它只能在某些特殊情况下完成，例如在有限域或复数域中使用，例如，方程式（1）的Kneser构造性证明（参见FTA项目[9]）。此外，在实践中，这些方法是不能令人满意的：前者提出了一个复杂性问题（一般来说，多项式的分裂域的大小在次数上是指数的），而后者可以产生任意代数数作为根（通常，在[9]中，根是柯西序列的极限对），并且这些通常很难处理。在本文中，为了解决系统，如（2），我们考虑一个替代的方法，称为quantifier消除，由于隐式存在quantifier（在主变量X的多项式），我们试图消除，这主要是基于摆脱的想法多项式部分，不包含解决方案。这可以通过多项式gcd的概念来实现，这是该方法的主要概念，并且可以简化待求解的系统。此外，该方法在某种意义上更强，因为它可以处理任何[3]由于他在1746年第一次认真尝试证明自由贸易协定，即使第一个证明通常被认为是高斯在1799年的博士论文D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）5759特征（不仅是0），即使后者必须知道。为了将这种方法集成到演绎系统（DS）中，可以考虑几种选择（如[1]中所述;[17]中也以更一般的方式讨论了其中一些想法，以开发可靠的算法软件）。第一种可能是以一种纯粹自给自足的方式来实现它，也就是说，这个方法完全是在DS中编码的，特别是在这里，我们必须定义gcd的概念（可能还有它的正确性证明）。这种选择可能看起来很自然，但它也似乎有点多余的计算机代数系统（CAS）的存在，这是专门用于这种计算，可能是更有效的。另一种选择是受益于计算机代数（CA）提供的帮助，每次需要符号计算时使用CAS，并以所谓的怀疑风格验证其正确性。实际上，我们也可以考虑一种相信的方法，即信任CAS并假设返回的计算结果是正确的，但这种假设有点太强了（CAS可能有一些错误，但更常见的是，在计算过程中可能会忽略一些附带条件），我们可能会发现这种选择不合适。在本文中，我们专注于一种怀疑的方法来对ACF（考虑单变量多项式）进行量化消除方法，特别是，我们描述了验证多项式是gcd（由于余因子和Bézout定理）比直接计算它要容易得多（用一个证明函数）。 为了实现该方法，我们选择Coq[22]作为DS，Maple[4]作为CAS，因为这两个工具之间的现有接口[8]（由作者设计）是多项式gcd扩展的适当基础。我们考虑的方法是普遍接受的（它结合了一些众所周知的属性），本文提供了两个主要的新颖性：第一个是以纯粹的建设性方式提出了量化消除问题的证明，以便可以提取算法;第二个是表明CAS不仅可以用于将计算引入DS（如[12]或[8]），而且可以增强此类工具的自动化2ACF上的量化消除在解释我们使用的方法之前，我们需要一些主要与多项式gcd相关的初步引理（作为参考，可以在附录A中找到相当知名的相应证明）。在下文中，函数deg和gcd将分别表示多项式的次数和两个多项式的幺一gcd。考虑多项式[4]“自给自足”、“怀疑论”和“相信论”这些词是亨克·巴伦德雷格特（Henk Barendregt）和阿尔耶·M·阿尔杰（Arjeh M. Cohen在[1]中。60D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）57P（X），符号P将表示，默认情况下，多项式P（X），除非在变量x的量化器约束下，它将表示值 在x处的对应函数P（X）。我们认为，我们是在一个ACFK中，每个多项式将在KJ[X]中，其中KJ<$KS.T. 等于零是可判定的，给定两个多项式P1和P2，gcd（P1，P2）∈KJ.2.1初步引理命题2.1（公共根）设P1和P2是两个非零多项式。设G= gcd（P1，P2）.我们有：P1=0P2=0 i P 2 =0iG= 0。命题2.2（非根值的存在性）设Q是一个非零多项式。我们有：x.Q/= 0。命题2.3（相对素多项式的根）设P和Q是两个互质的非零多项式（即gcd（P，Q）= 1）。 我们拥有：x.P=0命题2.4（商的根与gcd）设P和Q是两个非零多项式.设G= gcd（P，Q ） ，P1 为 多 项 式 s.P=GP1 。 我 们 有 ： x.P=0<$Q/=0i<$$>x.P1=0<$G/= 0。下面的命题指出，迭代命题2.4的应用定义了一个有根据的归纳方案（归纳是在度上进行的），这将允许我们确保我们的算法的终止命题2.5（度的减少）设P和Q是两个非零多项式。设G= gcd（P，Q），P1为多项式s. P=GP1。如果P和Q不是互质的，那么deg（P1）0和m >0时，Qi。(i) n = 0，m > 0：我们在左情况下（命题2.2）。(ii) n > 0，m = 0：根与P i是公共的，即它等价于（命题2.1）显示Px.P是否=0。如果P/=1，那么我们在左情况下（ACF的定义）;如果不是，我们在右情况下。(iii) n >0，m > 0：• 如果P=1，那么我们就在正确的情况下。• 否则设G=gcd（P，Q）：· 如果G=1，则它等价于显示P=0或不= 0（命题2.3）。· 否则设 PJ是多项式s. t。P=GPJ。这相当于展示了如果Pj=0<$G/= 0或不（命题2.4;由于命题2.5的良基归纳方案）。Q如前所述，我们可以从theo-rem2.6的构造性证明中提取出一个算法，该算法（如果可能的话）可以证明：P1=0... P n=0Qm/=0算法如下：I. 如果n=0，则转到III，否则计算P= gcd（P i，i=1.. n）。II. 如果m= 0：应用命题2.1。 这等价于证明P = 0：[5]我们在这里不回顾布劳威尔-海廷-柯尔莫戈罗夫的语义学的思想=0我62D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）571. 如果P/=1，则终止应用ACF2. 否则失败III. 如果m/= 0：1. 计算Q=Mi=1Qi2. 如果n=0，则应用命题2.23. 否则等价于证明了P=0<$Q/= 0：a. 如果P=1，则失败b. 否则计算G=gcd（P，Q）：i. 如果G=1，则应用命题2.3ii. 否则应用命题2.4并重新应用算法。实际上，将步骤III分别应用于每个Qi比应用于所有Qi的乘积更有效，但后者只是为了简化算法的表述。注2.7所描述的方法在ACF的一般理论中是完全构造性的，即使该方法在ACF的定义上停止，这使我们不必给出明确的解。事实上，这个定义是一个公理，不能在一般的ACF理论中实现（即建设性地证明）。然而，如果该方法在一般情况下保持构造性，则在某些特定情况下可以提供更多信息，例如，FTA的构造性证明可以用于建立有效根（即使这些根可能是任意代数数，这通常很难处理）。3使用CAS让我们看看如何将上一节中描述的过程集成到DS中，以及CAS如何帮助进行某些计算（主要是gcd）。我们还在Coq的框架中提出了一个具体的实现，其中Maple被调用来执行符号计算。3.1多项式及其特征为了实现2.2小节中描述的方法，我们必须确保一切都可以确定，更准确地说，系数是否为零。例如，这是计算多项式的次数或两个多项式的gcd所必需的（实际上，多项式的次数被定义为最大自然数s.t.相应的系数是非零的，而gcd算法，例如欧几里得零多项式）。在我们的方法中，这是通过假设我们使用KJ[X]上的多项式来确保的，其中KJ<$Ks. t。 等于零D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）5763可以确定，并且在KJ[X]上的多项式的gcd保持在KJ[X]中。在KJ上的前一个条件处理零系数的情况，而后者使得算法的递归调用（在2.2小节中描述）成为可能。因此，在我们的实现中，我们决定使用有理多项式，即具有有理系数的多项式然而，由于特征可能是非零的，后者必须给出（它在我们的理论中只是作为一个参数出现），然后可以确定等于零（相应的函数一般是由w.r.t.的特征）。3.2持怀疑态度的方法我们的方法的想法是纯粹的怀疑（见[1]关于如何使DS和CAS相互作用的一般研究这意味着量化器消除过程由DS处理，DS可能会调用CAS进行某些计算，并且必须验证这些计算的正确性。这些验证旨在确保DS的逻辑一致性不会受到这些外部计算的影响。实际上，这可能看起来很明显，但在这种方法中，如果在这个计算上不需要任何属性，那么并不总是需要证明外部计算的正确性。 为例如，考虑代数表达式x2−1，如果我们想使用CAS将其分解为（x+ 1）（x−1），则无需先验地验证CAS返回的结果是否正确。特别是，我们可以使用它，如果我们不假设这个结果是x2−1的因式分解（否则，我们可能会引入潜在的不一致性），则任何验证都是无效的。然而，如果我们想确保这两个表达式是等价的（例如，在证明中用前者替换后者），那么这个等价性必须证明（通常使用适当的环属性）。在我们的过程中，我们使用的主要符号计算是多项式gcd，这正是我们希望由CAS执行的。我们还必须指出，这个计算必须被验证为恰好是gcd，因为在过程中使用的第2要做到这一点，我们的想法是使用相反的Bézout定理3.1（Bézout定理，逆）设P，Q和G是三个非零多项式。若G整除P和Q，且存在两个多项式A和Bs. t. AP + BQ = G则G是P和Q的gcd。有了这个定理，除了gcd，我们需要问CAS还返回分别对应于P和Q除以G的两个同因式P1和Q1，以及Bézout的两个余因式A和B。64D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）57⎨关系。 因此，在DS中，仍然需要证明以下等式：⎧P=P1GQ=Q1G⎪BQ=AP+BQCAS提供的这些额外信息可以被视为证书，旨在帮助DS证明计算的正确性。然而，它们中的一些仅仅是简单的证明，例如，商P1也用于过程本身（见第2节中的命题2.4和2.5）。我们可以注意到，前面的等式比以自给自足的方式（即直接在DS中）计算gcd要容易得多，因为我们必须在DS中编写gcd函数，但更困难的是，我们还必须建立其正确性证明。在我们的方法中，我们可以潜在地受益于使用CAS提供的更聪明的算法（比Euclid3.3使用Coq和 Maple作为一个具体的应用，我们选择使用Coq[22]作为DS，Maple[4]作为CAS来实现我们的决策过程这一选择的动机是两个工具之间存在一个接口[8]（由作者设计，可作为Coq用户贡献），这是实现我们的方法所需的任何扩展的良好基础。 这个接口旨在以怀疑的方式将Maple对域上代数表达式的计算带到Coq。可能的属性（主要是需要通过怀疑模式验证的等式）由一种称为场[7]的策略自动处理（也是由作者设计的），它可能会生成一些由用户证明的副条件（在逆上）。为了实现我们的方法，有必要在Coq中开发一个单变量多项式理论，并且Coq/Maple接口已经扩展到处理多变量多项式。名义GCD这个操作显然返回了gcd，但也返回了子项和余因子（如前所述，需要证明它是gcd）。gcd的验证意味着证明3.2节中给出的等式，这是使用多项式运算和比较多项式系数自动完成的（我们使用策略域）。通过这种方式，⎪D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）5765Maple对于Coq用户来说是非常透明的。促使我们选择Coq的另一个原因是Coq拥有一种经过实验的顶级战术语言（见[6]）。有了这种高级语言，就没有必要详细介绍Coq的实现（如果你打算用完全可编程的元语言6编写你的战术，这是必要的），我们的方法已经非常直观地建立起来了（w.r.t.第2.2节中给出的程序）。这种可能性显然对开发人员很重要，但对任何在查看代码时不会迷路的用户也很重要。整个开发（包含更新的Coq/Maple界面，量化器消除策略以及一些示例）将很快作为新的Coq贡献提供。此开发适用于Coq8.0（最新版本的Coq）和MapleV（也应该适用于较新版本的Maple）。4一些示例为了展示一些示例，我们使用了在第3.3小节中描述的Coq/Maple和brie框架中实现的工具。作为一个ACF，我们考虑的构造（其中的元素是实数对），我们称之为C（ACF的性质已经被假设，但可以在以后证明常数C0和C1分别表示C的中性元素0和1。C的有理常数通过函数Ccte构建，给定自然数n，该函数返回表达式（C1+.+ C1）/C1，n次，其中+和/分别是C中的加法和除法。我们开发并称为pol的一元多项式理论（具有有理系数）需要多项式的规范表示，这些多项式被编码为列表系数/功率的排序相对于相对论时间递减。力量因此，使用构造器PList形成多项式，该构造器将系数/幂列表和该列表被正确排序的证明作为参数。给定一个值，函数UPeval允许我们计算一个多项式。在我们的例子中，我们考虑下面的多项式（为了简化，我们选择只给出整数系数，而不是有理系数;然而，在这些例子中，我们经常处理有理多项式，因为被gcd除的导数以及Bézout关系的余因子，对于确保3.2小节中描述的计算的正确性是必要的，通常是有理多项式）：[6]元语言必须与逻辑语言（定理在逻辑语言中被表达和证明）区分开来，它的目的是提供一种编写程序的方法，这些程序可以（自动）建立证明。66D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）57P1= 3X2+X+2P2= 3X3+ 10X2+ 5X+6Q1= 2X−1Q2= 2X2+ 5X−3它们应该被定义为Coq常数P1，P2，Q1和Q2。更准确地说，P1例如定义如下：定义P1： polC：= PListC（（Ccte 3，2）：：（Ccte 1，1）：：(Ccte 2，0）：：nil）sorted_p1.其中：：/nil是列表构造器，sorted_p1是证明（先前构建的）幂列表（即，2，1和0）是递减排序的。在下文中，我们假设ACF公理化、一元多项式理论、Coq/Maple接口和称为qelim的量化消除策略已经加载到Coq顶层。我们还假设前面的多项式P1、P2、Q1和Q2已经被定义。4.1一些简单的案例在这里，我们给出一些例子来说明2.2小节中描述的算法的一些已识别的情况。4.1.1情况II：n= 0且m =0我们建议证明以下命题：x.P1=0在这种情况下，我们有gcd（P1，P2）= 3X2+X+2，根据命题2.1，它等价于证明了x。3x2+x+2 = 0（这是由ACF的定义证明的）。在Coq中，我们有：Coq目标存在x： C，UPeval x P1 = C 0/\ UPeval x P2 = C 0。1个次级目标============================existsx：C，UPeval x P1 = C0/\UPeval x P2 = C0一旦P1和P2的定义展开，我们就应用定量消除策略（qelim）：Unnamed_thm展开P1、P2。1个次级目标============================存在x：C，UPevalx（PList C（（Ccte 3，2）：：（Ccte 1，1）：：(Ccte 2，0）：：nil）sorted_p1）= C0/\D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）5767UPeval x（PListC（（Ccte 3，3）：：（Ccte 10，2）：：（Ccte 5，1）：：（Ccte6，0）：：nil）sorted_p2）= C0未命名的_thmqelim。证明完成。同样，我们也可以测试n= 0和m/=0（情况2），例如，使用Q1和Q2来证明m/= 0。Q1/=0<$Q2= 0。4.1.2情况b：递归调用在下面的例子中，我们希望得到算法的递归调用（b的情况ii）。这可以在试图证明时获得x.P2=0在这种情况下，我们有gcd（P2，Q2）=X+3 =G，并且通过命题2.4，它等价于证明<$x.P2q= 0<$G/= 0，其中P2q是s. t。P2=P2qG.我们必须重新应用该算法：我们计算gcd（P2q，G）= 1，并且通过命题2.3，它等价于证明了P2q= 0（这是通过ACF的定义来证明的）。在Coq中，如前所述，在展开P2和Q2的定义之后，我们可以应用策略qelim：Coq目标存在x： C，UPeval x P2 = C 0/\ UPeval x Q2> C 0。Unnamed_thm<展开P2，Q2; qelim.证明完成。4.1.3案例a：失败最后，为了说明我们策略的完整性，我们可以给出一个失败的例子（在情况a中）。这种情况可能发生在试图证明以下命题时：x.P1=0<$Q1=0<$Q2= 0这里，P1和Q1是互质的，不可能找到公共根（实际上，Q2上的条件是无关紧要的，因为我们不能解决P1和Q1之间的约束）。在Coq中，我们有：Coq<目标存在x：C，UPeval x P1 = C 0/\UPeval x Q1 = C 0/\CoqUPeval x Q2> C0。Unnamed_thm展开P1，Q1，Q2; qelim.顶层输入，字符739-744> unfold P1，Q1，Q2; qelim.>^错误：策略失败“此系统没有解决方案！“68D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）57其中错误是由策略qelim引起的，该策略未能应用（因为要证明的陈述是错误的）。4.2另一示例一个更复杂的例子可以从一个几何问题中得到启发。例如，让我们考虑由以下多项式定义的两条曲线和一条直线：四次曲线=X4+X3+X2+X三次曲线=X3+X2+X+1直线=X+1问题是要知道是否存在两条曲线上但不在直线上的点，即。我们可以证明以下命题：x.x4+x3+x2+x=0非正式地，我们知道有3个点是x4+x3+x2+x= 0和x3+x2+x+1 = 0的解：i，−i和−1。解−1不满足x+1 = 0，但另外两个复解满足。因此，这个问题有一个解决方案。在Coq中，如果我们假设相应的四次、三次多项式线已经被定义，我们有：Coq目标存在x：C， UPeval xquartic = C 0/\Coq UPeval xcubic = C0/\ UPeval xline> C0。展开<四次、三次、直线;qelim。证明完成。5相关工作量化消除是计算机代数中一个非常丰富的主题。已经进行了许多研究，主要是在实闭场（RCF），但也超过ACF。关于ACFs和w.r.t.根据我们的方法，这些研究通常是在复数的特定背景下（假设零特征），或者不旨在在DS中实现（显然不考虑CAS这样做）。例如，我们可以参考John Harrison [11]在HOL证明助手中为一阶代数理论开发了一个决策程序，以证明FTA。Hervé Perdry在他的博士论文[18]中给出了一个简单的算法，灵感来自一种圆柱代数分解。最后，Doug Ierardi [14]给出了ACF的快速并行决策过程。D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）5769关于RCF，历史上，第一个量化消除算法是由Alfred Tarki [21]给出的（另见Abraham Seidenberg [20]的工作处理RCF的主要问题是算法的复杂性。因此，我们可以找到大量的文献，旨在提高这些领域的定量消除的效率。按时间顺序，我们有Kreisel-Krivine [15]，Collins [5]，Heintz-Roy-Solerne [13]，Renegar [19]的工作，他们给出了双指数算法，最近，最好的算法（w.r.t.最坏情况下的复杂性）的问题出现在[2]。其中一些算法已经在一些定理证明器中实现。例如，John Harrison [10]在HOL中使用Kreisel-Krivine算法的变体来实现这一点。在Coq中，Assia Mahboubi和Loïc Pottier [16]使用[3]中描述的Tarski-Seidenberg原理处理次数至多为3的单变量多项式。6结论6.1总结在这项工作中，已经实现了几个目标。首先，我们以一种原始的方式证明了ACF的一阶理论（对于单变量情况）的可判定性，即使用纯粹的构造性风格（没有排除中间和应用有根据的归纳方案）。从这个证明，我们已经能够提取一个量化消除算法的一阶理论的ACFs。接下来，我们已经描述了一个一般的方法来执行这个算法在DS中使用CAS的一些计算（本质上是gcd）在一个纯粹的怀疑的方式。最后，我们提出了一个实现，我们开发的框架Coq和Maple，以及一些例子，可以处理。如果从CAS导入计算以增强DS的计算能力可以被认为是这些天的常规，那么这个实现具体地展示了CAS计算如何也可以用于增强DS的自动化能力。6.2今后工作作为未来的工作，我们想处理多元多项式。然而，我们的程序不能直接扩展到这样做。 实际上，例如，即使我们将K[X，Y]的多元多项式视为K[X][Y]的递归单变量多项式，我们的过程也不能递归地重用，因为尽管K是场，但K[X]不是。因此，为了将我们的工作推广到多元情况，我们必须同时处理所有变量。 一个初步的想法可能是将问题转化为解决一个系统，70D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）57多项式方程（使用Rabinowitsch技巧将不等式转换为等效方程，即 x/= yz. （x-y）z+1 = 0）。 然后，我们可以使用，例如，Gröbner基（其计算也可以从Maple导入）来得到等价的三角系统，可以（通过替换）求解，或者希尔伯特的零点（更恰当地使用弱零点推论，说明I是K [ X 1，.，X n]I）中的所有多项式都存在公共零点，建立由系统的多项式生成的理想，并证明它是真理想。这项工作的另一个延伸可以是考虑区域合作框架。实际上，我们算法的主要部分可以重用（几乎所有的东西，除了用ACF的定义或命题2.2结束时），以适应RCF的量化消除。在这些域上，我们也可以扩展处理符号>的代数。这样的扩展将是有趣的，而不是方法本身（如第5节所述，在这个领域的文献非常丰富），但总是在DS中使用 a CAS。这使我们能够理解，在Coq和Maple的特定框架中，这项工作如何与[16]正交，即使这旨在处理相同的问题。确认我们要感谢Thierry Coquand，他帮助我们使用CAS将程序集成到DS中（特别是通过Bézout定理处理gcd证明还要感谢Hervé Perdry，他关于RCF上的量化消除的许多讨论启发了我们设计这种ACF方法。引用[1] Henk Barendregt和Arjeh M.科恩数学的电子通信和计算机代数系统和证明助手的相互作用。Journal of Symbolic Computation（JSC），32（1/2）：3[2] Saugata Basu，Richard Pollack，and Marie-Françoise Roy.论量化器消除的组合和代数复杂性ACM 杂志。，43（6）：1002在Proc中扩展摘要第35届计算机科学基金会学术研讨会，（1994）。[3] Jacek Bochniak，Michel Coste，and Marie-Françoise Roy.《实代数几何》，《数学与工程》第36卷。3.第三章。 Folge/A Series of Modern Surveys in Mathematics（英语：A Series ofModern Surveys in Mathematics）Springer-Verlag，1998. ISBN 3-540-64663-9。[4] 布鲁斯·W作者：Keith O.Geddes，Gaston H.本顿·冈内特作者：Michael B.Monagan和Stephen M. 瓦 特 Maple V 语 言 参 考 手 册 Springer-Verlag ， New York ， 1991.ISBN0387976221。D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）5771[5] George E.柯林斯实闭域的圆柱代数分解的第二届GI自动机理论和形式语言会议，第33卷，第134-183页。Springer-Verlag LNCS，1976年。[6] 大卫德拉哈耶一战术语言为系统Coq。 在Proceedings of Logic for Programming and Automated Reasoning（LPAR ），ReunionIsland （ France ） ， 1955 年 ， 第 85-95 页 。 Springer-Verlag LNCS/LNAI ， 2000 年 11 月 。http://cedric.cnam.fr/~delahaye/publications/LPAR2000-ltac.ps.gz。[7] 大卫·德拉哈耶和米凯拉·马约罗Field：une procédure de decision pour les nombres réelsenCoq.InJournées Francophones des Langages Appliatifs，Pontarlier（France）.INRIA，Janvier 2001. http://cedric.cnam.fr/~delahaye/publications/JFLA2000-Field.ps.gz。[8] 大卫·德拉哈耶和米凯拉·马约罗Coq中域上代数表达式的处理使用Maple。Journal of Symbolic Computation（JSC），2005.地出现。[9] Herman Geuvers ， Freek Wiedijk ， JanZwanenburg ， Randy Pollack ， and HenkBarendregt.“代数基本定理”项目，2000年。 http://www.cs.kun.nl/gi/projects/fta/。[10] 约翰·哈里森。用实数证明定理。Springer-Verlag，1998. ISBN3-540- 762566-6。[11] 约翰·哈里森。HOL中的复量化器消除。在理查德J。作者声明：Paul B.Jackson，编辑，TPHOLs2001：补充诉讼，第159-174页。爱丁堡大学信息学系，2001年。出版为信息学报告系列EDI-INF-RR-0046。 可在网上查阅：http：//www.informatics.ed.ac.uk/publications/report/0046。赫塔姆湖[12] 约翰·哈里森和劳伦特·泰瑞 一个怀疑论者Journal of Automated Reasoning，21：279[13] Joos Heintz，Marie-Françoise Roy，and Pablo Solerne.在塔斯基-塞登伯格的复杂性上。Bull.Soc. math. France，118：101[14] 道格·伊拉尔迪 代数闭域理论中的量子消元。在第21届ACM计算理论研讨会论文集，第138147. ACM Press，1989.[15] 格奥尔格·克赖塞尔和让·路易斯·克里文。数学逻辑基础：模型理论。Dunod，1964年。[16] Assia Mahboubi和Loic Pottier。消除对Coq相关性的定量分析。在《法语国家应用语言杂志》（法国）。INRIA，Janvier 2002.[17] 库尔特·梅尔霍恩可靠的计算机软件挑战RASC。在计算机科学透视中，计算机科学讲义第2598卷，第255Springer-Verlag，2003.[18] Hervé Perdry.价值体系理论的构成方面。博士论文，弗朗什孔泰大学[19] 詹姆斯·雷尼加论实数的一阶理论的计算复杂性和几何学Journal of Symbolic Computation（JSC），13（3）：255[20] 亚伯拉罕·塞登伯格初等代数的一种新判定方法。Annals of Mathematics，60：365[21] 阿尔弗雷德·塔斯基初等代数与初等几何的一种判定方法。加州大学出版社，1951年。先前的版本作为技术报告由兰德公司于1948年出版; C. 麦肯锡。[22] Coq开发团队Coq Proof Assistant参考手册8.0版。INRIA- Rocquencourt，2005年1月。http://coq.inria.fr/doc-eng.html。72D. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）57A证明在下文中，根据我们的惯例，符号P（xi）将默认表示多项式P（X）和xi（X）的乘积，而在数量因子x下，它将表示P（x）和xi（x）的乘积，即P（X）和xi（X）在x处的对应函数的值;然而，在命题2.2到2.4的证明中将进行局部例外，其中它将表示P（X）在xi处的对应函数的值。主要定理，我们需要在我们的证明是Bézout定理A.1（Bézout定理）设P和Q是两个非零多项式。设G= gcd（P，Q）. 存在两个多项式A和B，s.t. AP+BQ= G。命题2.1（公共根）设P1和P2是两个非零多项式。设G= gcd（P1，P2）.我们有：P1=0P2=0 i P 2 =0iG= 0。证据如果P1或P2是一个常数多项式，则G= 1，定理平凡地成立;否则，我们有：• 设x0是P1和P2的根. 我们拥有：P1=（X−x0）Q1P2=（X−x0）Q2使用BézoutG=AP1+BP2=A（X−x0）Q1+B（X−x0）Q2=（X−x0）（AQ1+BQ2）也就是说，x0也是G的根。• 设x0是G的一个根。我们有G=（x− x0）G1，P1=GQ1=（X−x0）G1Q1P2=GQ2=（X−x0）G1Q2也就是说x0也是P1和P2的根。Q命题2.2（非根值的存在性）设Q是一个非零多项式。我们有：x.Q/= 0。证据• deg（Q）= 0：Q=a/= 0，其中a是常数，任何x都是。• deg（Q）>0：我们知道，1 +Q= 0（根据ACF的定义，因为deg（Q）= deg（1 +Q）>0）。设x0为验证该命题的值，即s.t.1+Q（x0）= 0。那么x0是s. t。Q（x0）= −1 =0。QD. Delahaye，M.Mayero/Electronic Notes in Theoretical Computer Science 151（2006）5773命题2.3（相对素多项式的根）设P和Q是两个互质的非零多项式（即gcd（P，Q）= 1）。 我们拥有：x.P=0证据• 设x0为s.t. P（x0）= 0和Q（x0）= 0。 简单地说，我们有P（x0）=0。• 我们有gcd（P，Q）= 1。利用Bézout定理（定理A.