毕业设计论文 外文文献翻译 自动化专业 Automation 中英文对照.doc

《毕业设计论文 外文文献翻译 自动化专业 Automation 中英文对照.doc》由会员分享，可在线阅读，更多相关《毕业设计论文 外文文献翻译 自动化专业 Automation 中英文对照.doc（40页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、编号： 毕业设计英文翻译译文 题 目: Automation 院 系： 计算机系 专 业： 自动化 学生姓名： 学 号： 指导教师： 职 称： 2005 年 6 月 3日自动化汤姆里治2005 年四月 12 日目 录1 介绍 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 2 需求. . . . . . . . . . . . . . . . . . . . . . . . .

2、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 3 目前交互式证明器的自动化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4 4 技术. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3、. . . . . . . . . . . . . 5 4.1 证明的搜寻. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 逻辑系统. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6引进规那么. .

4、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.2 等式. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 改写. . . . . . . . . . . . . . . .

5、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 条件的简单化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 动态的完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 方程式的统一. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7、 . . . . . . . . . . . . . . . . . . .125 连接与整合. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 6 评估. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8、 . . . .13 6.1 评估生产需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .136.2 完整性. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 6.3 效率. . . .

9、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 6.4 实际应用. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7 替代选择. . . . . . . . . . . . . . . . .

10、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 8 结论. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19 1 介绍自动化可能是成功的机械化的关键。在一些情形中，机械化不需要自动化就可以实行。确实，在高度抽象的数学区域，大局部由使用者拼出的复杂

11、证明组成的机械化推论远远超过了那些目前能被自动化解决的范围。在这一背景下，如果自动化它被全部使用， 将指导在容易的可以解决的被紧紧地限定的次问题上。一个机械化的典型例子是我们的拉姆齐定理的形式化。另一方面，在推论相对被限制的地方，自动化能富有成效地在确认类型的证明中被应用，但是绝对程度的细节将使一个非自动化的机械化不可实行。许多人已经花费了数年来开展全自动系统。比方Vampire VR 和otter McC全自动系统。我们可以和这样的系统竞争的设想是愚蠢的。它们的执行是一种方式，这种方式超过目前在交互式定理证明器被实行的系统。这些方案正在进行是为了把这些系统和交互式定理证明器相连。这是极其有价

12、值的工作：如果知道一个一阶的陈述是可证明的，这时应该期待机器能提供一个证明。在这一节中，我们简略说明一些我们已经在各种不同的情况应用研究的技术。自然地我们不企图仅此一次去解决自动化推论的问题。宁可我们把重心集中在问题，而这些问题典型地出现在我们已经涉及的研究。我们首先简略说明我们需要的自动化的引擎功能。我们然后描述我们应用的技术，而且他们是如何整合的。我们评估根据我们的需求性质上地产生的引擎，和数量地有关于一件相当大的案例研究。这些技术中的少数是新奇的，宁可，我们企图用一种适宜的方式来融合现行的技术。这些步骤在HOL启发定理证明器被开展，这是我们建立的设计原型的一辆优良车辆的不同方法。2 需求

13、我们的自动化的需求是什么? 让我们区别一下自动化和全自动化的使用，以及交互式自动化的使用，每一种的需求都有非常地不同。也许料想不到地，失败的自动化证明引擎是基准，是观念，这观念是当交互式开展的复杂证明使我们花费大多数时间对 几乎 的可证明的义务的时候。因此我们想要证明器给我们完美的反响作为为什么任务不能够被执行的原因。这引证强调一种在自动化和交互式证明之间的重要的不同。在自动校对中，可典型地知道，目标是可证明的 ( 或至少，非常强烈地疑心，而且在结束相当多量的时间之前准备等候证明的搜寻)。确实，自动证明器被判断在他们能实际上证明多少可证明的目标之上。在交互式证明中， 我们花费我们大多数的时间在

14、几乎可证明的义务上。这是交互式和证明之间的不同。如果我们花费大部份的时间尝试去证明简单但不可证实的目标，然后校正的搜寻完全变成比拟不重要。这虽不能说是它全部失去重要:：如果一个系统缺乏完整性，这时它将会无法证明一些可证明的目标。什么类型的目标正在被放弃，这是非常必要而且主要去知道的，这是为了知道当一个证明器失败于证明一个目标时就能理解它是什么意思。这些知识也非常有用，当混合系统为了了解作为整个系统的行为，应当首先了解局部的行为。在一个交互式的环境中，在完全之上所有物可能被偏爱，就我们而言，自动化的最重要方面是简单化。 而这些我们不是意味着去落实简单 ( 要布多少根线来实现系统? 等等)，而是概

15、念上的简单化。例如，简单化到处被用于交互式定理求证。如果一组改写规那么不能融合，这时去了解简化器的行为，必须了解适用的规那么顺序。不用说，对于理解这是一件极端复杂的事情，而且属于这些所有物的证明在推测上极端易碎。概念上的简单化通过聚集和简易装置的终端对一个简化器进行紧密地约束。如果一个使用者要了解系统，概念上的简单化很重要。如果一个系统的概念简单，它将会很有希望被简单的使用。在一个交互式环境中，我们期待自动化失败。为了取得进步，我们必须了解一种证明的尝试为什么失败，证明器一定会提供反响。基于系统的决议能提供反响，但是他们是消灭性的 (在某种意义上目标转换成一种正常的形式在证明的尝试之前开始，破

16、坏了最初的逻辑结构)，所以反响很难被了解 (论证失败的点对于最初的目标能看出明显的不同)。较好的方式是引导在一个尽可能接近的方法证明到一个人类可能如何引导证明。在一些感觉中我们需要证明的系统应该是自然的。在这情况下，如果一种证明的尝试失败，失败的局部能时常被作为检验直接地返回给使用者。反响与能见度相关。时常一个使用者希望检查失败的证明，但是只有证明的踪迹是可得的，它能引起一个概念上的错误结合: 使用者把重心集中在结果，然而踪迹可能全部是有不同的自然。如果有许多没有被证明的局部，这时一个使用者不可能检查它们的全部，但是可能愿意沿着证明走。像约翰 哈里森的模式消除的执行的自动化方法，时常利用全球化

17、的节点优先寻址的信息在一棵树里搜寻一个证明。如果全球化的信息不是出现在结果中使用者有时机接近，它将会难以经过通过简单运用的自动证明器一步一次的自动化证明。当传导的搜寻正在使用全球化的信息时，自动证明器将不做出它做出的相同决定，因为它只能进入本地的结果。许多方法现在被交互式定理证明器所使用，就像伊莎贝尔的blast，留下未改变的目标如果它们失败于证明这目标的话。证明搜寻的自然方法期待在所有的情形中至少能做出一些进步，所以即使目标不是可证明的，它们也能够有所帮助。 比方，平安的步骤 (就像在许多系统的E) 应该被实行，简单化步骤被应用等等。自动化也应该是稳定的。在大量的证明中，一个证明时常混合交互

18、式和自动的证明。如果被自动化返回的目标容易根本地以目标的微小变化改变，这时关联的交互式证明将被毫无用处的给予，而且一定被改写。因为这一个理由，被自动化返回的不能解决的次目标应该在对于最初的目标的微小改变下稳定。如果一个证明能被建立，然后一开始把重心集中在使证明更加可维持的方面，就像鲁棒一样。效率是在蛋糕上的糖衣。完全也是重要的，虽然没有必要在一阶逻辑完全，但是宁可应该有一个给定的程序解决的层次问题一个清楚的观念。无论如何，一些系统的行为理论上理解是重要的，如果它接近简单的目标。让我们总结出这些观点： 自动化应该很简单：它应该在理论上很好地被了解，和在使用中可预期的。 自动化也应该提供反响，以至

19、于使用者能估定一种证明的尝试为什么失败。 一个甚至比拟强烈的需求是，自动化是可视的，在可视中通过证明的研究，能直接地检查自动化的执行。 自动化应该是自然的，这是为了使证明器和使用者之间的概念差距最小化。举例来说，自动化应该在标准的逻辑系统中执行，或者与使用者传导证明的决策程度相一致。 时常，使用者对一个证明进行优化有很多的平安步骤。与自动化在返回前至少做出改良相比，自动化简单的返回“可证明与“不可证明是没什么用处的。 自动化应该是稳定的，以至于在自动化的行为中理论上微小的改变不会产生大的变化。这是很重要的，因为交互式的证明包含大量隔行扫描使用者或自动化步骤的环节。 自动化也应该是鲁棒的，在意义

20、上微小的变化不会影响自动化的可证实性。 我们想要自动化对明显的理论是有效率的。 最后，我们想要自动化是完全精密的。她能很好的定义问题的层次。3 目前交互式证明器的自动化目前交互式定理证明器的自动化证明方法不符合先前环节的需求。Isabelle/ HOL是目前作为被认可的HOL执行的代表。 主要被使用的技术是一个描述的证明器blast，和简化器simp。这些都混合在单个的自动化策略里。 Isabelle也包括一个模式消除程序，它和blast使用起来有点相似。Simp 被广泛地使用，但是它并不是一个完全的一阶证明方法。然而，它能满足许多前期环节需求的事实解释了为什么它这么流行，在交互式证明中。bl

21、ast方法在肯定逻辑和组的简单问题上运行得很好，但是它很难了解它的特性是什么。它基于一个证明器leanTAP，那对一阶逻辑是完全的。另一方面，以下的目标稍微可证明在一阶逻辑，但是blast不行。f( g a)=a y g(f y)=y它甚至更加的混乱，但它在区间 g a 实现的时候，这区间在结果本身中发生，并是存在的证明。更糟的是，当像HOL 的类型逻辑被表达的时候，g a 是唯一的区间发生在可以使用的正确类型结果中。这一个失败对于有效地处理等式逻辑是一个描述类型程序失败的合并统一。因为它是这么的不受限制，所以自动方法几乎从不被用于交互式证明的中间。而且，它是不稳定的，在它产生的子目标中在对目

22、标的较小变化之下可能是野性地不同的，它的提出是无用的除了在紧紧地被控领域。整合一个现代的解决证明器Vampire进入Isabelle将没有必要纠正这些错误。基于解决的方式提供了一点支持对于交互式理论证明器，因为子句形式的减少意味着使用者有很少的可观性进入证明的搜寻，而且很少知道为什么一个特殊的辅助定理会失效。证明的搜寻是一个本地的向前的综合的搜寻，与一个全球化的向后的综合搜寻的典型描述介绍以及Isabelle的策略水平相反。因此，对于使用者，解决是一个不自然的系统。通常从这些系统来的反响是极差的甚至不存在的。此外，许多步骤应该被认为是平安的 (应用一个终端和聚合的改写组，运行一个 E 步骤)

23、因为系统被当作一个黑盒子使用，或目标率直地被解决，或者更通常，一点也不解决，而且系统包含的关于可靠应用的步骤被丧失的信息，留给使用者可以手动的应用这些步骤。这里的问题是系统无法做出改良那些无法直接证明的目标。我们也作关于一阶理论证明器的以下观察。这些证明器被设计去寻找大量的数量词实例，寻找可选择地系数平等推论。然而在交互式定理证明器里的自动化的失败没有失败于猜想大量的数量词实例。4 技术在下面这节，我们描述我们如何建立自动化。首先，我们正在尝试寻找证明，所以我们将会需要 ( 至少) 证明的搜寻引擎。然后，我们在很大的程度上愿做用手动的方式的模型证明。除了证明的搜寻之外，在手动证明中其他主要的利

24、用方法是简单化。我们描述我们怎样讨论简化器。有条件的简单化是一种简单化的形式，它的简化器采用递归的方式企图解决可能被应用的当前目标的改写选择。我们讨论正采用在这些目标上的简化器没有被最好的运行，并建议替代选择。然后，当使用简单化的时候，它是一个很好的方法去确定简单装置是集合的和终端的。我们描述完成的执行。当使用简单化的时候，然而，也想利用在改写一个证明的过程中产生的假设。确定改写规那么的组仍然是聚合的和终止的，就应该在证明搜寻时提供一些动态完成的形式。我们讨论我们如何抓住了这些议题。4.1证明的搜寻在这节中，我们描述我们证明搜寻的根本系统。这是一个单一的结论，对向后的证明搜寻是适当的直观系统。

25、我们避开统一的流行的区间计算。这有一些有趣的结果当混合证明搜寻时用其他的方法。注意我们只对自动化的一阶系统感兴趣。逻辑系统证明搜寻的二个主要系统是决议和描述。因为一个交互式环境的自动化，决议太不自然。因为这一原因，描述是更有希望的。我们因此限制我们的注意在基于描述的系统。描述系统典型地藉由否认目标而且寻找矛盾着手进行。我们甚至考虑到这是不自然的。我们因此集中在标准逻辑系统中直接执行的描述系统。使用这样一个系统根据复杂的执行有重要的意义，因为我们能只是简单地在 HOL 目标的水平搜寻使用或多或少标准的策略。这也对自然化有有利条件，因为使用者已经熟悉一个如此系统的证明和反响，因此我们能直接地对使用

26、者呈现失败的局部，这些使用者没有翻译出来自一些其它可能的证明系统的结果。单一结论系统对古典的证明是不适宜的，古典的证明被多样结论系统更好的支援。然而多样的结论系统是不自然的。如果我们对古典的证明感兴趣，我们一定成认我们的单一结论系统有缺点。另一方面，我们相信大规模的证明结构大概是直观的：我们典型地集中于一个目标，并且我们的辅助定理效劳作为证明中的中间观点，和我们的补助定理如证明的中间点效劳，即AB C作为一个补助定理对 (A B ) C不是典型地相等，因此我们期待在证明中到达一个点，这里A B 是可证明的，而不是去做一个可分的拆开。确定地对于我们感兴趣的领域，所有的证明本质上是直观的，以及古典

27、的推论被限制到可能被简单化或其他的限制技术处理的小区域。引进规那么我们希望做出更多的进步。虽然程序简述说明上方是完全的，它宁可是一边的。既然大多数的证明大量利用辅助定理，对应的目标传输容易变成相当拥挤。而且，当引进规定的时候，许多辅助定理自然地被浏览，也就是说，趋于使用精炼的结论 C 而不愿使用从开始向前连接着的结论。因为这些理由，我们也利用引进规那么 la PaulsonPNW03。这些典型不平安，但是如果我们再一次返回，而且轮流其他的防范，完全性就能被保存。这些引进规那么能像辅助定理一样被执行，但是被作记号作为引进规那么。在证明的搜寻时候，这些辅助定理的结论被相配对抗当前的目标。如果结论与

28、当前的目标相配，那么目标将被选择的引进规那么所代替，而且在事件中这些假定不能够被证明，那么返回将被采用。如果一条引进规那么标明是平安的，这时返回不发生。注意，这些提高没有必要来自理论的观点，而且它的唯一动机是做模型自然形式的证明。如果完全性以特定的方式被考虑，这时候能够看见完全性的保存。如果这些规那么是行为表现所预期的，那么在简单化之前需要等式的统一。然而，目前我们用手动的方式来模拟等式统一的使用。完全性失败对于引用规那么：如果我们以一条规那么作为一条引进规那么，这时我们无法是完全的? 不过这不是真实的，而且规那么是平安的，在哪一情况我们都很顺利，或不平安的，在哪一情况我们返回。需求的统一意味

29、着我们能防止我们能防止作为增加的假设而使用的规那么。然而，如果在一些阶段我们能以规那么作为一条引进规那么，这里有一个引进规那么被打算使用的环境，但是没有连接链，然而当一项额外的假定可能有时这里将没有统一的问题。而且，自从我们没有使用一个作为标准的辅助定理的规那么，使用完全化的概念将不是很清楚。让我们定义完全化的生产一个引进规那么去了解是否有一个证明作为一个辅助定理的规那么。这时一个使用规那么的证明作为一条引进规那么。在平等面前，我们应该因此使用统一去确定我们的引进规那么能被无论在那里都可能应用。既然在每个阶段我们有一个有限的场地区间组，与一个终端和集合的改写次序，这样一个方法能够可以实行，即使

30、在现阶段我们只能用人工模拟这样的步骤。引进规那么的使用会带来复杂化，因为完全化是否适合不清楚。如果引进规那么能作为一个正常的辅助定理使用，这时完全化是可以保存的，因此辅助定理被操作就像它是个正常的肯定逻辑。在一条引进规那么后面的方案是去平衡证明的搜寻，这会以别的方式主要地在左边上操作。在规那么 A B作为几个辅助定理和作为一个引进规那么之间的差异，是自动化能应用 L与一个作为辅助定理的规那么相结合。因此作为一个引进规那么，我们期望目标最终成为B和它能用A代替这些。4.2 等式改写改写是由用相等的子术语更换一个术语的变换过程。例如，我们可能使用辅助定理f (a) = a去改写Q f (f (a)

31、 到 Q f (a)然后到Q (a)。在这节中，我们的各种改写概念是非正式的。对于更多的信息读者可以请教优秀者。在用辞上的一个注解：一个简单化的次序是一个改写被限制的次序，过去一直用来证明一个区间改写系统的终止。然而，“简单化这个词时常被非正式地用于提到改写，而且“ 简化组这个词时常用来提及改写的系统规那么。我们下面采用这些非正式的用法。两个主要的简单化财富是终止和聚集。没有聚集，了解简化器的行为就必须知道改写被应用的次序。这太多而不是使用者所期待的。在一个交互式环境中终止非常有用，例如，它允许反响。而且，终止允许简单化与主要的证明的搜寻相整合。如果我们有聚集和终端，这时每一个区间有一个独特正

32、式形式，而且尝试的等式变得可决定。这是一个极其有用的简化组的财富。我们的根本策略是热心地应用简单化，在证明的搜寻每个步骤之后，使用假定去简化其他的假定和结论。我们用一个有终止和聚集的简化器工作。我们检查终止和聚集的手动使用完成。我们在个体的类型中应用简单化。如果简化组正在终止和聚合，这时它保存了证明搜寻的完全性。我们也在布尔类型应用简单化，但它不是一阶逻辑的一种可能性。例如，我们采用高阶对微小范围的数量词改写。不是太困难而无法争论而这也保存证明的搜寻完全。经常相似改写的假定在证明期间出现，而且这些可能被简化组合并。给一项假定x.P x和假定 P t，就可以简化 P t=，是再一次在布尔类型的简

33、化，而不是一阶的操作。我们不以这一种形式的假定作为改写：我们的对数量词例如的根本途径经由区间计算，而且使用这些简单化会破坏这方式的完全。我们使用假定形式x= y(可能数量化)来改写。 为了保有聚集和终止，我们完成简化组的生产并动态的产生改写。因为完成没被保证结束，完成被限制到一个步骤确实定数字，虽然在我们的应用中，完成总是成功。条件的简单化在这节中，我们描述有条件的简单化，并且注意到标准的途径去解决递归环境下简化器的实施可能没有被期待。我们建议一些其他的方法，而且讨论其他的有条件的简单化的问题。我们得出结论，目前有条件的简单化太复杂而无法作为 简单的 技术计算，并且确实太复杂而无法以一合理的方

34、式与证明的搜寻相连接。我们建议考虑有条件的改写就如平常的辅助定理的一样的替代选择。简单化的工作在于对形式a = b的改写，在目标的任何地方改写a到 b。有条件的简单化的工作在于对有条件的形式Aa = bA是一典型的连接的改写。在一个依次的 C 中，如果我们能证明C, 的话，我们就能在目标里调整a到b的改写。我们应该如何尝试去证明条件A? 假设我们正在用简单化连接一个完全的证明搜寻系统。在这情况下，非常好的 (从一个理论上的立场) 行为会被由需求获得，如果A是可证明的，那么它实际上是被证明的。因为对A的证明的搜寻是潜在的没有终止的，我们这时应该妥善地安排一个复杂的隔行扫描主要证明搜寻的过程，与子

35、证明搜寻企图去解决有条件的改写情况。一个如此方式是不适口的不只因为效率的原因。简单化的好处之一是，不像证明的搜寻，它正在终止。如果当采用有条件的简单化的时候，我们希望保存这一终止的行为，当企图证明条件的时候，我们应该遵行被涉及的非终止。一个我们应该采用的主要证明搜寻是去证明条件，但是限制对特别深度的搜寻。这也是不适口的。为了在一个合理的时间里保持简单化的运行，这深度应当非常小，因为条件的产生是很频繁的。这些小的深度不能提供更多的条件解决方法比其他简单的方法。对于一个小深度的有限制的证明搜寻，这也意味着它的理论限制也能成为实际的限制：任何的有限制的证明搜寻将会是不完全的，但是由于大的深度我们可以

36、有希望的忽略这样的不完全。小的深度意味着我们可能面临的条件能被解决的条件，这条件对于使用者是很清晰的，不过被限制的搜寻深度意味着情况没有被解决。根据我们的经验，深度必须至少有10个逻辑的步骤 ( E 及其他。)，连接中间有效的等式推论(我们想像一个情节我们有一个有效地处理等式的证明搜寻)。在实验方面，根据简化器的反响时间执行这些方法变得不实际，在深度4之后。在将来，这些方法对于电脑将变得是可实行的，虽然目前它不能。 一个使用有限制的证明搜寻的替代选择是为了解决从一个条件去确定一个可接受的条件类别，而且接受一些将会有可能是可证明的条件，但是它将会在外部被给的类别上失败。明显的选择是提议的逻辑。然

37、而，有条件的简单化的问题扩充多深入地超过偶然的失败证明一种提议有效的条件，如同我们稍后讨论一样，所以这方式不能产生任何很大实际的效益，虽然行为会至少在理论上有好的理解。被采用的 HOL ， HOL 启发和 Isabelle 的目前方式，是在条件上激发简单器它自己。这些递归的召集是潜在的非终止 (有条件的简单化极端地倾向于成环)，以至于被激发的递归简化器的时间是限制的。这些深度搜寻的限制当解决条件遭受同样的问题，这些问题在先前的段落被讨论过的。方式在许多方面比上面的很差，因为额外的简单化所有物有必要了解它的行为，当解决条件时，可能是不清晰的甚至在提议的条件上，让单独的情况来涉及述语。对于一个典型

38、的目标，我们只需要简单化能在一个简单了解的方法方面有进步。对于条件，我们的需求通常是体检可能的话，就被解决。简单化不是完全形式的证明，因此，我们希望，我们的情况将会是以致于那简单化能经常很好地运行。然而，简单化不能够证明所有的前置词条件以至于它的行为甚至在提议的水平是难了解的。在数量词推论上，甚至在最根本的水平，失败是基准。因此，当求证条件时，目前的方法无法足够地以非终止的问题处理。而且条件的级别可被简单化解决的很难去描述，而且不是简单的适合使用者去理解。完成完成是一个能确定简单组是聚合还是终止的程序。聚合与终止是我们要求简化组具备的两个主要所有物，所以完成是当采用简单化时一个有用的工具。我们

39、讨论我们的完成使用。在群的公理理论上使用完成的标准例子，源自一组终止和聚合的改写对于这一个理论构成一个标准的改写系统的规那么，展示了完成是有力的技术。在我们的工作中，这样的动力是从不被需要。我们实现了我们发现的非常有用的根本完成。因为我们的需要是被限制的，我们没有实现 Huet 的完全完成程序，虽然在不同的设定中这是令人想要的。我们放下这些是为了将来的工作。我们的完成程序也允许有条件的完成。当工作在一个键入设定的时候，时常希望在一个给定的类型中提及个体的一个子集。然后介绍一个述语的子类型，而且限制语句只谈论子类型的组成。动态的完成我们先前提到了它时常是一个希望以假定作为改写的例子。清楚地说，假

40、定是动态的并且在证明的程序中各处改变。虽然我们可能开始就错在改写的简单化规那么的组，如果我们使用假定，它可能很好的作为我们的根本简化组，增大假定，不再是聚合和终止。如果我们愿保存一个正在共同聚合和终止的简化组的所有形式，这时我们在证明的过程期间必须运行一些完成形式。我们需要这样的动态完成，因为它一定能在证明的过程期间被很好地运行。不幸地是，完成是一个相当昂贵的过程。而且，它大体上非终止的。然而，当看到各种规那么类型被使用的时候，典型地它们是一种非常简单的形式。举例来说，我们时常获得与假定类似的a = b a = c，然后着手进行一个可分的除去。 产生的目标有假定a = b 和 a = c，我们

41、愿作为简单化的规那么来使用它。多数的这些简单化规那么是根底的。在这情况下，完成被保证去结束，应该有一个方法发生短路的完成程序去得到一个能更快速地运行的相等程序。希望，如果我们能微小地减少完成的一条到另外一条规那么的改写，这时希望改写程序相对地充分运用( 当然地，这是伊莎贝尔空想的简单化的情形，而且 HOL 光简单化也在某些程度上是充分运用的) ，而且执行将会是可接受的。有一些文件覆盖了根本区间的完成。我们看 GNP +93。这一个运算法那么带来了一个根本的改写规那么组，而且在多项式产生一个减少的权威改写系统的时间。不幸地是，虽然过程在多项式时间里操作，但是它利用适宜的终止。适宜的终止在HOL启

42、发或Isabelle 中没有被执行，而且在及时上可能有一个没有充分运用的版本相对缓慢是多项式的(即，虽然来自 GNP+93 的运算法那么是多项式的在及时上，这里会有一个比例的高常数)。当然，在证明期间做一个增加的变化给等式组，因此，在这某种程度希望有一点提高，但是我们仍然应该有能够做更多的感觉。看一下我们使用作为改写的假定，它是清楚，超过根本的，他们甚至有比拟简单的自然：没有左手边的子区间被用于任何其他的改写规那么(比方，假定a = b，全然没有左手边的一个适当子区间，而且我们从没有另一项假定形式a = d同时发生的情况)。在这个例子中，它足够为了要维持聚合和终止，用这一条规那么改写所有其他的

43、简单化规那么。如果我们需要在线完成这些没有被满足的条件，我们会依靠我们的 (被限制的时间) 完成程序，但是在我们的个案研究中这不发生。当在根本完成的正确证明的上下文中考虑的时候，这一个结果是清晰的。然而，在我们的个案研究期间有假设干的复杂情节，没有这最正确化，导致我们的证明器花了特别久的时间。 方程式的统一我们的最高水平的证明搜寻基于列举区间上升到一个确定的区间深度。统一没有出现在一个这样的程序中。我们引用引进规那么 la Paulson进入我们的搜寻程序。现在由相配对的引进规那么对抗现在的目标规那么的结论被简单的完成。引进规那么像其他的辅助定理被对待，作为补充的假定它们合并的进入结果。不过，

44、他们作为引进规那么被作记号。我们用具体的例子说明它们的从区间的列举像其他辅助定理一样。结论通过简化器被改写。在证明搜寻的每个阶段，我们检查任何引进规那么的结论是否与目前的目标相配，而且如果因此我们以引进规那么的条件替换目标，返回不平安的引进规定，这有模拟等式统一的效果。5 连接与整合在这节中我们描述在早先的章节中被简述的技术如何整合进入一个单一战略，和在这一个战略和使用者之间的连接。我们的自动化包含一个描述的证明搜寻，藉由对固定的区间深度的数量词实例化，以要求散布到简单化。这些应该如何被整合? 如果简单化正在终止和聚集的，这时应用在证明搜寻的每个步骤后的简单化的明显策略保存完全。这是在这两项技

45、术整合后的必要观察。策略提供了一个连接给使用者。使用过程中使用者必须表达一组终止和聚集的改写规那么和一组引进规那么的过程。事实上，使用者也表达一组应该在证明期间被考虑的辅助定理，而且这些只是被当作先前描述与目标陈述的合并。证明搜寻地进行，与平安的规那么和简单化热心地应用，以及在不平安规那么上的返回。如果证明是不成功的，失败局部被返回给使用者几乎没有平安规那么，或简单化的步骤，可能被应用。对我们的方式一个缺点是结果相当大，因为我们正在特定的深度下面用所有的(类型-正确的) 区间例示数量词。它将有一点适应使用者的连接，以使这些实例化不直接地呈现给使用者，但是在要求上可视的。我们离开这更进一步工作。

46、6 评估在这节中，我们讨论我们的证明的过程怎样相当于根据在第2节中被简述的标准。我们然后讨论完全的议题。我们没有宣称有一个正式的证明对完全产生一些问题的类别，但是我们确实讨论过程有好的所有物。我们通过设置我们的技术产生其他的就像分析一样的理论证明技术。然后我们通过给出的成功例子评估实际的过程使用，而且描述过程的感觉。6.1评估生产需求我们的程序与在第2节提到的标准一起被设计。我们感到它满足简单化的需求。在概念上，我们正在执行一个标准直观的证明搜寻。我们合并平安的和不平安的规那么。我们在逻辑的水平(布尔类型)和领域的特性类型里使用简单化。我们的简单化规那么应该是聚集和终止的。当改写不破坏重要的所

47、有物时候，我们确信任何的假定都可以使用。我们只有在限制的它们有很好的行为的例子中使用简单 化以及有条件的简单化规那么。所有的这些观念很容易理解的。当使用程序的时候，概念上的简单化导致简单化。我们应当确定我们的简化组，我们的引进规那么组，以及与目标相关的辅助定理。策略在策略水平运行，因此，我们能通过激发一次一步的策略步进经过一个失败的证明尝试。既然程序是非破坏力的( 在某种意义上我们直接地搜寻使用自然减除的规那么，并非对正常的形式转换)，我们有高水平的可视化进入证明的搜寻。失败局部典型地立刻被理解。平安步骤的观念意谓，即使我们无法找到证明，我们回到使用者执行得相当多的我们取得进步的工作。不完全显示