英文资料.doc

英文资料.doc专业文档珍贵文档 Automation Tom Ridge April 12, 2005 Contents 1 Introduction. ..............................................................1 2 Requirements. .............................................................1 3 Current Automation in Interactive Provers. ......................................4 4 Techniques ...............................................................5 Proof Search ...........................................................6 Logical System .....................................................6 Intro Rules .........................................................6 Equality ...............................................................8 Rewriting ..........................................................8 Conditional Simplification ............................................9 .......................................................10 pletion ....................................................11 Equational Unification ...................................................12 5 Interface and Integration ......................................................12 6 Assessment ...............................................................13 Assessment wrt. Requirements ...............................................13 .............................................................14 专业文档珍贵文档 Efficiency .............................................................14 In Practice .............................................................15 7 Alternative ................................................................16 8 Conclusion ................................................................19 1 Introduction Automation can be key to essful mechanisation. In some situations, mechanisation is feasible without automation. Indeed, in highly abstract mathematical areas, most mechanised reasoning consists of the user spelling plicated arguments which are far beyond those which can