自动化外文翻译Word文档格式.docx

自动化外文翻译Word文档格式.docx

《自动化外文翻译Word文档格式.docx》由会员分享，可在线阅读，更多相关《自动化外文翻译Word文档格式.docx（45页珍藏版）》请在冰点文库上搜索。

1Introduction...............................................................1

2Requirements..............................................................1

3CurrentAutomationinInteractiveProvers.......................................4

4Techniques...............................................................5

4.1ProofSearch...........................................................6

4.1.1LogicalSystem.....................................................6

4.1.2IntroRules.........................................................6

4.2Equality...............................................................8

4.2.1Rewriting..........................................................8

4.2.2ConditionalSimplification............................................9

4.2.3Completion.......................................................10

4.2.4DynamicCompletion....................................................11

4.2.5EquationalUnification...................................................12

5InterfaceandIntegration......................................................12

6Assessment...............................................................13

6.1Assessmentwrt.Requirements...............................................13

6.2Completeness.............................................................14

6.3Efficiency.............................................................14

6.4InPractice.............................................................15

7Alternative................................................................16

8Conclusion................................................................19

1Introduction

Automationcanbekeytosuccessfulmechanisation.Insomesituations,mechanisationisfeasiblewithoutautomation.Indeed,inhighlyabstractmathematicalareas,mostmechanisedreasoningconsistsoftheuserspellingoutcomplicatedargumentswhicharefarbeyondthosewhichcancurrentlybetackledbyautomation.Inthissetting,automation,ifitisusedatall,isdirectedateasilysolvable,tightlydefinedsubproblems.AtypicalexampleofsuchamechanisationisourformalisationofRamsey'

sTheorem[Rid04].Ontheotherhand,automationcanbefruitfullyappliedinverificationstyleproofs,wherethereasoningisrelativelyrestricted,butthesheerlevelofdetailmakesanon-automatedmechanisationinfeasible.

ManymanyearshavebeenspentdevelopingfullyautomaticsystemssuchasVampire[VR]andOtter[McC].Itwouldbefoolishtoimaginethatwecouldcompetewithsuchsystems.Theirperformanceiswaybeyondthatofsystemscurrentlyimplementedininteractivetheoremprovers.Projectsareunderway[MP04]tolinksuchsystemstointeractivetheoremprovers.Thisisextremelyvaluablework:

ifoneknowsthatafirstorderstatementisprovable,thenoneshouldprobablyexpectthatthemachinecanprovideaproof.

Inthissection,weoutlinesometechniqueswehaveappliedinvariouscasestudies.Naturallywedonotseektosolvetheproblemofautomatedreasoningonceandforall.Ratherwefocusontheproblemsthattypicallyariseinthecasestudieswehavebeeninvolvedwith.Westartbyoutliningthefunctionalitywerequireoftheautomatedengine.Wethendescribethetechniquesweapplied,andhowtheywereintegrated.Weevaluatetheresultingenginequalitativelyintermsofourrequirements,andquantitativelywithrespecttoasizablecasestudy.Fewofthesetechniquesarenovel,rather,weseektocombineexistingtechniquesinasuitablefashion.

TheseproceduresweredevelopedintheHOLLighttheoremprover,whichwefoundtobeanexcellentvehicleforprototypingdifferentapproaches.

2Requirements

Whatdowerequireofourautomation?

Letusdistinguishbetweenautomationforfullyautomaticuse,andautomationforinteractiveuse,therequirementsforeachbeingconsiderablydifferent.

Perhapsunexpectedly,failureoftheautomatedproofengineisthenorm,isthesensethatwheninteractivelydevelopingcomplexproofswespendmostofourtimeonobligationsthatare"

almost"

provable.Thuswewouldliketheprovertogiveusexcellentfeedbackastowhyobligationscouldnotbedischarged.[Sym98]

Thisquoteemphasizesanimportantdifferencebetweenautomaticandinteractiveproof.Inautomaticproof,onetypicallyknowsthatthegoalisprovable（oratleast,suspectsverystrongly,andispreparedtowaitaconsiderableamountoftimebeforeterminatingaproofsearch）.Indeed,automaticproversarejudgedonhowmanyprovablegoalstheycanactuallyprove.Ininteractiveproof,"

wespendmostofourtimeonobligationsthatarealmostprovable"

.Thisisthedifferencebetweeninteractiveandautomaticproof.Ifwespendmostofthetimetryingtoprovegoalsthataresimplynotprovable,thencompletenessoftheproofsearchbecomeslessimportant.Thisisnottosaythatitlosesimportancealtogether:

ifasystemlackscompleteness,thenitwillfailtoprovesomeprovablegoals.Itisvitallyimportanttoknowwhatsortofgoalsoneisgivingupon,inorderthatonecanunderstandwhatitmeanswhenaproverfailstoproveagoal.Suchknowledgeisalsousefulwhencombiningsystems:

inordertounderstandthebehaviourofthesystemasawholeone

shouldfirstunderstandthebehaviouroftheparts.

Whatpropertiesmightbepreferred,inaninteractivesetting,overcompleteness?

Forus,themostimportantaspectofautomationissimplicity.Bythiswedonotmeanimplementationsimplicity（howmanylinesdidittaketoimplementthesystem?

etc.）,butconceptualsimplicity.Forinstance,simplificationisusedubiquitouslyininteractivetheoremproving.Ifthesetofrewriterulesisnotconfluent,thentounderstandthebehaviourofthesimplifier,onehastounderstandtheorderinwhichtherulesareapplied.Needlesstosay,thisisanextremelycomplexthingtounderstand,andproofswhichdependonthesepropertiesarepresumablyextremelyfragile.Conceptualsimplicityforasimplifieriscloselyboundupwithconfluenceandterminationofthesimpset.Conceptualsimplicityisimportantifauseristounderstandthesystem.Ifasystemisconceptuallysimple,itwillhopefullybesimpletouse.

Inaninteractivesetting,weexpectautomationtofail.Inordertomakeprogress,wemustunderstandwhyaproofattemptfails:

theprovermustprovidefeedback.Resolutionbasedsystemscanprovidefeedback,buttheyaredestructive（inthesensethatthegoalisconvertedintoanormalformbeforetheproofattemptstarts,destroyingtheoriginallogicalstructure）,sothatthefeedbackcanbedifficulttounderstand（thepointwheretheprooffailsmaylookverydifferenttotheoriginalgoal）.Abetterapproachistoconducttheproofinawaythatisascloseaspossibletohowahumanmightconducttheproof.Werequiretheproofsystemtobenaturalinsomesense.Inthiscase,ifaproofattemptfails,thefailingbranchcanoftenbereturneddirectlytotheuserforinspection.

Feedbackisrelatedtovisibility.Oftenauserwishestoinspectafailedproof,butonlyaprooftraceisavailable,whichcancauseaconceptualmismatch:

theuserisfocusedonsequents,whereasthetracemaybeofadifferentnaturealtogether.Iftherearemanyunprovedbranches,thenausermightnotinspectthemall,butmightwishtostepthroughtheproof.Automaticmethods,suchasJohnHarrison'

simplementationofmodelelimination[Har96],oftensearchforaproofinatreemakinguseofglobalinformationaboutnodesvisitedpreviously.Ifthisglobalinformationisnotpresentinthesequenttheuserhasaccessto,itwillbedifficulttostepthroughtheautomaticproofbysimplyinvokingtheautomaticproverastepatatime:

theautomaticproverwillnotmakethesamedecisionsitmadewhenconductingthesearchusingglobalinformationbecauseitonlyhasaccesstothelocalsequent.

Manymethodscurrentlyemployedbyinteractivetheoremprovers,suchasIsabelle'

sblast,leavethegoalunchangediftheyfailtoproveit.Naturalmethodsofproofsearchexpecttomakeatleastsomeprogressinallsituations,sothattheycanassistevenifthegoalisnotprovable.Forinstance,safesteps（suchas∧Einmanysystems）shouldbeperformed,simplificationstepsappliedandsoon.

Automationshouldalsobestable.Inlargeproofs,onefrequentlymixesinteractiveandautomaticproof.Ifthegoalsreturnedbyautomationareapttochangeradicallywithslightvariationsinthegoal,thenthedependentinteractiveproofscanberendereduseless,andmu