多项式与超越函数相关问题的判定过程及其在控制系统中的应用

理论计算机科学电子笔记151（2006）111-125www.elsevier.com/locate/entcs控制系统Ruth Hardy露丝·哈代1，2圣安德鲁斯大学计算机科学学院圣安德鲁斯摘要本文给出了多项式与超越函数相关问题的一个判定过程。该程序适用于函数是连续可微分的有限个点的交点在一个封闭的凸集。 它决定的问题的形式wheeen∈{=，>，<}. 在映射和PVS执行过程中执行的最佳执行将限制执行枫树， PVS和QEPCAD连接。正是在 目前有限 对于那些两次不可分割的导数是有理函数的函数（有理可导）。这个过程特别适用于控制系统的分析，以确定重要的性质，如稳定性。关键词：可靠数学，形式化方法，量化消除，控制系统，Maple-PVS，QEPCAD1介绍数学、计算机科学和控制工程领域中的许多问题都可以归结为决策和量化消元问题[7]、[14]、[20]，通常涉及三角函数和超越函数;代数曲面求交和显示问题;机器人运动规划问题1.感谢Ursula Martin和Richard Boulton的帮助和指导，特别是在本书的早期阶段，也感谢Roy Dyckho和Steve Linton的持续帮助和指导。另外还要感谢John Hall、RickHyde和Yoge Patel分享他们对控制工程的见解，并感谢Rob Arthan、Tom Kelsey和Colin2Ema il：rh@d c s. st-and。梭uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.026112R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111（其目的是确定一些物体，其物理属性和运动范围可以用代数来描述，是否可以从一些初始配置移动到一些最终配置）;稳定性分析，使用冯诺依曼条件的稳定性差分格式。实闭域（RCF）的量化消除算法已经被定义[6]，[17]，[18]，并且针对涉及三角函数或超越函数的特殊类型的问题提出了各种算法[ 2 ]，[ 21 ]，但这些算法仅限于非常具体的问题，并且通常不包括对反三角函数或超越函数（如arctan或自然对数）的支持，这些函数在控制工程中很重要。控制系统分析中出现的一个问题是确定给定函数是否大于区间内的另一个函数[10]。本文给出了这类函数f：R2→R问题的一个判定过程，连续可区分的有限数量的点，闭凸集（一个集合，使得位于集合的两个端点之间的每个元素都是集合的成员，并且集合的边界点是它的该方法要求对数学公式进行高效、可靠的符号处理和精确的没有任何一个现有的工具具备所有这些特性。计算机代数系统（CAS）在符号操作方面表现出色，通常为数值计算提供了强大的方法，但它们不能保证正确的结果;形式定理证明器（TP）可以保证正确的结果，但对于自动符号操作和数值计算来说效率低下。人们对开发能够提供CAS的能力和TP的严格性的系统非常感兴趣这种类型的系统分为两个主要类别：对TP的计算支持和对CAS的正式支持Maple-HOL [ 11 ]和Maple-Isabelle [ 3 ]等系统提供了TP HOL和Isabelle与CAS Maple之间的链接，允许TP在适当的情况下调用Maple的计算能力，以提高证明或证明搜索的效率; Maple-PVS [ 1 ]提供了Maple与TP PVS之间的链接，允许Maple调用PVS的定理证明能力，以提高其结果的可靠性; Omega证明开发系统[ 15 ]支持在证明规划阶段将计算机代数集成到机械化推理系统中[5]扩展CAS，支持形式定理证明。的原型工具利用Maple-PVS系统提供的可靠有效的数学运算，在Maple-PVS系统中实现了决策过程判定程序适用的公式在本文第2节中根据实数的一阶逻辑L的一个片段进行了曲线的各种重要几何性质在第三节中给出。R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111113在第四节中，描述了基于曲线的几何性质来判定语言L的句子的过程在第5节中，讨论了与程序自动化相关的实际问题，并给出了一个原型。本文介绍了一个结合Maple、PVS和QEPCAD的工具，它演示了如何将计算机代数、定理证明和数量消除系统结合起来，实现L中包含一个量化变量。第6节给出了一个简单的例子，分析控制系统的方法最后，结论和进一步工作的方向在第7节中提出。2分类闭凸集是Rn的一个子集，使得位于集合的两个成员之间的直线上的每个元素也是集合的成员，并且集合的所有极限点也是集合的成员。在一维情况下，集合D<$R是闭凸集当且仅当D是闭区间。连续可微分项是导数存在且连续的函数，也就是说，它是f（x）形式的表达式，使得f（x）存在且是连续项的向量有理项是一种特殊形式的连续可微项，并且是多项式在变量xi中的实系数ai的乘积。如果这些系数是非代数的，那么它们可以用具有实代数界的区间（a il，a iu）来描述。线性项是有理项的特殊形式，例如证明了它们在所有变量中都是线性的，即它们是形式a0+ni=0时aixi其中a0，ai是实代数数，xi是实变量。一有理可拓项是连续可拓项的一种特殊形式，项，使得它是可微分的，并且所有的偏导数都是有理项，即，它是f（x）形式的表达式，使得f存在并且是有理项的向量。有限有效项是具有有限个凸性和/或凸性区域的连续可微分项。L语言中的原子公式是指在某个闭凸集x ∈ D <$f（x）<$0上包含有限个等价项的方程或不等式，其中D是Rn的闭凸集，f： Rn→R且<$f ∈{=，>，<}. 任意公式都是通过对变量xi迭代应用命题算子，，<$和量化算子，得到的。每个公式都可以改写为等价的前束范式。如果x在公式φ中的所有出现都被量化，那么φ是一个封闭公式，给定实数上公式的自然解释，它要么是真的，要么是假的。114R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）1113曲线的几何性质函数f：Rn→R，其中domf是凸集，定义为凸函数，当：f（θx+（1−θ）y）≤θf（x）+（1−θ）f（y），x，y∈domf，0≤θ≤ 1从这个定义中可以推导出各种几何性质，例如，凸曲线在xi方向上的梯度不会减少，xi增加;3凸曲线位于其任何切线上或之上;在任何方向上，曲线位于在边界点处连接曲线的弦上或之下一个线性项既是凸的也是凹的，并且有无穷多个交点。从曲线中添加或减去线性函数可以保持曲线的凸性/凸性。4决策程序本节中描述的决策过程是为了采用第2节中描述的语言中的正规公式并输出输入的真值而开发的目前输入仅限于R或R2的函数。该程序是为应用于控制系统的分析而开发的，不仅适用于实闭域的语句，而且适用于导数为有理函数的任何它封装了一系列其他任何决策过程都没有涵盖的函数，包括自然对数和arctan，这是控制工程领域中特别重要的函数该过程依赖于一组条件，这些条件允许基于对曲线的凸性性质的检查（参见第3节）来确定曲线f：R2→R和平面p：R2→R=0的相对以及在一个封闭的凸集中仔细确定的若干点处的曲线和平面的检查。判定过程用于凸曲线的一组条件在下面详细描述，并针对区间D=[a，b]中的f：R→R进行说明只有凸曲线f（x）在凸集上的情况才像所有其他情况一样详细说明。情况与此对称凹情况是凸情况的反射，可以通过在适当的区域中查看−f（x假设曲线f（x）是连续可微的，并且在3需要注意的是，梯度的比较不是根据陡度（即梯度的范数），而是根据实际值进行的。R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111115闭凸集D，则：(i) 曲线在x∈D上为负当且仅当曲线在D的边界0f（x）(ii) 曲线在x∈D上是正的当且仅当下列互斥条件之一成立：(a) 曲线在任何方向上的梯度在区域内的任何（扩展）点处等于零，并且曲线在该点处为正。点，即，f（x）=（0，f1（x））或f（ x） = （ f2 （ x） ， 0 ） 且 f（x）>0(b) 曲线在任何方向上的梯度在该区域内的任何点处都不等于零，曲线在区域边界处为正a Bf（x）0a Bf（x）（0，f1）和f（f2，0）和f（边界（D））>00a Bf（x）0a B如果上述条件都不适用于凸曲线，则在曲线等于零的区域内至少有一个点对于一个变量的有限有效函数，任何感兴趣的区间都可以分成有限个区间，在这些区间上曲线要么是凸的，或凹，然而，对于多变量函数，可能存在曲线既不是凸也不是凹的区域（考虑z=x2−y2）。这些区域包含鞍点，必须单独处理。在这些116R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111在某些区域，函数在某些方向上是凸的，在其他方向上是凹的这些区域中函数的最大值和最小值位于边界上，并且这些边界上函数的符号可以用于确定该区域中曲线是正的还是负的。为了使用这里描述的条件来决定第2节中描述的语言的句子，闭凸集必须被分割成曲线是凸的、凹的或包含鞍点的区域判定过程采用第2节中描述的语言的前束范式中的句子φ，并执行以下步骤：步骤1：将φ中的存在量化转换为泛量化，给出φJ。这是一个简化算法的语法转换：x.P（x）变成<$x。P（x）步骤2：从φJ中取每个原子式fi<$i0，并确定区域凸性的Dij，Dij和包含鞍点的Dij。步骤3：对于domfi内的每个区域Di j，应用来自条件集合如果所有这些区域都满足正确的条件，则第i个如果条件不适用于任何区域，则公式的值为0。步骤4：通过将命题运算符应用于步骤3的真值，构造句子φJ（以及φ）的真值本节中给出的一组条件适用于有限有效的函数，即具有连续导数和有限个区域的函数，其中曲线是凸的或凹的。在实践中，这一要求被加强到有限有效的理性可区分的函数。在PVS中存在这些情况的覆盖证明以及该过程的终止证明，假定凸性是已知的，并且曲线是凸或凹的区域的数量在闭凸集中是有限的5Maple-PVS中的实现为了实现这一过程，必须能够可靠地计算连续可微分函数的交点、相应曲线的凸性和曲线在给定点处的符号。这不仅需要强大的符号操作，其结果是正确的保证，但也验证了数值计算。计算机代数系统（CAS）为符号操作和数学公式的分析提供了一种强有力的方法，R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111117执行第4节决定程序所要求的转换和计算。 但它们并不总是能保证正确的结果，在数值计算中常常忽略假设和边条件，产生偏置点误差。形式定理证明器为形式分析提供了强大的方法，但缺乏有效地执行符号操作或数值计算的能力。Maple-PVS [1]工具提供了CAS Maple [16]和定理证明器PVS [13]之间的链接。该系统允许Maple执行的计算由PVS正式验证Maple负责制定要证明的引理，并将其传递给PVS以及要采取的QEPCAD-PVS [19]工具提供了一个共享对象文件，可以由PVS加载，以允许通过外部函数调用访问QEPCAD[12]例程。PVS认为这些函数调用的结果是可靠的这个系统允许PVS在其证明中使用强大而有效的量化消除Maple-PVS系统已扩展为允许将QEPCAD共享对象文件自动加载到PVS中（参见图1）。这允许通过PVS策略调用QEPCAD例程。枫PVSQEPCAD共享目标文件PVS接口外部接口外部函数调用Fig. 1. Maple-PVS-QEPCAD。原型工具在Maple-PVS-QEPCAD系统中实现，以允许在正式和符号设置中应用第4节中描述的决策程序决策过程的原型工具是专门为控制工程领域而设计的。在尼科尔斯图分析[9]中，必须确定参数函数是否保持在平面上的某个用户需要向原型工具提供参数函数和区域的表示;元组的列表B，每个元组包含区间x∈[ai，bi]，所有这些都是不相交的，以及线lij和不等式符号lij。Li的每个元素表示一个约束在参数函数的范围每个元组表示域x∈[ai，bi]中Li中的约束的析取列表B表示由元组表示的约束的合取。118R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111图二、原点周围的不良区域示例5.1输入y=Y（ω），x=X（ω）B=[x∈[−1， 0]，[−1−x，>]，[1 +x，<]]，[x∈[0， 1]，[1−x，<]，[−1+x，>]]表示约束好吧（X（ω）∈[−1， 0]<$− 1−X（ω）>Y（ω）<$1 +X（ω）Y（ω）换句话说，参数曲线不能进入原点附近的菱形区域（见图2）。为了将决策过程应用于输入，需要一定量的预处理来正确地这需要输入的符号操作和数值计算，并且是一项非常适合Maple的任务，Maple通过Maplet提供原型工具的前端。它们提供了一个类似Java一个简单的类型检查机制确保输入的类型和格式正确Maple处理输入以形成用于决策过程的适当句子，并调用PVS，PVS又可以调用QEPCAD，以执行所需的验证。一旦过程完成，Maple将显示决策过程的结果，以及显示指定区域的边界线和曲线图的图。以下描述了在考虑曲线y=Y（ω）和x=X（ω）的参数方程以及包含区间x∈[ai，bi]的元组的列表B和线lij和不等式符号lij的列表Li。设fij（ω）=Y（ω）−lij（X（ω））(i) 对用户提供的输入进行类型检查，如果格式不正确，则会产生错误消息，原型工具会停止。R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111119(ii) Maple计算、重写和简化参数方程关于x的导数和二阶导数。由于决策过程依赖于曲线的凸性以及二阶导数的符号，因此确认Maple正确计算了这一点并且没有忽略任何重要的边条件是很重要的。Maple调用PVS来确认函数定义良好，并且是可区分的。如果PVS未能提供所需的证明，则原型工具将生成相应的错误消息并停止。(iii) 区间[ai，bi]是关于x的，但该过程将要求这些区间是关于ω，i，e。[ai，bi] = [X（ωik），X（ωik+1）].为了用ω计算这些区间，必须找到ai=X（ωik）或bi=X（ωik）的所有实数解，然后通过观察每个ωik和ωik+1之间的一个点，就可以确定相应的区间。由于Maple使用数值计算来完成此操作，因此它可以避免由计算点错误引起的不精确算法问题，并且可能无法找到所有解决方案。为了确保所有的解决方案已被发现，它必须表明，解决方案发现的Maple实际上是近似的解决方案，并有没有其他的解决方案，在区间[ai，bi]。设Di表示Maple解周围的小区间(1)好吧ω∈Di<$X（ω）= ai<$X（ω）= bi以确保在时间间隔内有解决方案，(2)ω1，ω2。ω1∈ Di<$ω2∈ Di<$（X（ω1）=ai<$X（ω1）=bi）<$（X（ω2）=ai<$X（ω2）=bi）<$ω1=ω2以确保在每个间隔中只有一个解。决策程序也适用于（3）ω。ω∈/D<$X（ω）/=ai<$X（ω）/=bi其中D是实数x的集合，使得x ∈ D0<$x ∈ D1<$。. ，以确保除了Maple找到的解决方案之外没有其他解决方案如果失败，prototype工具将产生一个适当的错误消息并停止。为了补偿MapleMaple计算ωik和ωik+1，使得[ai，bi][X（ωik），X（ωik+1）]，然后Maple调整一些δ，使得[ai，bi]<$[ X（ωik−δ），X（ωik+1+δ）]。重要的是，此条件成立，因此Maple调用PVS来验证解决方案如果PVS未能提供所需的证明，则原型工具将生成相应的错误消息并停止。120R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111(iv) Maple计算fij在区间[ωik−δ，ωik+1+δ]中的反截点，这是使用数值方法来找到fij对x的二阶导数（与二阶导数相同）的在步骤ii）中计算的参数曲线的Δ V为零，并且因此由于不精确的算术而导致误差为了避免这个问题，Maple计算小区间[pikm−δ，pikm+δ]，其中点Lie（称为插入间隔）。 PVS被要求确认不仅这些区间包含两个严格凸或凹的区域之间的真实相交点而不是零曲率点，而且这些点中的每一个都是[pikm−δ，pikm+δ]，并且fij在[pikm−δ，pikm+δ]中的导数不等于零，除非它正好在交点处。这是一这是PVS解决的相对困难的问题，但由于fij的导数和二阶导数是合理的，因此它是量化消除的理想选择PVS使用QEPCAD-PVS链接调用QEPCAD策略来验证Maple如果PVS未能提供所需的证明，则原型工具将生成相应的错误消息并停止。(v) 区 间 [ωik−δ ， ωik+1+δ] 被 分 割 成 [ωik−δ ， pikm−δ][pikm−δ ，pikm+δ][pikm+δ，ωik+1+δ]，在这些区间上，曲线要么是凸的，要么是凹的，要么是一个区间。(vi) Maple以λω ∈ [a，b]的形式给出了PVS要解决的引理。fij（ω）<$ij0使用不等式符号<$ij和上一步计算的区间。PVS被Maple称为证明这些引理，实质上确定来自条件集合的期望情况是否在区间的情况下，句子的真实性不是使用第4节的情况之一来发现的，而是在必要时通过检查区间的界限来确定的，因为由于这些区间的性质，fij的最大值和最小值必须位于界限上的原子公式fij<$ij0的真值是从合取中建立起来的对应引理的每个真值(vii) 由每个Li表示的公式的真值由每个fijij0的真值的析取建立。然后，由B表示的公式的真值由每个Li的真值的合取建立。prototype工具会生成一条适当的消息，说明公式是真还是假。(viii) Maple生成直线图和曲线的参数图PVS使用定制的库，其中包含有关控制系统分析中重要的各种函数的可区分性的引理，例如R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111121arctan、自然对数、以10为底的对数、任意有理函数和参数函数，以及对QEPCAD的高级策略和这些库包含自然对数和arctan作为泰勒级数的定义，这允许定义任何给定输入的这些函数的值的界限6一个简单的例子在本节中，我们将给出一个简单的例子，说明如何使用第4的决策过程和第5节中给出的实现来正式确定曲线是否与直线相交。 给出的例子是典型的形式，出现在尼科尔斯图分析控制系统。这是一个特别有趣的例子，因为曲线包含凸性和凸性的区间，曲线垂直的点和多个关于ω的区间对应于一个关于x的区间。考虑以下边界线和参数方程（见图（3）：B= x ∈ [− 1. 五，零。5]，[[55 + 8x，>]，[65− 12x，<]] 10 ln（p）−20 ln（ω6+5ω4 + 60ω2 + 16）Y（ω）=X（ω）=arctan，其中ω≥0，以及中文（简体）.797 ω6+ 14382 ω4+ 755 ω2− 3194ω800ω8+ 4803ω6+ 12054ω4−1597ω2+ 55p= 640000ω16 + 7684800ω14 + 42990418ω12 +136160432ω10338091528ω8− 21346562ω6− 87425842ω4− 4998610ω2+ 10204661Maple计算给定的导数fJ和二阶导数fJJ，参数函数考虑ln（10）为范围（2. 302585090，2. 302585100），导数和二阶导数都是有理函数。Maple调用PVS来确认参数函数是两次可微分的，并且导数是Maple指定的。对于PVS来说，这是一个相对简单的任务，它使用定制的库和强大的通用简化和重写策略（如GRIND）来提供相关的证明。下一步是确定ω上对应于X（ω）∈[−1]的区间。五，零。5]。Maple计算X（ω1j）= −1的所有解。5且X（ω1j）= 0。5丢弃所有122R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111这留下三个解ω1，1= 0。4231452940，ω1，2= 0。7664324880和ω1，3= 1。631039454，给出了四个潜在的对应区间：[−∞，ω1，1]，[ω1，1，ω1，2]，[ω1，2，ω1，3]，[ω1，3，∞]Maple确认这些确实是近似解，并且通过让δ = 0，它们是函数定义域中的唯一解。001.将决策程序应用于好吧 ω ∈ [ω1，i− δ，ω1，i+ δ]<$X（ω）= − 1. 5<$X（ω）= 0。5.确定解的存在性，ω1，ω2。ω1∈ [ω1，i− δ，ω1，i+ δ]<$ω2∈ [ω1，i− δ，ω1，i+ δ]<$（X（ω1）= −1. 5 <$X（ω1）= 0。5）n（X（ω2）= −1. 5 <$X（ω2）= 0。第五章）ω1=ω2确定每个区间内每个解的唯一性，好吧ω≥0<$ω∈/[ω1，1−δ，ω1，1+δ]<$ω∈/[ω1，2−δ，ω1，2+δ]<$ω∈/[ω1，3−δ，ω1，3+δ]<$X（ω）−1。5<$X（ω）=0。5由于这些问题都不涉及参数方程，因此判定过程的应用要简单得多，并且不需要应用第5节中的步骤iii。而且，由于前两个问题中没有交点（在大多数情况下也不可能有交点，因为感兴趣的区间很小），该过程的应用再次简化，不需要像第5节中步骤iv和v所描述的那样将区间分割成子区间。一旦确认Maple找到的解确实是正确的，就检查每个区间内的一个点，确定[ω1，1，ω1，2]和[ω1，3，∞]对应于区间X（ω）∈[−1]。五，零。5]。为了确保这些间隔的界限是δ = 0。01;下界减少δ，上界增加δ。在这一点上，Maple调用PVS来确认其计算是正确的，即[-1。五，零。5]<$[X（ω1，1-δ），X（ω1，2+ δ）]和[limω→∞X（ω），0. [limω→∞X（ω），X（ω1，3+δ）].PVS使用自定义构建的库，并调用QEPCAD以确保此安全属性。Maple计算参数函数的不连续点，包括通过确定二阶导数的分母和分子等于零的点而变得垂直的点。对不在任何感兴趣区间内的所有点进行分类，留下单个点ω1，3，1= 1。在区间[limω→∞X（ω），X（ω1，3+δ）]内，求出了一个线性方程组。 枫计算插入间隔[ω1，3，1−δ，ω1，3，1+δ]并调用PVS，使用QEPCAD策略证明了只有一个干扰点R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111123在区间中，没有导数等于零的点<$ω ∈ [ω1，3，1− δ，ω1，3，1+ δ]。<$ω2∈ [ω1，3，1− δ，ω1，3，1+ δ]。（fJJ（ω）= 0<$fJJ（ω2）= 0）<$ω=ω2J<$ω∈[ω1，3，1−δ，ω1，3，1+δ].f（ω）−8 = 0J<$ω∈[ω1，3，1−δ，ω1，3，1+δ].f（ω）+ 12/ = 0然后Maple用公式表示适当的引理（4）λω∈ [ω1，1− δ，ω1，2+ δ]。Y（ω）−l1，1（X（ω））<$1，10<$Y（ω）−l1，2（X（ω））<$1，20(5)λω∈ [ω1，3− δ，ω1，3，1− δ]。Y（ω）−l1，1（X（ω））<$1，10 <$Y（ω）− l1，2（X（ω））<$1，20（6）λω∈ [ω1，3，1−δ，ω1，3，1+ δ].Y（ω）−l1，1（X（ω））<$1，10<$Y（ω）−l1，2（X（ω））<$1，20(7)λω∈ [ω1，3，1+ δ，∞]。Y（ω）−l1，1（X（ω））<$1，10<$Y（ω）−l1，2（X（ω））<$1，20这些引理中的每一个都对应于决策过程中使用的一种情况，或者对应于一个区间。对于引理4、5和7，PVS使用来自判定过程的适当情况来形成证明，引理6的证明直接从引理5和7的真值得出。这就完成了决策过程的计算。Maple显示了这个公式的真实性以及直线和参数曲线的图，如图3所示。7结论和今后的工作本文给出的判定过程允许人们判定闭凸集上的有限自反函数的句子的真值这封装了一系列的功能，不包括现有的决策程序，并在数学，计算机科学和控制工程中有广泛的应用该过程需要符号处理、数值计算和形式化的数学分析。实现该程序的原型工具利用现有的Maple-PVS链接提供可靠的数学计算，并利用QEPCAD-PVS链接利用现有的量化器消除技术。该过程目前适用于R2的函数，而原型工具在包含单个量化变量的公式中实现了R今后的工作包括扩大124R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111图三. Y相对于X的参数图，显示线l1，1和l1，2。决策过程更高的维度的功能，提高效率，目前的原型工具，并扩展其功能，包括决策涉及更高的维度与大量的量化变量的功能引用[1] A亚当斯，M邓斯坦，H戈特利布森，T凯尔西，U马丁和S奥雷。 计算机代数满足自动定理证明：集成Maple和PVS。In R. J Boulton和P. B Jackson，编辑，第14届高阶逻辑定理证明国际会议论文集（TPHOLs 2001），计算机科学讲义第2152卷，第27-42页。Springer-Verlag，2001.[2] H Anai和V Weispfenning。 决定线性三角问题。 在C Traverso，编辑，ISSAC北京：人民出版社，2000年。[3] C Ballarin，K Homann和J Calmet。定理与算法： isabelle 与maple之间的接口。以 . H. MLevelt，编辑，ISSACACM Press，1995.[4] A Bauer ， E Clark ， 和 X Zhao. Analytica - 结 合 定 理 证 明 和 符 号 计 算 的 实 验 。 Journal ofAutomated Reasoning，21（3）：295[5] B Buchberger，T Jebelean，F Kriftner，M Marin，E Tomuta和D Vasaru。一个定理项目的调查。在W Kuechlin，编辑，ISSACACM Press，1997.[6] B. F Caviness和J. R Johnson，编辑。量化器消元和圆柱代数分解。Springer Wien纽约，1998年。[7] 多尔兹曼用实数量化消元法求解几何问题。技术报告Rep. MIP-9903，UniversitétPassa u，1999.[8] 多尔兹曼和斯特姆Redlog ：计算机代数满足计算机逻辑。ACM SIGSAM Bulletin ，31（2）：2R. Hardy/Electronic Notes in Theoretical Computer Science 151（2006）111125[9] R. C Dorf和R.毕晓普。现代控制系统。Prentice-Hall，第九版，2001年。[10] 行动小组FM（AG08）。鲁棒性光控制设计挑战问题公式化和手册：高发病率研究模型（HHHRM）。技术报告TP-088-4，第3版，欧洲航空研究和技术小组，1997年。[11] JHarrisonandLDThhhry.请参阅以下表格：HOL和MA P LE的格式。在A Voronkov，编辑，逻辑编程和自动推理：第四届国际会议论文集，LPARSpringer-Verlag，1993.[12] H洪。 Qepcad。 可查阅http://www.cs.usna.edu/www.qepcad/B/QEPCAD.html。[13] SRI International. PVS。 可在www.example.com上获得http://pvs.csi.sri.com。[14] 吉尔斯特兰先生。非线性控制系统的量化消元法设计Journal of Symbolic Computation，24（2）：137[15] M Kerber，M Kohlhase，and V Sorge. 将计算机代数集成到证明计划中。Journal of Automated Reasoning，21（3）：327[16] Maplesoft 枫树 可在http://www.maplesoft.com/products/maple/上获得。[17] 塞登伯格初等代数的一种新判定法。Annals of Math，60：365-374，1954.[18] 塔斯基初等代数和几何的一种判定方法。加州大学出版社，1951年。[19] 蒂瓦里人PVS-QEPCAD。提供http://www.csl.sri.com/users/tiwari/qepcad.html网站。[20] 维·韦斯芬宁通过量化器消除的模拟和优化。Journal of Symbolic Computation，24（2）：189[21] 维·韦斯芬宁 决定线性指数问题。 SIGSAM Bullettin，34（1）：30