自动化Automation

自动化Automation(中文15000,英文11000字)

1  介绍
自动化可能是成功的机械化的关键。在一些情形中，机械化不需要自动化就可以实行。确实，在高度抽象的数学区域，大部分由使用者拼出的复杂证明组成的机械化推论远远超过了那些目前能被自动化解决的范围。在这一背景下，如果自动化它被全部使用， 将指导在容易的可以解决的被紧紧地限定的次问题上。一个机械化的典型例子是我们的拉姆齐定理的形式化。另一方面，在推论相对被限制的地方，自动化能富有成效地在确认类型的证明中被应用，但是绝对程度的细节将使一个非自动化的机械化不可实行。
许多人已经花费了数年来发展全自动系统。比如Vampire [VR] 和otter [McC]全自动系统。我们可以和这样的系统竞争的设想是愚蠢的。它们的执行是一种方式，这种方式超过目前在交互式定理证明器被实行的系统。这些计划正在进行是为了把这些系统和交互式定理证明器相连。这是极其有价值的工作：如果知道一个一阶的陈述是可证明的，这时应该期待机器能提供一个证明。
在这一节中，我们简略说明一些我们已经在各种不同的情况应用研究的技术。自然地我们不企图仅此一次去解决自动化推论的问题。宁可我们把重心集中在问题，而这些问题典型地出现在我们已经涉及的研究。我们首先简略说明我们需要的自动化的引擎功能。我们然后描述我们应用的技术，而且他们是如何整合的。我们评估根据我们的需求性质上地产生的引擎，和数量地有关于一件相当大的案例研究。这些技术中的少数是新奇的，宁可，我们企图用一种适宜的方式来融合现行的技术。
这些步骤在HOL启发定理证明器被发展，这是我们建立的设计原型的一辆优良车辆的不同方法。

1 Introduction
Automation can be key to successful mechanisation. In some situations, mechanisation is feasible without automation. Indeed, in highly abstract mathematical areas, most mechanised reasoning consists of the user spelling out complicated arguments which are far beyond those which can currently be tackled by automation. In this setting, automation, if it is used at all, is directed at easily solvable, tightly defined subproblems. A typical example of such a mechanisation is our formalisation of Ramsey's Theorem [Rid04]. On the other hand, automation can be fruitfully applied in verification style proofs, where the reasoning is relatively restricted, but the sheer level of detail makes a non-automated mechanisation infeasible.