电子式里程碑毕业设计英文翻译.doc

《电子式里程碑毕业设计英文翻译.doc》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、编号：毕业设计英文翻译译文题目:Automation院（系）：计算机系专业：自动化学生姓名：李林学号：010320311指导教师：龙超职称：实验师2005年6月3日自动化汤姆里治2005年四月12日目录1介绍..................................................................12需求...................................................................13目前交互式证明器的自动化.....................................

2、.......44技术...................................................................54.1证明的搜寻..............................................................64.1.1逻辑系统...............................................................64.1.2引进规则............................................................

3、...64.2等式....................................................................84.2.1改写...................................................................84.2.2条件的简单化................................................................94.2.3完成........................................................

4、..........104.2.4动态的完成..............................................................114.2.5方程式的统一...............................................................125连接与整合..............................................................126评估.........................................................

5、.........136.1评估生产需求..............................................................136.2完整性.................................................................146.3效率..................................................................146.4实际应用.......................................................

6、.......157替代选择..............................................................168结论..................................................................191介绍自动化可能是成功的机械化的关键。在一些情形中，机械化不需要自动化就可以实行。确实，在高度抽象的数学区域，大部分由使用者拼出的复杂证明组成的机械化推论远远超过了那些目前能被自动化解决的范围。在这一背景下，如果自动化它被全部使用，将指导在容易的可以解决的被紧紧地限定的次问题上。一个机

7、械化的典型例子是我们的拉姆齐定理的形式化。另一方面，在推论相对被限制的地方，自动化能富有成效地在确认类型的证明中被应用，但是绝对程度的细节将使一个非自动化的机械化不可实行。许多人已经花费了数年来发展全自动系统。比如Vampire[VR]和otter[McC]全自动系统。我们可以和这样的系统竞争的设想是愚蠢的。它们的执行是一种方式，这种方式超过目前在交互式定理证明器被实行的系统。这些计划正在进行是为了把这些系统和交互式定理证明器相连。这是极其有价值的工作：如果知道一个一阶的陈述是可证明的，这时