资源描述
编号： 毕业设计英文翻译译文 题 目: Automation 院 系： 计算机系 专 业： 自动化 学生姓名： 学 号： 指导教师： 职 称： 2005 年 6 月 3日自动化汤姆里治2005 年四月 12 日目 录1 介绍 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 2 需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 3 目前交互式证明器的自动化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4 4 技术. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.1 证明的搜寻. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 逻辑系统. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6引进规那么. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.2 等式. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 改写. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 条件的简单化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 动态的完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 方程式的统一. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .125 连接与整合. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 6 评估. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 6.1 评估生产需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .136.2 完整性. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 6.3 效率. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 6.4 实际应用. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7 替代选择. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 8 结论. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19 1 介绍自动化可能是成功的机械化的关键。在一些情形中，机械化不需要自动化就可以实行。确实，在高度抽象的数学区域，大局部由使用者拼出的复杂证明组成的机械化推论远远超过了那些目前能被自动化解决的范围。在这一背景下，如果自动化它被全部使用， 将指导在容易的可以解决的被紧紧地限定的次问题上。一个机械化的典型例子是我们的拉姆齐定理的形式化。另一方面，在推论相对被限制的地方，自动化能富有成效地在确认类型的证明中被应用，但是绝对程度的细节将使一个非自动化的机械化不可实行。许多人已经花费了数年来开展全自动系统。比方Vampire VR 和otter McC全自动系统。我们可以和这样的系统竞争的设想是愚蠢的。它们的执行是一种方式，这种方式超过目前在交互式定理证明器被实行的系统。这些方案正在进行是为了把这些系统和交互式定理证明器相连。这是极其有价值的工作：如果知道一个一阶的陈述是可证明的，这时应该期待机器能提供一个证明。在这一节中，我们简略说明一些我们已经在各种不同的情况应用研究的技术。自然地我们不企图仅此一次去解决自动化推论的问题。宁可我们把重心集中在问题，而这些问题典型地出现在我们已经涉及的研究。我们首先简略说明我们需要的自动化的引擎功能。我们然后描述我们应用的技术，而且他们是如何整合的。我们评估根据我们的需求性质上地产生的引擎，和数量地有关于一件相当大的案例研究。这些技术中的少数是新奇的，宁可，我们企图用一种适宜的方式来融合现行的技术。这些步骤在HOL启发定理证明器被开展，这是我们建立的设计原型的一辆优良车辆的不同方法。2 需求我们的自动化的需求是什么? 让我们区别一下自动化和全自动化的使用，以及交互式自动化的使用，每一种的需求都有非常地不同。也许料想不到地，失败的自动化证明引擎是基准，是观念，这观念是当交互式开展的复杂证明使我们花费大多数时间对 几乎 的可证明的义务的时候。因此我们想要证明器给我们完美的反响作为为什么任务不能够被执行的原因。这引证强调一种在自动化和交互式证明之间的重要的不同。在自动校对中，可典型地知道，目标是可证明的 ( 或至少，非常强烈地疑心，而且在结束相当多量的时间之前准备等候证明的搜寻)。确实，自动证明器被判断在他们能实际上证明多少可证明的目标之上。在交互式证明中， 我们花费我们大多数的时间在几乎可证明的义务上。这是交互式和证明之间的不同。如果我们花费大部份的时间尝试去证明简单但不可证实的目标，然后校正的搜寻完全变成比拟不重要。这虽不能说是它全部失去重要:：如果一个系统缺乏完整性，这时它将会无法证明一些可证明的目标。什么类型的目标正在被放弃，这是非常必要而且主要去知道的，这是为了知道当一个证明器失败于证明一个目标时就能理解它是什么意思。这些知识也非常有用，当混合系统为了了解作为整个系统的行为，应当首先了解局部的行为。在一个交互式的环境中，在完全之上所有物可能被偏爱，就我们而言，自动化的最重要方面是简单化。 而这些我们不是意味着去落实简单 ( 要布多少根线来实现系统? 等等)，而是概念上的简单化。例如，简单化到处被用于交互式定理求证。如果一组改写规那么不能融合，这时去了解简化器的行为，必须了解适用的规那么顺序。不用说，对于理解这是一件极端复杂的事情，而且属于这些所有物的证明在推测上极端易碎。概念上的简单化通过聚集和简易装置的终端对一个简化器进行紧密地约束。如果一个使用者要了解系统，概念上的简单化很重要。如果一个系统的概念简单，它将会很有希望被简单的使用。在一个交互式环境中，我们期待自动化失败。为了取得进步，我们必须了解一种证明的尝试为什么失败，证明器一定会提供反响。基于系统的决议能提供反响，但是他们是消灭性的 (在某种意义上目标转换成一种正常的形式在证明的尝试之前开始，破坏了最初的逻辑结构)，所以反响很难被了解 (论证失败的点对于最初的目标能看出明显的不同)。较好的方式是引导在一个尽可能接近的方法证明到一个人类可能如何引导证明。在一些感觉中我们需要证明的系统应该是自然的。在这情况下，如果一种证明的尝试失败，失败的局部能时常被作为检验直接地返回给使用者。反响与能见度相关。时常一个使用者希望检查失败的证明，但是只有证明的踪迹是可得的，它能引起一个概念上的错误结合: 使用者把重心集中在结果，然而踪迹可能全部是有不同的自然。如果有许多没有被证明的局部，这时一个使用者不可能检查它们的全部，但是可能愿意沿着证明走。像约翰 哈里森的模式消除的执行的自动化方法，时常利用全球化的节点优先寻址的信息在一棵树里搜寻一个证明。如果全球化的信息不是出现在结果中使用者有时机接近，它将会难以经过通过简单运用的自动证明器一步一次的自动化证明。当传导的搜寻正在使用全球化的信息时，自动证明器将不做出它做出的相同决定，因为它只能进入本地的结果。许多方法现在被交互式定理证明器所使用，就像伊莎贝尔的blast，留下未改变的目标如果它们失败于证明这目标的话。证明搜寻的自然方法期待在所有的情形中至少能做出一些进步，所以即使目标不是可证明的，它们也能够有所帮助。 比方，平安的步骤 (就像在许多系统的E) 应该被实行，简单化步骤被应用等等。自动化也应该是稳定的。在大量的证明中，一个证明时常混合交互式和自动的证明。如果被自动化返回的目标容易根本地以目标的微小变化改变，这时关联的交互式证明将被毫无用处的给予，而且一定被改写。因为这一个理由，被自动化返回的不能解决的次目标应该在对于最初的目标的微小改变下稳定。如果一个证明能被建立，然后一开始把重心集中在使证明更加可维持的方面，就像鲁棒一样。效率是在蛋糕上的糖衣。完全也是重要的，虽然没有必要在一阶逻辑完全，但是宁可应该有一个给定的程序解决的层次问题一个清楚的观念。无论如何，一些系统的行为理论上理解是重要的，如果它接近简单的目标。让我们总结出这些观点： 自动化应该很简单：它应该在理论上很好地被了解，和在使用中可预期的。 自动化也应该提供反响，以至于使用者能估定一种证明的尝试为什么失败。 一个甚至比拟强烈的需求是，自动化是可视的，在可视中通过证明的研究，能直接地检查自动化的执行。 自动化应该是自然的，这是为了使证明器和使用者之间的概念差距最小化。举例来说，自动化应该在标准的逻辑系统中执行，或者与使用者传导证明的决策程度相一致。 时常，使用者对一个证明进行优化有很多的平安步骤。与自动化在返回前至少做出改良相比，自动化简单的返回“可证明与“不可证明是没什么用处的。 自动化应该是稳定的，以至于在自动化的行为中理论上微小的改变不会产生大的变化。这是很重要的，因为交互式的证明包含大量隔行扫描使用者或自动化步骤的环节。 自动化也应该是鲁棒的，在意义上微小的变化不会影响自动化的可证实性。 我们想要自动化对明显的理论是有效率的。 最后，我们想要自动化是完全精密的。她能很好的定义问题的层次。3 目前交互式证明器的自动化目前交互式定理证明器的自动化证明方法不符合先前环节的需求。Isabelle/ HOL是目前作为被认可的HOL执行的代表。 主要被使用的技术是一个描述的证明器blast，和简化器simp。这些都混合在单个的自动化策略里。 Isabelle也包括一个模式消除程序，它和blast使用起来有点相似。Simp 被广泛地使用，但是它并不是一个完全的一阶证明方法。然而，它能满足许多前期环节需求的事实解释了为什么它这么流行，在交互式证明中。blast方法在肯定逻辑和组的简单问题上运行得很好，但是它很难了解它的特性是什么。它基于一个证明器leanTAP，那对一阶逻辑是完全的。另一方面，以下的目标稍微可证明在一阶逻辑，但是blast不行。f( g a)=a y g(f y)=y它甚至更加的混乱，但它在区间 g a 实现的时候，这区间在结果本身中发生，并是存在的证明。更糟的是，当像HOL 的类型逻辑被表达的时候，g a 是唯一的区间发生在可以使用的正确类型结果中。这一个失败对于有效地处理等式逻辑是一个描述类型程序失败的合并统一。因为它是这么的不受限制，所以自动方法几乎从不被用于交互式证明的中间。而且，它是不稳定的，在它产生的子目标中在对目标的较小变化之下可能是野性地不同的，它的提出是无用的除了在紧紧地被控领域。整合一个现代的解决证明器Vampire进入Isabelle将没有必要纠正这些错误。基于解决的方式提供了一点支持对于交互式理论证明器，因为子句形式的减少意味着使用者有很少的可观性进入证明的搜寻，而且很少知道为什么一个特殊的辅助定理会失效。证明的搜寻是一个本地的向前的综合的搜寻，与一个全球化的向后的综合搜寻的典型描述介绍以及Isabelle的策略水平相反。因此，对于使用者，解决是一个不自然的系统。通常从这些系统来的反响是极差的甚至不存在的。此外，许多步骤应该被认为是平安的 (应用一个终端和聚合的改写组，运行一个 E 步骤) 因为系统被当作一个黑盒子使用，或目标率直地被解决，或者更通常，一点也不解决，而且系统包含的关于可靠应用的步骤被丧失的信息，留给使用者可以手动的应用这些步骤。这里的问题是系统无法做出改良那些无法直接证明的目标。我们也作关于一阶理论证明器的以下观察。这些证明器被设计去寻找大量的数量词实例，寻找可选择地系数平等推论。然而在交互式定理证明器里的自动化的失败没有失败于猜想大量的数量词实例。4 技术在下面这节，我们描述我们如何建立自动化。首先，我们正在尝试寻找证明，所以我们将会需要 ( 至少) 证明的搜寻引擎。然后，我们在很大的程度上愿做用手动的方式的模型证明。除了证明的搜寻之外，在手动证明中其他主要的利用方法是简单化。我们描述我们怎样讨论简化器。有条件的简单化是一种简单化的形式，它的简化器采用递归的方式企图解决可能被应用的当前目标的改写选择。我们讨论正采用在这些目标上的简化器没有被最好的运行，并建议替代选择。然后，当使用简单化的时候，它是一个很好的方法去确定简单装置是集合的和终端的。我们描述完成的执行。当使用简单化的时候，然而，也想利用在改写一个证明的过程中产生的假设。确定改写规那么的组仍然是聚合的和终止的，就应该在证明搜寻时提供一些动态完成的形式。我们讨论我们如何抓住了这些议题。4.1证明的搜寻在这节中，我们描述我们证明搜寻的根本系统。这是一个单一的结论，对向后的证明搜寻是适当的直观系统。我们避开统一的流行的区间计算。这有一些有趣的结果当混合证明搜寻时用其他的方法。注意我们只对自动化的一阶系统感兴趣。逻辑系统证明搜寻的二个主要系统是决议和描述。因为一个交互式环境的自动化，决议太不自然。因为这一原因，描述是更有希望的。我们因此限制我们的注意在基于描述的系统。描述系统典型地藉由否认目标而且寻找矛盾着手进行。我们甚至考虑到这是不自然的。我们因此集中在标准逻辑系统中直接执行的描述系统。使用这样一个系统根据复杂的执行有重要的意义，因为我们能只是简单地在 HOL 目标的水平搜寻使用或多或少标准的策略。这也对自然化有有利条件，因为使用者已经熟悉一个如此系统的证明和反响，因此我们能直接地对使用者呈现失败的局部，这些使用者没有翻译出来自一些其它可能的证明系统的结果。单一结论系统对古典的证明是不适宜的，古典的证明被多样结论系统更好的支援。然而多样的结论系统是不自然的。如果我们对古典的证明感兴趣，我们一定成认我们的单一结论系统有缺点。另一方面，我们相信大规模的证明结构大概是直观的：我们典型地集中于一个目标，并且我们的辅助定理效劳作为证明中的中间观点，和我们的补助定理如证明的中间点效劳，即AB C作为一个补助定理对 (A B ) C不是典型地相等，因此我们期待在证明中到达一个点，这里A B 是可证明的，而不是去做一个可分的拆开。确定地对于我们感兴趣的领域，所有的证明本质上是直观的，以及古典的推论被限制到可能被简单化或其他的限制技术处理的小区域。引进规那么我们希望做出更多的进步。虽然程序简述说明上方是完全的，它宁可是一边的。既然大多数的证明大量利用辅助定理，对应的目标传输容易变成相当拥挤。而且，当引进规定的时候，许多辅助定理自然地被浏览，也就是说，趋于使用精炼的结论 C 而不愿使用从开始向前连接着的结论。因为这些理由，我们也利用引进规那么 la PaulsonPNW03。这些典型不平安，但是如果我们再一次返回，而且轮流其他的防范，完全性就能被保存。这些引进规那么能像辅助定理一样被执行，但是被作记号作为引进规那么。在证明的搜寻时候，这些辅助定理的结论被相配对抗当前的目标。如果结论与当前的目标相配，那么目标将被选择的引进规那么所代替，而且在事件中这些假定不能够被证明，那么返回将被采用。如果一条引进规那么标明是平安的，这时返回不发生。注意，这些提高没有必要来自理论的观点，而且它的唯一动机是做模型自然形式的证明。如果完全性以特定的方式被考虑，这时候能够看见完全性的保存。如果这些规那么是行为表现所预期的，那么在简单化之前需要等式的统一。然而，目前我们用手动的方式来模拟等式统一的使用。完全性失败对于引用规那么：如果我们以一条规那么作为一条引进规那么，这时我们无法是完全的? 不过这不是真实的，而且规那么是平安的，在哪一情况我们都很顺利，或不平安的，在哪一情况我们返回。需求的统一意味着我们能防止我们能防止作为增加的假设而使用的规那么。然而，如果在一些阶段我们能以规那么作为一条引进规那么，这里有一个引进规那么被打算使用的环境，但是没有连接链，然而当一项额外的假定可能有时这里将没有统一的问题。而且，自从我们没有使用一个作为标准的辅助定理的规那么，使用完全化的概念将不是很清楚。让我们定义完全化的生产一个引进规那么去了解是否有一个证明作为一个辅助定理的规那么。这时一个使用规那么的证明作为一条引进规那么。在平等面前，我们应该因此使用统一去确定我们的引进规那么能被无论在那里都可能应用。既然在每个阶段我们有一个有限的场地区间组，与一个终端和集合的改写次序，这样一个方法能够可以实行，即使在现阶段我们只能用人工模拟这样的步骤。引进规那么的使用会带来复杂化，因为完全化是否适合不清楚。如果引进规那么能作为一个正常的辅助定理使用，这时完全化是可以保存的，因此辅助定理被操作就像它是个正常的肯定逻辑。在一条引进规那么后面的方案是去平衡证明的搜寻，这会以别的方式主要地在左边上操作。在规那么 A B作为几个辅助定理和作为一个引进规那么之间的差异，是自动化能应用 L与一个作为辅助定理的规那么相结合。因此作为一个引进规那么，我们期望目标最终成为B和它能用A代替这些。4.2 等式改写改写是由用相等的子术语更换一个术语的变换过程。例如，我们可能使用辅助定理f (a) = a去改写Q f (f (a) 到 Q f (a)然后到Q (a)。在这节中，我们的各种改写概念是非正式的。对于更多的信息读者可以请教优秀者。在用辞上的一个注解：一个简单化的次序是一个改写被限制的次序，过去一直用来证明一个区间改写系统的终止。然而，“简单化这个词时常被非正式地用于提到改写，而且“ 简化组这个词时常用来提及改写的系统规那么。我们下面采用这些非正式的用法。两个主要的简单化财富是终止和聚集。没有聚集，了解简化器的行为就必须知道改写被应用的次序。这太多而不是使用者所期待的。在一个交互式环境中终止非常有用，例如，它允许反响。而且，终止允许简单化与主要的证明的搜寻相整合。如果我们有聚集和终端，这时每一个区间有一个独特正式形式，而且尝试的等式变得可决定。这是一个极其有用的简化组的财富。我们的根本策略是热心地应用简单化，在证明的搜寻每个步骤之后，使用假定去简化其他的假定和结论。我们用一个有终止和聚集的简化器工作。我们检查终止和聚集的手动使用完成。我们在个体的类型中应用简单化。如果简化组正在终止和聚合，这时它保存了证明搜寻的完全性。我们也在布尔类型应用简单化，但它不是一阶逻辑的一种可能性。例如，我们采用高阶对微小范围的数量词改写。不是太困难而无法争论而这也保存证明的搜寻完全。经常相似改写的假定在证明期间出现，而且这些可能被简化组合并。给一项假定x.P x和假定 P t，就可以简化 P t=，是再一次在布尔类型的简化，而不是一阶的操作。我们不以这一种形式的假定作为改写：我们的对数量词例如的根本途径经由区间计算，而且使用这些简单化会破坏这方式的完全。我们使用假定形式x= y(可能数量化)来改写。 为了保有聚集和终止，我们完成简化组的生产并动态的产生改写。因为完成没被保证结束，完成被限制到一个步骤确实定数字，虽然在我们的应用中，完成总是成功。条件的简单化在这节中，我们描述有条件的简单化，并且注意到标准的途径去解决递归环境下简化器的实施可能没有被期待。我们建议一些其他的方法，而且讨论其他的有条件的简单化的问题。我们得出结论，目前有条件的简单化太复杂而无法作为 简单的 技术计算，并且确实太复杂而无法以一合理的方式与证明的搜寻相连接。我们建议考虑有条件的改写就如平常的辅助定理的一样的替代选择。简单化的工作在于对形式a = b的改写，在目标的任何地方改写a到 b。有条件的简单化的工作在于对有条件的形式Aa = bA是一典型的连接的改写。在一个依次的 C 中，如果我们能证明C, 的话，我们就能在目标里调整a到b的改写。我们应该如何尝试去证明条件A? 假设我们正在用简单化连接一个完全的证明搜寻系统。在这情况下，非常好的 (从一个理论上的立场) 行为会被由需求获得，如果A是可证明的，那么它实际上是被证明的。因为对A的证明的搜寻是潜在的没有终止的，我们这时应该妥善地安排一个复杂的隔行扫描主要证明搜寻的过程，与子证明搜寻企图去解决有条件的改写情况。一个如此方式是不适口的不只因为效率的原因。简单化的好处之一是，不像证明的搜寻，它正在终止。如果当采用有条件的简单化的时候，我们希望保存这一终止的行为，当企图证明条件的时候，我们应该遵行被涉及的非终止。一个我们应该采用的主要证明搜寻是去证明条件，但是限制对特别深度的搜寻。这也是不适口的。为了在一个合理的时间里保持简单化的运行，这深度应当非常小，因为条件的产生是很频繁的。这些小的深度不能提供更多的条件解决方法比其他简单的方法。对于一个小深度的有限制的证明搜寻，这也意味着它的理论限制也能成为实际的限制：任何的有限制的证明搜寻将会是不完全的，但是由于大的深度我们可以有希望的忽略这样的不完全。小的深度意味着我们可能面临的条件能被解决的条件，这条件对于使用者是很清晰的，不过被限制的搜寻深度意味着情况没有被解决。根据我们的经验，深度必须至少有10个逻辑的步骤 ( E 及其他。)，连接中间有效的等式推论(我们想像一个情节我们有一个有效地处理等式的证明搜寻)。在实验方面，根据简化器的反响时间执行这些方法变得不实际，在深度4之后。在将来，这些方法对于电脑将变得是可实行的，虽然目前它不能。 一个使用有限制的证明搜寻的替代选择是为了解决从一个条件去确定一个可接受的条件类别，而且接受一些将会有可能是可证明的条件，但是它将会在外部被给的类别上失败。明显的选择是提议的逻辑。然而，有条件的简单化的问题扩充多深入地超过偶然的失败证明一种提议有效的条件，如同我们稍后讨论一样，所以这方式不能产生任何很大实际的效益，虽然行为会至少在理论上有好的理解。被采用的 HOL ， HOL 启发和 Isabelle 的目前方式，是在条件上激发简单器它自己。这些递归的召集是潜在的非终止 (有条件的简单化极端地倾向于成环)，以至于被激发的递归简化器的时间是限制的。这些深度搜寻的限制当解决条件遭受同样的问题，这些问题在先前的段落被讨论过的。方式在许多方面比上面的很差，因为额外的简单化所有物有必要了解它的行为，当解决条件时，可能是不清晰的甚至在提议的条件上，让单独的情况来涉及述语。对于一个典型的目标，我们只需要简单化能在一个简单了解的方法方面有进步。对于条件，我们的需求通常是体检可能的话，就被解决。简单化不是完全形式的证明，因此，我们希望，我们的情况将会是以致于那简单化能经常很好地运行。然而，简单化不能够证明所有的前置词条件以至于它的行为甚至在提议的水平是难了解的。在数量词推论上，甚至在最根本的水平，失败是基准。因此，当求证条件时，目前的方法无法足够地以非终止的问题处理。而且条件的级别可被简单化解决的很难去描述，而且不是简单的适合使用者去理解。完成完成是一个能确定简单组是聚合还是终止的程序。聚合与终止是我们要求简化组具备的两个主要所有物，所以完成是当采用简单化时一个有用的工具。我们讨论我们的完成使用。在群的公理理论上使用完成的标准例子，源自一组终止和聚合的改写对于这一个理论构成一个标准的改写系统的规那么，展示了完成是有力的技术。在我们的工作中，这样的动力是从不被需要。我们实现了我们发现的非常有用的根本完成。因为我们的需要是被限制的，我们没有实现 Huet 的完全完成程序，虽然在不同的设定中这是令人想要的。我们放下这些是为了将来的工作。我们的完成程序也允许有条件的完成。当工作在一个键入设定的时候，时常希望在一个给定的类型中提及个体的一个子集。然后介绍一个述语的子类型，而且限制语句只谈论子类型的组成。动态的完成我们先前提到了它时常是一个希望以假定作为改写的例子。清楚地说，假定是动态的并且在证明的程序中各处改变。虽然我们可能开始就错在改写的简单化规那么的组，如果我们使用假定，它可能很好的作为我们的根本简化组，增大假定，不再是聚合和终止。如果我们愿保存一个正在共同聚合和终止的简化组的所有形式，这时我们在证明的过程期间必须运行一些完成形式。我们需要这样的动态完成，因为它一定能在证明的过程期间被很好地运行。不幸地是，完成是一个相当昂贵的过程。而且，它大体上非终止的。然而，当看到各种规那么类型被使用的时候，典型地它们是一种非常简单的形式。举例来说，我们时常获得与假定类似的a = b a = c，然后着手进行一个可分的除去。 产生的目标有假定a = b 和 a = c，我们愿作为简单化的规那么来使用它。多数的这些简单化规那么是根底的。在这情况下，完成被保证去结束，应该有一个方法发生短路的完成程序去得到一个能更快速地运行的相等程序。希望，如果我们能微小地减少完成的一条到另外一条规那么的改写，这时希望改写程序相对地充分运用( 当然地，这是伊莎贝尔空想的简单化的情形，而且 HOL 光简单化也在某些程度上是充分运用的) ，而且执行将会是可接受的。有一些文件覆盖了根本区间的完成。我们看 GNP +93。这一个运算法那么带来了一个根本的改写规那么组，而且在多项式产生一个减少的权威改写系统的时间。不幸地是，虽然过程在多项式时间里操作，但是它利用适宜的终止。适宜的终止在HOL启发或Isabelle 中没有被执行，而且在及时上可能有一个没有充分运用的版本相对缓慢是多项式的(即，虽然来自 GNP+93 的运算法那么是多项式的在及时上，这里会有一个比例的高常数)。当然，在证明期间做一个增加的变化给等式组，因此，在这某种程度希望有一点提高，但是我们仍然应该有能够做更多的感觉。看一下我们使用作为改写的假定，它是清楚，超过根本的，他们甚至有比拟简单的自然：没有左手边的子区间被用于任何其他的改写规那么(比方，假定a = b，全然没有左手边的一个适当子区间，而且我们从没有另一项假定形式a = d同时发生的情况)。在这个例子中，它足够为了要维持聚合和终止，用这一条规那么改写所有其他的简单化规那么。如果我们需要在线完成这些没有被满足的条件，我们会依靠我们的 (被限制的时间) 完成程序，但是在我们的个案研究中这不发生。当在根本完成的正确证明的上下文中考虑的时候，这一个结果是清晰的。然而，在我们的个案研究期间有假设干的复杂情节，没有这最正确化，导致我们的证明器花了特别久的时间。 方程式的统一我们的最高水平的证明搜寻基于列举区间上升到一个确定的区间深度。统一没有出现在一个这样的程序中。我们引用引进规那么 la Paulson进入我们的搜寻程序。现在由相配对的引进规那么对抗现在的目标规那么的结论被简单的完成。引进规那么像其他的辅助定理被对待，作为补充的假定它们合并的进入结果。不过，他们作为引进规那么被作记号。我们用具体的例子说明它们的从区间的列举像其他辅助定理一样。结论通过简化器被改写。在证明搜寻的每个阶段，我们检查任何引进规那么的结论是否与目前的目标相配，而且如果因此我们以引进规那么的条件替换目标，返回不平安的引进规定，这有模拟等式统一的效果。5 连接与整合在这节中我们描述在早先的章节中被简述的技术如何整合进入一个单一战略，和在这一个战略和使用者之间的连接。我们的自动化包含一个描述的证明搜寻，藉由对固定的区间深度的数量词实例化，以要求散布到简单化。这些应该如何被整合? 如果简单化正在终止和聚集的，这时应用在证明搜寻的每个步骤后的简单化的明显策略保存完全。这是在这两项技术整合后的必要观察。策略提供了一个连接给使用者。使用过程中使用者必须表达一组终止和聚集的改写规那么和一组引进规那么的过程。事实上，使用者也表达一组应该在证明期间被考虑的辅助定理，而且这些只是被当作先前描述与目标陈述的合并。证明搜寻地进行，与平安的规那么和简单化热心地应用，以及在不平安规那么上的返回。如果证明是不成功的，失败局部被返回给使用者几乎没有平安规那么，或简单化的步骤，可能被应用。对我们的方式一个缺点是结果相当大，因为我们正在特定的深度下面用所有的(类型-正确的) 区间例示数量词。它将有一点适应使用者的连接，以使这些实例化不直接地呈现给使用者，但是在要求上可视的。我们离开这更进一步工作。6 评估在这节中，我们讨论我们的证明的过程怎样相当于根据在第2节中被简述的标准。我们然后讨论完全的议题。我们没有宣称有一个正式的证明对完全产生一些问题的类别，但是我们确实讨论过程有好的所有物。我们通过设置我们的技术产生其他的就像分析一样的理论证明技术。然后我们通过给出的成功例子评估实际的过程使用，而且描述过程的感觉。6.1评估生产需求我们的程序与在第2节提到的标准一起被设计。我们感到它满足简单化的需求。在概念上，我们正在执行一个标准直观的证明搜寻。我们合并平安的和不平安的规那么。我们在逻辑的水平(布尔类型)和领域的特性类型里使用简单化。我们的简单化规那么应该是聚集和终止的。当改写不破坏重要的所有物时候，我们确信任何的假定都可以使用。我们只有在限制的它们有很好的行为的例子中使用简单 化以及有条件的简单化规那么。所有的这些观念很容易理解的。当使用程序的时候，概念上的简单化导致简单化。我们应当确定我们的简化组，我们的引进规那么组，以及与目标相关的辅助定理。策略在策略水平运行，因此，我们能通过激发一次一步的策略步进经过一个失败的证明尝试。既然程序是非破坏力的( 在某种意义上我们直接地搜寻使用自然减除的规那么，并非对正常的形式转换)，我们有高水平的可视化进入证明的搜寻。失败局部典型地立刻被理解。平安步骤的观念意谓，即使我们无法找到证明，我们回到使用者执行得相当多的我们取得进步的工作。不完全显示它本身作为一个失败去猜想大量的数量词实例。随着动态完成的失败，不完全也能在证明搜寻期间产生。 简单化导致了稳定性。当在它已经成功之前，我们会称的证明器是单调的，在那增加的辅助定理中，简单化的规那么，或不平安的规那么不会导致程序的失败。同样地证明器是鲁棒的，即使对定义有微小的变化等等。我们不会宣称程序是有效率的。6.2完全我们自动化有一些不完全的来源。FOL 的可证明性大体上是无法决定的。我们对区间集合的子集深度限制。是否有一个证明仅仅涉及到深度限制区间是现在可决定的，但是我们将会不可防止地失败于找到我们的限制子集之外包括区间放置的证明。这是一个不完全的来源。然而，我们可能连续地增加区间深度并且这样来恢复对可决定性花费的完全。FOL 能在方程序的推论 McK75 中置入，所以期待等式推论说明对通常证明搜寻的类似问题。我们的方式是限制我们自己对终止和聚集的改写规那么组。因此完成可能失败，或不可能结束，这是一个不完全的来源。而且，我们采用动态的完成，能同样地失败，虽然在实践中这不是一个问题。然而，完成能让使用者大量的进行交互式处理。如果使用者确定，改写规那么组是聚集和终止的，而且如果动态的完成在证明搜寻期间总是成功的，这时我们的等式操作将会是完整的。6.3 效率目前自动化方法的成功很大停留在统一上，然而我们只有稍微地使用统一，当操作引进规那么时。根据证明的搜寻，根据执行我们的程序将会广泛类似像吉尔曼这样的前统一程序。举例来说，以下的目标是可决定的：(xyz.P x y P y z P x z) (xyz.Q x y Q y z Q x z) (xy.P x yP y x) (xy.P x y Q x y) (xy.P x y) (xy.Q x y)确实，事实或一个公式的虚伪能在一个只有四种要素的模型中被评估。然而，即使这样一个的目标是可决定的，甚至于一些现代解决方法基于证明器的努力。不幸的是，我们的程序注定要花非常长的时间。在防御中，这样的目标很少在交互式定理的证明中被碰到。如果他们被遇见，使用者当然可以用一个交互式的决议证明器去解决他们。除了根本的证明搜寻之外，我们对等式推论给予特别的关注。我们在完成上对等式结束的方式，和在各种可变的条件是满足的。然而，如果保持这些情况，达成平等的方式或许是有效的。现代的决议证明器采用无穷尽的完成，推测的行为将不再比完成一个完全存在的改写组有效率。6.4实际应用因为它概念简单，证明器是非常容易使用的。从一个定理到下一个定理的典型移动，激发证明器关于简化组和预先辅助定理组的使用。如果证明没有被建立，我们会见到失败局部。这个局部通常是很容易理解的。几乎总是(在我们的个案研究中，总是)需要增加一个简化规那么，或一个不是不重要的辅助定理。如果辅助定理没有已经被证明就应该取出并证明它。增加必要的规那么，程序被重复执行，通常是成功的。大体上说，我们没有修整简单化规那么和辅助定理组到每个定理：这些规那么被利用取决与上下文的内容，而且总是一个良好的主意去使用它们如果可以的话。相对于这些，太多的规那么能导致执行能力的降低，但是通常它正工作在一个给定的理论中，这里辅助定理的数量相对地被限制。有时候必须用一个巧妙的区间例示一个数量词，但是这些是自然的困难的步骤。在使用者的手段(并非检查一些失败的局部的表现)下步进的经过证明的能力是非常有用的，而且提供很好的可视化，如果一些东西没有正确工作的话。我们讨论完全不是首要重要的，但是清楚地自动化的目标是协助使用者证明辅助定理。如果自动化能直接证明辅助定理，我们将没有抱怨的了。在我们的个案研究中我们执行许多证明。一个主要的结果包含超过250条交互式证明的手写体。这些证明的手写体不是最初的证明抄写，所以自动化可以可实现的再造它们。我们的自动化能够解决每一个辅助定理。 我们提供针对证明的一个区段的统计，它涉及辅助定理 theorem_3_ nes_Mup，对于其他辅助定理是代表性的。这些辅助定理依次有一个次补助定理theorem_3_Mup _3。在下面的列表中，我们记录定理名称，策略手写体的组成没有我们的自动化，组成有我们的自动化和花费的时间。当求证 theorem_3_nes_Mup时，次辅助定理 theorem_3_nes_Mup_3 被提供应自动化。当这个次辅助定理被省略，而且主要的辅助定理不需要theorem_3_nes_Mup协助的时候，我们也记录发生的东西。这涉及了证明器在主要的辅助定理的证明期间的再次证明。在这情况下，一个证明被建立，虽然它需要花超过5 分钟的时间。然而，我们相信，这是由于自动化策略的无效率实行，而且我们想要在将来的工作中再实现它。这些补助定理对自动化对个案研究的其他辅助定理的效果是有代表性的。而且，我们已经在其他的领域中相对成功的应用了这样的技术。即使执行很差劲，调和这些证明程序以至于辅助定理能被证明是一个主要的完成。事实上我们可以用一个常用的方法提供程序有很好的理论所有的证据。 定理名称 策略行 自动操作的策略行 自动操作的时间/秒theorem3_ nes_Mup _3 28 1 66theorem3_ nes_ Mup 12 1 24theorem3_ nes_Mup n/a 1 3057 替代选择我们开展的自动化被我们在案例研究中遇见的问题所激发。然而，我们总是能够完成我们的简化组的事实应该是一件幸运的事情。大体上我们能期待完成举例失败对于表达交换性的规那么来说，所以测试两个区间经过一个权威的改写组的等式。这里有一些处理问题的环境的方法，比方顺序改写交互式的规那么的例子，但是我们想要这个时机考虑替代选择一般的对等式处理的途径。到现在为止，我们的证明搜寻限制了被考虑的区间深度。看起来似乎限制等式推论到一个共同的区间子集是很合理的，而且在这里面采用适合终止限制的子集。这些介绍是过程的不完全。求证 s= t 使用等式需要的公理，大体上，是任意很大深度的区间。如果我们限制我们考虑的区间深度，我们的等式推论将会是不完全的。举例来说，假设我们通过转移链s = u = v = x = y=t来证明一个等式s = t。这样的一个证明被展示在图1。如果我们限制我们考虑到 d 或更小的区间深度，图可能与图2相似。 在这个情况下，等式s= u= v 将会被获得，但是等式x= y 和 y= t 将不会被获得。 如果没有 s= t 的证明存在与被限制的共同区间里，我们将会无法推论得到s=t。因此在任何给出的我们证明搜寻的阶段，我们的等式推论将会是不完全的。然而，如果我们连续地增加我们考虑的区间深度，我们将重新获得等式推论的完全性。在这一环境下，方程式的统一，生产被限制的区间组，变成可决定的，而且能非常有效率地实现。这个方式的另一个优点是给同等级别的代表能在一个使用者特别的习惯下被选择。举例来说，使用者可能选择同等类型的子句作为代表，或最小的产生一些词典的路径命令。这对使结果保持易读有帮助。这方式的另一个优点是使用者的理解是简单的，而且我们在证明搜寻的方法密合得很好。聚焦在单个复杂性上的衡量，比方区间深度，在一些程序之上，是一个统一的步骤。而且，缺点和方式的不完全经由完成在这里是不存在的。我们留下这些替代选择的执行给将来的工作。区间深度s u v x y t区间图1: 传递性的等式证明 d区间深度s u v x y t 区间图2: 有深度限制的传递性等式证明 8 结论我们已经呈现我们开展去抓住一件大的个案研究的自动化。自动化被修整到交互式的使用，自动化以一个证明搜寻引擎和简单化的整合为根底，本质上依赖于完成。这节的奉献是根据根本的证明搜寻，和它的简单化整合，在一个交互式假定里解说目前自动化的失败。我们的技术没有走出等式术语逻辑的范畴，不过甚至在这样一个被限制领域，我们遇到了很多的问题。另一方面，解决这些问题，我们没有对特殊自动化领域的需求。我们不否认，在线性算术区域中，这样的程序对有效的自动化是很有必要的。然而，我们的经验说明简单化和证明的搜寻是一个非常有效的组合，这可能是逻辑现象一个例证 从一点点开始一个长的方法。在先前的章节中我们提到一些将来工作的可能性，我们在这里概述。 引进规那么的完全理论的议题应该是被追求的，虽然这不可能有许多实际的影响。 在证明搜寻期间，怎样合并辅助定理的议题是应该追求的。克雷格的插入补助定理意味着以句法的特征为根底的新奇方式在当前目标和一个辅助定理之间被分享：如果一个辅助定理和当前目标以不同的语言被表达，这时辅助定理为了要证明当前目标是没有什么用的。克雷格的插入补助定理为 FOL 支撑，但是把扩充的主意到较富有的理论是有可能的。 完成可能被扩充为完全的完成la Huet。有条件的完成也应该被实现，以便它应付通常的情形，而且支持理论应该被开展。更远地说，为了支持不同的等式概念，完成的执行应该被一个等式的概念参数化，这等式与HOL的嵌入的等式不同。一件额外的工作是整合好自动的终止证明器，就像完成程序的 AProVE，所以使用者交互作用是最小化的。 自动化的连接应该被扩充，以便使用者不会因太多的信息而忙得不可开交。 自动化整体上而言为了提高策略的效率，需要再实现。 我们企图实行替代选择的方法和证明的搜寻去处理经由适宜的关闭和连接等式这包括将来的工作的产生作为这个工作的直接结果。我们现在考虑其他没有被防范的时机。虽然我们相信我们的方式很大地解决了一个被给定的辅助定理的证明问题，但是辅助定理和定义的选择主要是一个技巧的事情。在辅助定理的情况下，我们典型地在理论的边界上累积它们，然后寻找一般的辅助定理，它包含了几个这样的例子。这些增强是归纳假定的增强的回忆。我们也发现在一些领域中,在理论之间有一个在边界上的非琐细的辅助定理的爆发，这在推广上无法被减少。这典型地普通数学对象的发生，就像一棵树。许多辅助定理直观上似乎合理的，但是它们的证明时常包括相当多的努力。在这情况下，似乎很难控制子理论的传播使其进入主要的理论，因为子理论的辅助定理是如此的普遍被用于主要的理论之中。因此在这里我们有三个相关的问题，即：来自一个子理论的重要而独立的辅助定理的扩展被请求。辅助定理的直观似乎合理的，这很难去证明。辅助定理渗入主要理论,减少模组化和使主要的理论很重地依赖在子理论上。这里似乎没有方法减少在一些辅助定理里的爆发。根据证明，我们注意到困难从需要发生小心地说归纳法补助定理，所以这主要地是归纳证明的一个自动化的失败。我们也注意在这一个区域中的大部份的定义暗示可运行,以至于这里有一些模式检查的形式范围经由定义的执行。这依次能用来告诫一个归纳的证明器作为事实或不同的猜想辅助定理。我们没有提及自动化的归纳法，或其他的更高阶的功能。我们有更多要说关于在章节？的介绍。但是能够说这可能像一个困难的领域。我们也注意关于在策略混合的推论方面的困难。我们感觉到最近的提议朝向微积分学的策略可以证明是有趣的。我们建议相对琐细的步骤, 就像确定策略手写体是树结构而不是线性的结构, 而且在证明
展开阅读全文