电子式里程碑毕业设计英文资料.doc

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

1、AutomationTomRidgeApril12,2005Contents1Introduction...............................................................12Requirements..............................................................13CurrentAutomationinInteractiveProvers......................

2、.................44Techniques...............................................................54.1ProofSearch...........................................................64.1.1LogicalSystem.....................................................64.1.2IntroRu

3、les.........................................................64.2Equality...............................................................84.2.1Rewriting..........................................................84.2.2ConditionalSimplification............

4、................................94.2.3Completion.......................................................104.2.4DynamicCompletion....................................................114.2.5EquationalUnification............................................

5、.......125InterfaceandIntegration......................................................126Assessment...............................................................136.1Assessmentwrt.Requirements...............................................136.2Compl

6、eteness.............................................................146.3Efficiency.............................................................146.4InPractice.............................................................157Alternative.................

7、...............................................168Conclusion................................................................191IntroductionAutomationcanbekeytosuccessfulmechanisation.Insomesituations,mechanisationisfeasiblewithoutautomation.Indeed,inh

8、ighlyabstractmathematicalareas,mostmechanisedreasoningconsistsoftheuserspellingoutcomplicatedargumentswhicharefarbeyondthosewhichcancurrentlybetackledbyautomation.Inthissetting,automation,ifitisusedatall,isdirectedateasilysolvable,tightlydefin