1、编号： 毕业设计英文翻译 题 目: Automation 院 （系） ： 计算机系 专 业： 自动化 学生姓名： 学 号： 指导教师： 职 称： Automation Tom Ridge April 12, 2005 Contents 1 Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 2 Requirements. . . . . . . . . . . . . .
2、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 3 Current Automation in Interactive Provers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 4 Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3、. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.1 Proof Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.1.1 Logical System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4、 . . . . . . . . . . . . 6 4.1.2 Intro Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 4.2 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 4.2.
5、1 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 4.2.2 Conditional Simplification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2.3 Completion . . . . . . . . . . . . . . . .
6、 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.2.4 Dynamic Completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11 4.2.5 Equational Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 5 Interface and Integration . . . . . . . . . . . . . . . . . . . . . . . .
