电子式里程表英文翻译

编号：

毕业设计英文翻译译文

题 目: Automation

院 （系）： 计算机系

专 业： 自动化

学生姓名： 李 林

学 号： 010320311

指导教师： 龙 超

职 称： 实验师

2005 年 6 月 3日

自动化

汤姆里治

2005 年四月 12 日

目 录

1 介绍 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1

2 需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1

3 目前交互式证明器的自动化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4

4 技术. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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动态的完成. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11

4.2.5方程式的统一. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 5 连接与整合. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12

6 评估. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13

6.1 评估生产需求. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13

6.2 完整性. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

6.3 效率. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14

6.4 实际应用. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7 替代选择. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

8 结论. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .19

1 介绍

自动化可能是成功的机械化的关键。在一些情形中，机械化不需要自动化就可以实

行。确实，在高度抽象的数学区域，大部分由使用者拼出的复杂证明组成的机械化推论

远远超过了那些目前能被自动化解决的范围。在这一背景下，如果自动化它被全部使用，

将指导在容易的可以解决的被紧紧地限定的次问题上。一个机械化的典型例子是我们的

拉姆齐定理的形式化。另一方面，在推论相对被限制的地方，自动化能富有成效地在确

认类型的证明中被应用，但是绝对程度的细节将使一个非自动化的机械化不可实行。

许多人已经花费了数年来发展全自动系统。比如Vampire [VR] 和otter [McC]全自

动系统。我们可以和这样的系统竞争的设想是愚蠢的。它们的执行是一种方式，这种方

式超过目前在交互式定理证明器被实行的系统。这些计划正在进行是为了把这些系统和

交互式定理证明器相连。这是极其有价值的工作：如果知道一个一阶的陈述是可证明的，

这时应该期待机器能提供一个证明。

在这一节中，我们简略说明一些我们已经在各种不同的情况应用研究的技术。自然

地我们不企图仅此一次去解决自动化推论的问题。宁可我们把重心集中在问题，而这些

问题典型地出现在我们已经涉及的研究。我们首先简略说明我们需要的自动化的引擎功

能。我们然后描述我们应用的技术，而且他们是如何整合的。我们评估根据我们的需求

性质上地产生的引擎，和数量地有关于一件相当大的案例研究。这些技术中的少数是新

奇的，宁可，我们企图用一种适宜的方式来融合现行的技术。

这些步骤在HOL启发定理证明器被发展，这是我们建立的设计原型的一辆优良车

辆的不同方法。

2 需求

我们的自动化的需求是什么? 让我们区别一下自动化和全自动化的使用，以及交互

式自动化的使用，每一种的需求都有非常地不同。

也许料想不到地，失败的自动化证明引擎是基准，是观念，这观念是当交互式发展

的复杂证明使我们花费大多数时间对 " 几乎 " 的可证明的义务的时候。因此我们想要

证明器给我们完美的反馈作为为什么任务不能够被执行的原因。

这引证强调一种在自动化和交互式证明之间的重要的不同。在自动校对中，可典型

地知道，目标是可证明的 ( 或至少，非常强烈地怀疑，而且在结束相当多量的时间之

前准备等候证明的搜寻)。的确，自动证明器被判断在他们能实际上证明多少可证明的

目标之上。在交互式证明中，" 我们花费我们大多数的时间在几乎可证明的义务上"。

这是交互式和证明之间的不同。如果我们花费大部份的时间尝试去证明简单但不可证实

的目标，然后校正的搜寻完全变成比较不重要。这虽不能说是它全部失去重要:：如果一

个系统缺乏完整性，这时它将会无法证明一些可证明的目标。什么类型的目标正在被放

弃，这是非常必要而且主要去知道的，这是为了知道当一个证明器失败于证明一个目标时就能理解它是什么意思。这些知识也非常有用，当混合系统为了了解作为整个系统的

行为，应当首先了解部分的行为。

在一个交互式的环境中，在完全之上所有物可能被偏爱，就我们而言，自动化的最

重要方面是简单化。 而这些我们不是意味着去落实简单 ( 要布多少根线来实现系统?

等等)，而是概念上的简单化。例如，简单化到处被用于交互式定理求证。如果一组改

写规则不能融合，这时去了解简化器的行为，必须了解适用的规则顺序。不用说，对于

理解这是一件极端复杂的事情，而且属于这些所有物的证明在推测上极端易碎。概念上

的简单化通过聚集和简易装置的终端对一个简化器进行紧密地约束。如果一个使用者要

了解系统，概念上的简单化很重要。如果一个系统的概念简单，它将会很有希望被简单

的使用。

在一个交互式环境中，我们期待自动化失败。为了取得进步，我们必须了解一种证

明的尝试为什么失败，证明器一定会提供反馈。基于系统的决议能提供反馈，但是他们

是毁灭性的 (在某种意义上目标转换成一种正常的形式在证明的尝试之前开始，破坏了

最初的逻辑结构)，所以反馈很难被了解 (论证失败的点对于最初的目标能看出明显的不