编号：毕业设计英文翻译译文题目: Automation院（系）：计算机系专业：自动化学生姓名：学号：指导教师：职称：2005 年6 月3日自动化汤姆里治2005 年四月 12 日目录1 介绍 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 目前交互式证明器的自动化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .44 技术. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 4.1 证明的搜寻. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.1.1逻辑系统. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.1.2引进规则. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.2 等式. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 4.2.1改写. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 4.2.2条件的简单化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 4.2.3完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.2.4动态的完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .114.2.5方程式的统一. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .125 连接与整合. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .126 评估. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 6.1 评估生产需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13 6.2 完整性. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 6.3 效率. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .146.4 实际应用. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 替代选择. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 结论. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .191 介绍自动化可能是成功的机械化的关键。
在一些情形中，机械化不需要自动化就可以实行。
确实，在高度抽象的数学区域，大部分由使用者拼出的复杂证明组成的机械化推论远远超过了那些目前能被自动化解决的范围。
在这一背景下，如果自动化它被全部使用，将指导在容易的可以解决的被紧紧地限定的次问题上。
一个机械化的典型例子是我们的拉姆齐定理的形式化。
另一方面，在推论相对被限制的地方，自动化能富有成效地在确认类型的证明中被应用，但是绝对程度的细节将使一个非自动化的机械化不可实行。
许多人已经花费了数年来发展全自动系统。
比如Vampire [VR] 和otter [McC]全自动系统。
我们可以和这样的系统竞争的设想是愚蠢的。
它们的执行是一种方式，这种方式超过目前在交互式定理证明器被实行的系统。
这些计划正在进行是为了把这些系统和交互式定理证明器相连。
这是极其有价值的工作：如果知道一个一阶的陈述是可证明的，这时应该期待机器能提供一个证明。
在这一节中，我们简略说明一些我们已经在各种不同的情况应用研究的技术。
自然地我们不企图仅此一次去解决自动化推论的问题。
宁可我们把重心集中在问题，而这些问题典型地出现在我们已经涉及的研究。
我们首先简略说明我们需要的自动化的引擎功能。
我们然后描述我们应用的技术，而且他们是如何整合的。
我们评估根据我们的需求性质上地产生的引擎，和数量地有关于一件相当大的案例研究。
这些技术中的少数是新奇的，宁可，我们企图用一种适宜的方式来融合现行的技术。
这些步骤在HOL启发定理证明器被发展，这是我们建立的设计原型的一辆优良车辆的不同方法。
2 需求我们的自动化的需求是什么? 让我们区别一下自动化和全自动化的使用，以及交互式自动化的使用，每一种的需求都有非常地不同。
也许料想不到地，失败的自动化证明引擎是基准，是观念，这观念是当交互式发展的复杂证明使我们花费大多数时间对" 几乎" 的可证明的义务的时候。
因此我们想要证明器给我们完美的反馈作为为什么任务不能够被执行的原因。
这引证强调一种在自动化和交互式证明之间的重要的不同。
在自动校对中，可典型地知道，目标是可证明的( 或至少，非常强烈地怀疑，而且在结束相当多量的时间之前准备等候证明的搜寻)。
的确，自动证明器被判断在他们能实际上证明多少可证明的目标之上。
在交互式证明中，" 我们花费我们大多数的时间在几乎可证明的义务上"。
这是交互式和证明之间的不同。
如果我们花费大部份的时间尝试去证明简单但不可证实的目标，然后校正的搜寻完全变成比较不重要。
这虽不能说是它全部失去重要:：如果一个系统缺乏完整性，这时它将会无法证明一些可证明的目标。
什么类型的目标正在被放弃，这是非常必要而且主要去知道的，这是为了知道当一个证明器失败于证明一个目标时就能理解它是什么意思。
这些知识也非常有用，当混合系统为了了解作为整个系统的行为，应当首先了解部分的行为。
在一个交互式的环境中，在完全之上所有物可能被偏爱，就我们而言，自动化的最重要方面是简单化。
而这些我们不是意味着去落实简单( 要布多少根线来实现系统? 等等)，而是概念上的简单化。
例如，简单化到处被用于交互式定理求证。
如果一组改写规则不能融合，这时去了解简化器的行为，必须了解适用的规则顺序。
不用说，对于理解这是一件极端复杂的事情，而且属于这些所有物的证明在推测上极端易碎。
概念上的简单化通过聚集和简易装置的终端对一个简化器进行紧密地约束。
如果一个使用者要了解系统，概念上的简单化很重要。
如果一个系统的概念简单，它将会很有希望被简单的使用。