Form and Content

Ph.D.DissertationProposal

JaredDavis

DepartmentofComputerSciencesTheUniversityofTexasatAustin1UniversityStationC0500Austin,TX78712-0233,USA

jared@cs.utexas.edu

October22,2007

Contents

1Introduction

2Sketchofourproposal

2.1Formalverification........................1332.2Ourchoiceoflogic........................2.3Computerscheckingproofs....................2.4Ourproofchecker.........................2.5Proofcheckerextensions.....................2.6Proposedextensions.......................2.7Usingextensions.....

....................3Presentandremainingwork

3.1Sketchofourlogic........................3.2Ourproofchecker.........................3.3BuildingProofp-checkableproofs................3.4ExtendingProofpwithanewrule................3.5Provingthenewruleissound..................3.6Remainingwork..........................4Relatedwork

4.1Currenttheoremprovers.....................4.2Embeddedproofcheckers.....................4.3Independentproofchecking...................4.4Metareasoning.......

...

................

4577810111116181820232424282930

1Introduction

Programshaveprecisesemantics,sowecanusemathematicalprooftoes-tablishtheirproperties.Theseproofsareoftentoolargetovalidatewiththeusual“socialprocess”ofmathematics,soinsteadwedevelopandcheckthemwiththeorem-provingsoftware.Thissoftwaremustbesophisticatedenoughtomaketheproofprocesstractible,butthisverysophisticationcastsdoubtuponthewholeenterprise:whoverifiestheverifier?

Inthisthesis,weproposedevelopingauseful,mechanically-verifiedthe-oremprover.Ourprogramwillsatisfytwooften-conflictinggoals:

•Trust.Ourproverwillbebasedonawell-understoodlogicandshouldonlyaccepttheorems.Thesoundness-criticalcodewillbeeasytoiden-tifyandshortenoughforagoodprogrammerormathematiciantoreviewinafewhours.

•Capability.Oursystemwillprovidetoolstohelptheuserconstructproofs.Forexample,itwillpermittheusertosetuplemmasthatcanbeautomaticallyreusedtomakeprogressinnewproofattempts.Therearemanywaystoapproachthesegoals.Oursistoproveourprogramissound,i.e.,ifitclaimsaformulaisatheorem,thenitisatheorem.

Ofcourse,wecannotmeaningfullyuseourprogramtoproveitsownsoundness,sincethiswouldbelikeaskingsomeoneiftheyeverlie.Instead,weimaginetwoprograms,AandB.Aisaproofcheckerthatonlyacceptsproofscomposedofthemostprimitivesteps,likeinstantiationandcut;Aissosimplethesocialprocessofmathematicscanestablishbothitssoundnessandtheconsistencyofthelogicaltheoryitimplements(soweknowtheoremsare“alwaystrue”).Meanwhile,Bisthepractically-useful,automatedtheoremproverweareproposingtoverify.Inthisthesis,wewillconstructanA-styleproofthatshowsBissound,andcheckthisproofwithA.Then,sincewetrustA,andsinceAsaysBissound,wecanalsotrustB.

Ourfirsttaskistowritetheproofchecker,A.WhichlogicshouldAimplement?Wewilluseacomputational,quantifier-free,first-orderlogicoftotal,recursivefunctionswithinduction,modeledaftertheACL2logic.Ourlogic,likeanyother,putsforthasyntacticdefinitionofproof,sowritingaproofcheckerjustmeanstranslatingthisdefinitionintoaprogram.Thisisstraightforwardandcouldbedoneinanyreasonableprogramminglanguage,sowhichlanguageshouldweuse?Ourlogic,likeACL2’s,iscompatiblewith

1

CommonLisp,sowecantreatthefunctionswedefineasLispprograms.AndthereisgoodreasontowriteAasaprograminourlogic.SinceourgoalistouseAtoprovethesoundnessofB(“ifBacceptsφ,thenφisprovable”),weneedawaytoexpressprovabilityinourlogic.WritingAinourlogicletsusdothisquiteeasily,i.e.,wecansay“φisprovablewhenthereisaproofofφthatAaccepts.”

Wealsoneedtodevelopthetheoremprover,B.LikeA,wewriteBasaprograminourlogicsowecanreasonaboutitsdefinition.BwillbefarmoresophisticatedthanA,e.g.,itwillincludearule-drivensimplifierwhichcanemploycalculation.ButthismeanstheproofofB’ssoundnesswillbeadeepresult,whichisconcerningsinceA-styleproofsaretedioustowriteandexcessivelylarge.

Howcanweconstructthisproof?OurapproachisfirsttouseACL2,amatureandcapabletheoremprover,to“sketchout”theproof(normallyACL2isthoughtofasaformalandtrustedtool,buthereweareonlyusingitinaninformalcapacity.)UsingACL2inthiswayallowsustoplanourproofwithoutneedingtoconfront,simultaneously,theproblemofbuildingA-styleproofs.Afterwehaveasolidideaofhowtheproofshouldgo(andarereasonablyconvinceditis,infact,atheorem),wecanbeginworkingontranslatingoursketchintoanA-styleproof.

HowbigwillthisA-styleproofbe?WillitbepracticaltouseAtocheckit?HereourapproachistolayertheverificationofB.Thatis,insteadofgoingdirectlyfromAtoB,wewilluseAtoverifyA󰀁,aslightlyricherproofchecker,thenuseA󰀁toverifyA󰀁󰀁,etc.,untilwegettoB.EachsuccessiveproofcheckeracceptsanewkindofproofstepthatisnotavailableinA,e.g.,perhapsA󰀁addsatautologycheckersoitcanproveanytautologyinonestep,whereasitmighttakehundredsorthousandsofstepstoprovesometautologywithA.OnceeachAihasbeenverified,wecantrustitasmuchaswetrustA,andwecanmakeuseofitsnewcapabilitiesaswesetouttoverifyAi+1.

SuccessfullyverifyingBwillmakethefollowingcontributions:•Anewtool.Ourfinalprogramwillbesuitableindomainsfromcircuitanalysistoprogramverification,andwillconveygreaterconfidencethantoolswithlarger,lessdeliberately-definedcores.

•Metatheoryasaproverdesign.Wewillcounterthesizeofformalproofsbyaddingnewproofmethodstoraiseourlevelofabstraction,whileverifyingthesemethodstoensuresoundness.

2

•Extensibleproofmethods.Usersmaydevelopnew,customproofmeth-odsfortheirdomainseitherastactic-styleprogramsforB,orasnewprovers(B󰀁,B󰀁󰀁,...)whichcanbeverifiedwithB.TheworkwehavedonetoverifyBwillprovideusefullemmasforverifyingthesenewprovers.

•Efficientproofconstruction.Wewillformallyverifyseveralextendedproofmethods.Byhavingshownthesealgorithmscanbetrusted,wemayfreelyusethemwithoutcheckingtheirwork.Forexample,Bwillincludeaverifiedrewriter.

•Potentialtargetforothersystems.Externalprogramsmaybeabletoconstructhigher-level,B-orB󰀁-styleproofsmoreeasilythanlow-levelA-styleproofs.

2Sketchofourproposal

Wewillnowgiveamoredetailedtourofourproposal.Webeginbydiscussingthenotionsofformalproofandformalverification(§2.1),thelogicwewilluse(§2.2),thepotentialforerrorswhencomputerscheckproofs(§2.3),andourA-styleproofchecker(§2.4).Wethenturnourattentiontotheextendedproofcheckers(A󰀁,A󰀁󰀁,...,B)anddescribehowtheycanbeimplemented(§2.5),whattypesofproofmethodstheywillimplement(§2.6),andfinallyhowtheycanbeputtouseintheproofofB’ssoundness(§2.7).

2.1Formalverification

Formalverificationistheuseofmathematicalprooftoshowhardwareorsoftwaredesignshavedesirableproperties.WeadoptaHilbert-esquenotionofproofasa“step-by-step,syntacticallycheckabledeductionasmaybecar-riedoutwithinaconsistent,formallogicalcalculus.”[DLP77]Wecallthisformalproof.

The“veryidea”offormalverificationwaschallengedbyJamesFet-zer[Fet88],whoarguedprogramsarenotmathematicalentitiesbecausetheyrunoncomputers;hence,asinotherappliedscienceswheremeasurementsareimpreciseandnaturallawsareimperfectlyunderstood,strictdeductiveproofsareinappropriate.Butwe,likeHoare[Hoa69],viewComputerScienceasan“exactscience”ofabstractmathematics;ourprogramminglanguages

3

havepuresemanticsindependentlyfromanyphysicalcomputers,anditisthroughthesesemanticswewishtoanalyzeaprogram’sdesign.

DeMillo,Lipton,andPerlis[DLP77]contestedthevalueofformalproof,arguingproofisinsteadthesocialprocesswherebymathematicianscometoagreeaformulaisatheorem.Wecallthisinformalproof.Formalproofs,theyargued,aretoolonganddetailedtobebelievable,andcannotconveyintuitiontothereader.Thisobjectionwasnotwidelyaccepted[Mac01,§6],forasFetzer[Fet88]observed,thevalidityofaformulaandourbeliefinitsvalidityaredistinct;WinstonandO’Brienmayagreetwoplustwomakesfive,buttheirconsensusdoesnotmakeitso.Incontrast,onlytruthsmaybederivedinasoundlogicalframework,soformalproofscanserveas“objectiveevidence”ofthetruthofastatement.

Thereislittlehopemathematicianswillbewillingorabletoproveprop-ertiesaboutinterestingprogramsinformally,as“theproofsofevenverysimpleprogramsrunintodozensofprintedpages.”[DLP77]Butunlikethevaguely-definedsocialprocessbehindinformalproofs,formalproofsinvolveonlysimpleruleswhoseapplicationcanbecheckedbycomputerprograms.Byautomatingtheconstructionandcheckingofformalproofs,formalveri-ficationbecomespossible.

2.2Ourchoiceoflogic

Beforewecanbuildandcheckformalproofs,wemustdecideupona“for-mallogicalcalculus”touse.Moderntheoremproversdonotagreeonanystandard,andthischoiceis“amatteroftasteandexperience”[LP99]whichmaybeviewed“eclecticallyandpragmatically.”[Mac01,§8]

WeproposeusingasimplifiedversionoftheACL2logic[KM98,KMM00].Ourobjectswillbethesymbolsandnaturals,recursivelyclosedunderor-deredpairing.Wewilleliminateguards[KM94,§4.3]andpackagestosim-plifytheconnectionwithCommonLisp.Wewillalsoadoptinfinitely-manyprimitiveconstantsandanewrule,calledbaseevaluation,forapplyingthebasicfunctionslikeconsand+toconstants;thisismuchlikeMc-Carthy’s[McC60]Lispinterpreter,apply,whichhadspecialcasestoevaluate“elementaryS-functions”likecons.

ThemajorcharacteristicsoftheACL2logicwillbepreserved.Ourlogicwillbefirst-order,willlackexplicitquantifiers,andwillhaveequalityasitsonlypredicatesymbol.WewilldirectlyadoptShoenfield’s[Sho67]rulesofpropositionalcalculusandACL2’sinstantiationandinductionrules.Wewill

4

permittheintroductionoftotal,untyped,recursivefunctions,theintroduc-tionofSkolemfunctions,andinductionuptoε0.

Finally,partingwithACL2tofollowtheworkofG¨odel[G¨od31],wewillextendourlogicwithanintegratedproofcheckersowemayestablishmetatheoremsaboutprovability,e.g.,“A󰀁onlyacceptsprovableformulas.”WewillalsoaddaruleofcomputationalreflectionasdescribedbyHarri-son[Har95],toallowtheuseofmetatheoremsduringproofs,e.g.,“A󰀁acceptsφ,soφmustbetrue.”

Thelogicjustdescribedwillberatherrestrictive,notablylackingtypes,quantifiers,andhigher-orderfunctions.But,asKaufmann,Manolios,andMoore[KMM00]havenoted,theselimitationsoften“canbeovercomewith-outundueviolencetotheintuitionsyouaretryingtocapture.”Asevidenceofthisclaim,considerthediverseusesofthesimilarly-restrictiveACL2sys-tem,whichincludetheverificationof:

•processormodels[BKM96,Moo98,GWH00,Saw00],•RTLdesigns[Rus98,RF00],•circuitmodels[Hun00,HR05,HR06],•virtualmachines[BM96,LM03],•compilers[BT00,Goe00],•imperativeprograms[LM04],and

•otheralgorithms[RMT03,TB03,RRAHMM04,MZ05].

Therearealsoadvantagestousingasimplelogic.Forexample,termquo-tationandreflectionaremorestraightforwardwhennotypesareinvolvedandtermequalitydoesnotrelyonreductions[Bar01,How88].Also,becauseourtermsaresosimple,oursystemwillnotneedatypechecker,typeinferenceengine,ormuchinthewayofinterfacinglayerssuchasparsersandtermrendering.

2.3Computerscheckingproofs

Formalproofsaretoolongforhumanstocheckreliably,butcomputersarewellsuitedtothistask.Ourproofcheckingprogram,whichwecalledAinthe

5

introduction,willbeafunctioncalledProofp,definedinourlogic;ourlogicwillbecompatiblewithCommonLisp,sowecanuseaLispsystemtorunthisfunctiononacomputer.ThereareseveralLispimplementations,operatingsystems,andhardwareplatformstochoosefrom,asshowninFigure1.

AllegroLinux x86, x86−64, PPCMacOSX PPC, IntelWindows 32/64Solaris SPARC, AMD64Misc. Unix 32/64CLISPVarious Linux, BSDMacOSX (Fink)Windows (Cygwin)Solaris x86, SPARCMisc. Unix 32/64CMUCLLinux x86, AlphaVarious BSD x86MacOSX PPCSolaris SPARCGCLLinux x86, PPC, SPARC, ...FreeBSDWindows 32 (Cygwin)Solaris SPARCOpenMCLLinux x86−64, PPCMacOSX x86−64, PPCSBCLLinux x86, PPC, SPARC, ...Various BSD x86MacOSX PPC, IntelSolaris x86, SPARCFigure1:AsamplingofCommonLispsystems

Computers,operatingsystems,andLispcompilersarenotperfect,andtheirdefectsmightcauseourprogramtoincorrectlyacceptaninvalidproof.Tomakethislesslikely,wesuggestusingaheterogeneouscollectionofplat-formswhencheckingproofsofinterest.Thisidea,calledn-versionprogram-ming[Avi95],isnotwithoutprecedentincomputer-assistedproof[Mac01,ch.4].Becauseseparategroupshaveindependentlydevelopedthesehard-wareplatforms,operatingsystems,andLispimplementations1,itisunlikelyadiversecombinationofthesesystemswillshareanequivalenterror.

Thisargumentisadmittedlyinformal,butasDijkstra[Dij82]wrote,“[Sci-entificthought]derivesitseffectivenessfromourwillingnesstoacknowledgethesmallnessofourheads”anddealwithproblems“indepthandiniso-lation.”Therearenoformallyverifiedprocessors,operatingsystems,andprogrammingenvironmentsavailableforustouse,andwemuststartsome-where.

1

CMUCLandSBCLareforksofthesamecodebase,buttheotherLispsareoriginal.

6

2.4Ourproofchecker

G¨odel[G¨od31]definedaproofcheckercalledBw2withinhislogicinordertoprovehisincompletenesstheorem.Bwdependedupon43auxiliarydefinitionswhichdealtwithencodingproofsasobjectsinthelogic,andwithrecognizingvalid,encodedproofsteps.

Ourlogicwillbemorecomplex,andourProofpfunctionwillmakeuseofauxiliarydefinitionsincludingprimitiveLispfunctions(suchascons,natp,and+),basiclistutilities(e.g.,len,app,andmemberp),recognizersandconstructorsfortermsandformulas,substitutionoperations,andrecogniz-ersforvalidproofsteps.OurworkingdraftofProofpinvolvesaround100definitions,totallingunder1,000linesofLisp.InadditiontoProofp,wewillalsohaveasmallcommandlooptoreadinstructionsfrominputfiles.

ItwillbedifficulttowriteinterestingProofp-checkableproofssinceProofponlyimplementsbasicrulesofinferenceandprovidesnoautomation.How-ever,itissimplywrittenandisshortenoughtobethoroughlyreviewed.Partofourdissertationwillbeanexplanationofwhythisprogramcorrectlyimplementsourlogic,andwhyourlogicisreasonable.

2.5Proofcheckerextensions

Foroursystemtobeuseful,wewillneedtomakeproofconstructioneasierandmoreautomatic.Weplantodothisbyaddingnewproofmethodsthatarenotfoundamongtheinferencerulesofourlogic.Intheintroduction,wecalledtheseA󰀁,A󰀁󰀁,...,B.Tomaintainourtrustinthesystem,wewillneedtoensurethesenewproofmethodsaresound,i.e.,theycanonlybeusedtoderiveprovableformulas.

OurProofpfunctionisshowngraphicallyinFigure2.Forsimplicitywewillignorethefunctionarities,axioms,andtheoremsittakesasinputs,andonlywriteProofp(x),wherexistheallegedprooftocheck.Proofswillbemadeupofproofsteps,andeachstepwillhaveamethodofproof,aconclusion,and(exceptforaxiomsandtheorems)somesubproofs.Aproofstepwillbeacceptablewhenitsmethodcanbeappliedtoitssubproofstoobtainitsconclusion,e.g.,thecontractionmethodcanbeappliedtoasubproofofφ∨φtoconcludeφ.AproofwillbeacceptedbyProofpwhenallitsstepsareproperapplicationsoftheinferencerulesofourlogic.

2

ShortforBewisfigur,Germanforprooffigure.

7

AcceptAlleged Proofassociativitycutcontraction. . .TheoremsAxiomsFunction AritiesProofpRejectFigure2:OperationofProofp

Anextensionwillbeanewproofcheckingfunction,sayProof2p,thatacceptsalltheproofmethodsknowntoProofpandalsosomenewmethods.Forexample,perhapsProof2pwilladdModusPonensoratautologychecker.WewillsayProof2pissoundwhenwecanprovethesoundnessclaim,

∀x:Proof2p(x)→Provablep(Conclusion(x)),

whereProvablep(φ)isdefinedas,

∃p:Proofp(p)∧Conclusion(p)=φ.

Ifthisclaimisatheorem,thenProof2pdoesnotallowustoproveanythingthatcannotbeprovenbyProofp.

Wecouldestablishsoundnessclaimsbyhandorwithanothertheoremprover,butourtrustinProof2pwouldthendependonexternalproofs.Toavoidthis,weproposedefiningourextensionsasfunctionsinourlogic,sowecanexpressthesesoundnessclaimsinourlogicandprovethemusingonlyProofpandalready-verifiedextensions.

Intheend,wewilltrustallformulasacceptedbyProofparevalidbe-causeProofpisshortandsimpleenoughtoreviewthoroughly.OneoftheseformulaswillstateProof2pcannotacceptformulasthatarenotacceptedbyProofp.Hence,wecantrustanyformulaacceptedbyProof2pistrue.

2.6Proposedextensions

Weplantoaddseveralproofmethods,whichwehaveclassifiedinFigure3aseitherderivedrulesofinferenceorheuristictheoremproving.

8

Derived Rules of InferencePropositional RulesEquality RulesLambda Reduction RulesThe Deduction LawThe Tautology TheoremEquivalence SubstitutionSubstitution of Equals for EqualsHeuristic Theorem ProvingFormula Compilation, ClausificationCalculation of Ground TermsEquality ReasoningConditional Term RewritingDestructor EliminationClause SimplificationFigure3:Overviewofourextensions

Wewillbeginwithderivedrulesofinferenceformanipulatingproposi-tionalformulas,suchasModusPonensanddoublenegationrules.Wewillthenaddrulesforequality,suchasitstransitivityandcommutativity,andthesubstitutionofequaltermsforargumentstofunctionsandlambdas.Moreinterestingderivedrulesofinferencewillincludethedeductionlaw,whichallowsustoproveF→GbytemporarilyassumingFistrue,thenshowingGfollows.OtherclassicmetatheoremswillfollowtheworkofShoen-field[Sho67]andShankar[Sha94],andwillinclude:

•Tautologycheckingforidentifyingpropositionaltautologies,

•Equivalencesubstitutionforpropositionalformulas,i.e.,replacingoc-currencesofFwithGandviceversaafterprovingF↔G,and•Equalitysubstitutionforformulas,i.e.,replacingoccurrencesoft1fort2andviceversaafterprovingt1=t2.

Theseprooftechniquesdonotembodyagenericproofstrategyanddonottakeadvantageofuser-createdknowledgesuchaslemmalibraries.Toaddressthesedeficiencies,ourheuristictheoremprovingextensionsarein-tendedtomimicthekeystrategiesusedbyACL2:toproveaformula,wewillcompileitintoanequivalentterm,whichwillbeconvertedintoaclause;wewillsimplifytheclausebyapplyingconditionalrewriterules,equalityreasoning,andcalculation.Thisapproachallowspreviously-provenlemmas

9

tobeautomaticallyreusedinnewproofattempts,sotheusercanfocusondevelopingstrategiesfortheprovertofollowonitsown.

2.7Usingextensions

Logiciansoftenappealtometatheoremsduringotherwise-formalproofs.Forexample,afterprovingthetautologytheorem,onemightsay,“sinceφisatautology,letpbeaproofofφ,”withoutexplicitlysayinghowpistobeconstructed.Inotherwords,wefeelfreetosubstitutethemetatheoreticallyestablished“φisprovable”foraformalproofofφ.

Reflectionreferstotechniquesthatcapturethisideawithoutaseparatemetalogic.Inoursystem,themetatheoreticnotion“φisprovable”willbeanordinary,formalproofofProvablep(󰀂φ󰀁),where󰀂φ󰀁istheencodedformofφ.Tousethismetatheorem,wewillsupportcomputationalreflection[Har95]:

Provablep(󰀂φ󰀁)

.φSupposeProof2pisanextendedproofcheckerthataddstautologycheck-ing,andwehaveprovenitssoundnessclaim.WenowwanttobeabletoproveformulaswithProof2panditsbuilt-intautologycheckerinsteadofusingtheless-capableProofp.Ourreflectionruleisoneoftwocapabilitiesneededforthis;efficientcomputationofgroundtermsistheother.SupposepisaProof2p-levelproofofφ.Then,wecanconvertpintoaProofp-levelproofasfollows:

1.2.3.4.5.6.

∀x,Proof2p(x)→Provablep(Conclusion(x))SoundnessTheoremProof2p(p)→Provablep(Conclusion(p))InstantiationProof2p(p)→Provablep(󰀂φ󰀁)ComputationProof2p(p)ComputationProvablep(󰀂φ󰀁)ModusPonensφReflection

RecallthatourlogicwillbecompatiblewithCommonLisp,andour

extensionssuchasProof2pwillbefunctionsinourlogic.Asaresult,aCommonLispsystemcanrunourextensions.Tojustifysteps3and4above,wewilluseLisptoevaluateConclusion(p)andProof2p(p).

Manytheoremprovers,includingACL2,PVS,Isabelle/HOL[BN02],andCoq,allowevaluationsinaprogramminglanguagetobetreatedasproofsof

10

equality.ButHarrison[Har95]hasreferredtothistransitionasa“glaringleapoffaith,”andLispevaluationiscertainlynobasicruleofinference.Tohelpjustifyourapproach,anearlyextensionwillbeanevaluatorinthespiritofMcCarthy’s[McC60]functionapply,andwewillproveourevaluatorproducesavaluethatislogicallyequaltoitsinputterm.WebelieveourevaluatorcorrectlymodelsthesemanticsofLispevaluationforourfragmentofthelanguage,butthisargumentcanonlybemadeinformallysinceLisp’sevaluatorisnotdefinedinourlogic.

3Presentandremainingwork

Inthissection,wedescribeourlogic(§3.1),theworkingdraftofourproofchecker(§3.2),andtheconstructionofProofp-levelproofs(§3.3).WethenintroduceasimpleextensionofProofp(§3.4)andexplainhowwewereabletoverifythisextension(§3.5).Finally,weremarkuponwhatstillneedstobedone(§3.6).

3.1Sketchofourlogic

Ouruniverse,U,containsthenaturalsandsymbols,closedunderorderedpairing.WetakesomenotationalconventionsfromLisp:•Wewritetheorderedpairofaandbas(a.b),•(x1x2...xn.b)isshorthandfor(x1.(x2...xn.b)),•()isshorthandforthesymbolnil,•(x)isshorthandfor(x.nil),and

•(x1x2...xn)isshorthandfor(x1.(x2...xn)).

Ourtermsareprimitiveconstants,variables,functionapplications,andλabbreviations.Wewritetermsinthetypewriterfont.

•Wehaveaprimitiveconstantforeveryx∈U,whichwewillwriteas’x.Forexample,’(1.2)istheconstantcorrespondingto(1.2).•Wehaveavariableforeverysymbolexcepttandnil.Forexample,x,y,foo,andbar,arevariables.

11

•Wehaveafunctionnameforeverysymbolexceptnil;quote;first;second;third;fourth;fifth;and;or;list;cond;let;let*;pequal*;por*;andpnot*.Weassociateanaritywitheachfunctionname.Afunctionapplicationiswrittenas(ft1...tn)wherefisafunctionnameofarityn,andeachtiisaterm.

•Alambdaabbreviationiswrittenas((λ(x1...xn)β)t1...tn),whereeachxiisadistinctvariable,andβandeachtiareterms.Tomakesubstitutionsimpler,βmayhavenofreevariablesbesidesthexi.Sincewedonotallowtorniltobevariablesymbols,noambiguityariseswhenweomitthequoteson’tand’nil;similarlywewillnotbothertoquotenumberswhenwewishtousethemasconstants.

Ourformulasareequalitiesbetweenterms(writtent1=t2),negations(written¬F),anddisjunctions(writtenF∨G).Otherconnectives(e.g.,→,∧,and↔)aretreatedasabbreviations.Ourformulashavenoquantifiers,andweinterpretfreevariablesinformulasasuniversallyquantifiedatthetoplevel.

OurrulesforpropositionalcalculusareshowninFigure4,andourrulesforequalityareshowninFigure5.MostofthesearetakenfromACL2[KMM00,§6]andShoenfield[Sho67].

Wetakeforgrantedcertainbasefunctions,inspiredbyCommonLisp,showninFigure6.Thesefunctionsaretotal;theycanbeappliedtoanyobjectsinouruniverse.Foreachbasefunctionfofarityn,andforallcon-stantsc1,...,cn,weaddanaxiomoftheform(fc1...cn)=x,wherexistheappropriateconstant.Theseaxiomsallowustouseprimitivecalcula-tionsinproofs,e.g.,wecanprove(+12)=3inonestep.Theseaxiomsalsoallowustodevelopanevaluatorforarbitrarygroundterms,basedonMcCarthy’s[McC60]applyfunction.

LikeKaufmannandMoore[KM98,p.31–47],weaddseveral“symbolicaxioms”toexplainthebehaviorofourbasefunctions,e.g.,(consp(consxy))=tandx=y→(equalxy)=nil.Wealsoaddanencodingoftheordinalsuptoε0,takenfromManoliosandVroon[MV06],whichwewilluseforterminationproofsandtojustifyinduction.OurinductionruleisbasedonACL2’srule[KMM00,p.80],andisshowninFigure7.Wefinallydefineourproofcheckerinthelogicsowecanreasonaboutprovability.

12

¬A∨AA∨AAAB∨AA∨(B∨C)(A∨B)∨CA∨B¬A∨C

B∨CAA/σPropositionalschema

Contraction

Expansion

Associativity

Cut

Instantiation

Figure4:Propositionalrules

x=x

x1=y1→x2=y2→x1=x2→y1=y2

x1=y1→···→xn=yn→(fx1...xn)=(fy1...yn)((λ(x1...xn)β)t1...tn)=

β/[x1←t1,...,xn←tn]

ReflexivityaxiomEqualityaxiomFunctionalequality

schemaBetareduction

schema

Figure5:Equalityaxioms

13

(ifxyz)(equalxy)(conspx)(natpx)(symbolpx)(consxy)(carx)(cdrx)(Returnsyifxisnon-nil,zotherwiseChecksifxandyarethesameChecksifxisapairChecksifxisanaturalChecksifxisasymbol

Buildsthepair(x.y)

Accessesthefirstelementofanorderedpair∗Accessesthesecondelementofanorderedpair∗Checksifxislessthany†

Performsnatural-numberadditionofxandy†

Performsnatural-numbersubtractionofyfromx†

(symbol-∗†‡

afterinterpretingnon-pairargumentsas(nil.nil)afterinterpretingnon-naturalargumentsas0afterinterpretingnon-symbolicargumentsasnil

Figure6:Basefunctions

14

Inductionrule.

Wemayderiveaformula,F,from:•Aterm,m,calledthemeasure,•Asetofformulas,{q1,...,qk},

•Foreachformulaqi,asetofsubstitutionlists,

Σi={σi,1,σi,2,...,σi,hi},and

•Proofsofeachofthefollowingformulas:

–Basisstep

F∨q1∨···∨qk

–Inductivesteps

Foreach1≤i≤k,

F∨¬qi∨¬F/σi,1∨···∨¬F/σi,hi–Ordinalstep∗

(ordpm)=t

–Measuresteps†

Foreach1≤i≤kand1≤j≤hi,¬qi∨(ord∗†

ordpisourrecognizerforencodedordinalsordFigure7:Inductionrule

15

3.2Ourproofchecker

Wehavedevelopedadraftofourproofchecker,whichiscompleteexceptforthereflectionruleandefficientcomputation.WehaveportedourprogramtoseveralLispimplementations.OurproofcheckerissimilartoG¨odel’s[G¨od31,pp.163–171]Bwprogram,whichwasbasedon43auxiliarydefinitions,including:

•Basicoperationstoencoderecursivestructuresasprimepowers(1–10),•Constructorsforencodedformulas(13–16),

•Recognizersforencodedvariables,types,formulas,andsequencesofformulas(11,12,17–23),

•Variablebindingandsubstitutionoperations(25–33,37),and•Recognizersforvalidproofsteps(34–36,38–43).

Ourlogicismorecomplex,andourProofpprogramreliesuponaround100definitions.G¨odelencodedtermsasnumbersusingprimepowers.Ourencodingismorereadablesincewecanuselistsandsymbols.•Weencode’xas(quotex),

•Weencodethevariableforthesymbolvasv,

•Weencode(ft1...tn)as(f󰀂t1󰀁...󰀂tn󰀁),where󰀂ti󰀁representstheencodingofti,and

•Weencode((λ(x1...xn)β)t1...tn)as

((lambda(󰀂x1󰀁...󰀂xn󰀁)󰀂β󰀁)󰀂t1󰀁...󰀂tn󰀁).

Sincewedonotallowquotetobeusedasafunctionname,thereisnoconfusionastowhetheranencodedtermrepresentsaconstantorafunctioncall.Similarly,wedonotpermitpequal*,pnot*,orpor*tobeusedasfunctionnames,sowecanencodetheformulaswithoutoverlappingthetermsasfollows:

•Weencodet1=t2as(pequal*󰀂t1󰀁󰀂t2󰀁),

16

•Weencode¬Fas(pnot*󰀂F󰀁),and•WeencodeF∨Gas(por*󰀂F󰀁󰀂G󰀁).

Finally,weencodeproofsusingappeals.Eachappealrepresentsasinglestepintheproof,andisatupleoftheform:

(methodconclusion[subproofs][extras]),

where:

•Themethodisthenameoftheproofrulebeingused,•Theconclusionistheformulathissteppurportstoprove,

•Ifpresent,thesubproofsarealistofsubsidiaryappealswhichmustalsobecheckedbeforethisappealcanbeconsideredvalid(rulesofinferencehavesubproofs,whileaxiomsare“atomic”anddonot),and

•Ifpresent,theextrascontainanyadditionalinformationneededtojus-tifythisstep,e.g.,anappealtoinstantiationshouldspecifythesubsti-tutiontobeused.

Foreachruleofinference,weintroduceafunctiontocheckifanappealisavalidapplicationoftherule.Forexample,ourinstantiationruleallowsustoproveA/σfromaproofofA,sowewritethefunctionInstantiationOkp(x),whichchecksthat:

•Themethodisinstantiation,

•Thereisasinglesubproof,callitsconclusionA,•Theextrascontainasubstitutionlist,callitσ,and•TheconclusionisA/σ.

Finally,weintroduceProofStepOkp,whichchecksifasinglestepintheproofisvalidbyinspectingitsmethodandcallingtheappropriaterule-checker.WerecursivelyextendProofStepOkpacrosstheentireprooftoob-tainProofp,ourwhole-proofchecker.

17

3.3BuildingProofp-checkableproofs

ItisimpracticaltowriteProofp-checkableproofsbyhand.Forexample,evenourproofofx=y→z=x∨z=y,showninFigure8,takesafullpage.Accordingly,wehavedevelopedfunctionstoconstructproofsforus.Thesebuilderstypicallyusesomeinputproofs,formulas,ortermstocreateanewproofofacertainshape.WedonotneedtotrustthesebuilderssincewecanchecktheiroutputwithProofp.

Webeginwithsimplebuildersforourprimitiverules.Forexample,BuildPropSchemaconsestogetheraproofof¬A∨AgiventheformulaA,andBuildCutconsestogetheraproofofB∨CgivenproofsofA∨Band¬A∨C.Theseareusedtocreatenewbuildersthatactlikederivedrulesofinference,e.g.,“commutativityofor”isnotaprimitiverule,butwecanderiveB∨AfromaproofofA∨Basfollows:

1.A∨BGiven

2.¬A∨APropositionalschema3.B∨ACut

Wecantranslatethesestepsintoafunction,BuildCommuteOr,whichcreates

aproofofB∨Ausingaproof,x,ofA∨Basinput:

BuildCommuteOr(x:A∨B)=BuildCut(x,BuildPropSchema(A)).Wehavedevelopedmanybuilders,includingfunctionsformanipulatingpropositions,reasoningaboutlogicalequality,dealingwithlambdas,andhandlingthespecialequal,if,iff,andnotfunctions.Ourmostsophisti-catedbuildersperformlargetaskssuchasif-lifting,clausesplitting,evalua-tion,andrewriting.Thesetoolsallowustodescribetheproofswewishtoconstructmoreconcisely,buttheproofstheygeneratecanbecomelargeandcheckingthemcanbecomputationallyexpensive.

3.4ExtendingProofpwithanewrule

Wehaveverifiedanewproofchecker,Proof2p,whichextendsproofpbyadditionallyaccepting“commutativityofor”inferencesinonestep.SinceProofponlyneededtwostepstoachievethesameeffect,theaddedpowerofProof2poverProofpisnegligible.ButverifyingthisextensionrequiredustouseProofptoreasonaboutitselfanditsrelationshiptoProof2p,andshowswecanhandleallthe“generic”workinvolvedwithverifyingextensions.

18

(CUT(POR*(PEQUAL*XY)(POR*(PNOT*(PEQUAL*ZX))(PNOT*(PEQUAL*ZY))))

((ASSOCIATIVITY(POR*(POR*(PNOT*(PEQUAL*ZX))(PNOT*(PEQUAL*ZY)))(PEQUAL*XY))((CUT(POR*(PNOT*(PEQUAL*ZX))(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY)))

((CONTRACTION(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))(PNOT*(PEQUAL*ZX)))((CUT(POR*(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))(PNOT*(PEQUAL*ZX)))

(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))(PNOT*(PEQUAL*ZX))))

((CUT(POR*(PEQUAL*YY)

(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX))))

((ASSOCIATIVITY(POR*(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX)))

(PEQUAL*YY))

((EXPANSION(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(POR*(PNOT*(PEQUAL*ZX))(PEQUAL*YY)))

((EXPANSION(POR*(PNOT*(PEQUAL*ZX))(PEQUAL*YY))

((INSTANTIATION(PEQUAL*YY)

((AXIOM(PEQUAL*XX)))((X.Y)))))))))

(PROPOSITIONAL-SCHEMA(POR*(PNOT*(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX))))

(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX)))))))

(CUT(POR*(PNOT*(PEQUAL*YY))

(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX))))

((ASSOCIATIVITY(POR*(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX)))

(PNOT*(PEQUAL*YY)))

((CUT(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(POR*(PNOT*(PEQUAL*ZX))(PNOT*(PEQUAL*YY))))

((ASSOCIATIVITY(POR*(POR*(PNOT*(PEQUAL*ZX))(PNOT*(PEQUAL*YY)))

(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY)))

((INSTANTIATION(POR*(PNOT*(PEQUAL*ZX))

(POR*(PNOT*(PEQUAL*YY))

(POR*(PNOT*(PEQUAL*ZY))

(PEQUAL*XY))))

((AXIOM(POR*(PNOT*(PEQUAL*X1Y1))

(POR*(PNOT*(PEQUAL*X2Y2))

(POR*(PNOT*(PEQUAL*X1X2))

(PEQUAL*Y1Y2))))))

((X1.Z)(X2.Y)(Y1.X)(Y2.Y)))))

(PROPOSITIONAL-SCHEMA(POR*(PNOT*(POR*(PNOT*(PEQUAL*ZX))

(PNOT*(PEQUAL*YY))))

(POR*(PNOT*(PEQUAL*ZX))

(PNOT*(PEQUAL*YY)))))))))

(PROPOSITIONAL-SCHEMA(POR*(PNOT*(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX))))

(POR*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))

(PNOT*(PEQUAL*ZX)))))))))))

(PROPOSITIONAL-SCHEMA(POR*(PNOT*(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY)))

(POR*(PNOT*(PEQUAL*ZY))(PEQUAL*XY))))))))

(PROPOSITIONAL-SCHEMA(POR*(PNOT*(POR*(PNOT*(PEQUAL*ZX))(PNOT*(PEQUAL*ZY))))

(POR*(PNOT*(PEQUAL*ZX))(PNOT*(PEQUAL*ZY)))))))

Figure8:Proofp-checkableproofofx=y→z=x∨z=y

19

ThedefinitionofProof2pisstraightforward.Webeginbyintroducinganewfunction,CommuteOrOkp(x),whichacceptstheappealxonlyif:•Themethodiscommute-or,

•ThereisasinglesubgoalwhoseconclusionhastheformA∨B,and•TheconclusionisB∨A.

WethenintroduceProof2StepOkp,whichacceptstheappealsrecognizedbyCommuteOrOkpandProofStepOkp.WefinallyintroduceProof2p,whichrecursivelyensureseverystepinaproofisProof2StepOkp.

ToshowwecantrustProof2p,weneedtoshowitonlyacceptsproofsofformulasthatcouldbeprovenbyProofp.Thatis,wewanttoshow:

∀x:Proof2p(x)→Provablep(Conclusion(x)),

whereProvablep(φ)isdefinedas:

∃p:Proofp(p)∧Conclusion(p)=φ

Theinformalproofisstraightforward.AssumeProof2p(x)holds,andin-ductivelyassumeallthesubproofsofxconsistentirelyofProofp-levelsteps.Ifxisanotacommute-orstep,thenxisalreadyacceptedbyProofp.Oth-erwise,xmustbeacommute-orstep;assumeitconcludesB∨AfromitssubproofofA∨B,andapplyBuildCommuteOrtothissubprooftoobtainanentirelyProofp-levelproofofx’sconclusion.

Ourstrategyforverifyingotherextensionsissimilar:wewriteabuilderfunctionthatmimicsourextensionandcanbuildaproofofanyconclusiontheextensionmightmake.Wethenshowwheneverweusetheextensioninahigh-levelproof,ourbuildercouldhavebeenusedtocreateanequivalentlow-levelproof.Hence,theextensioncanonlybeusedtoacceptprovableformulas.

3.5Provingthenewruleissound

WehaveconstructedaProofp-checkableproofofoursoundnessclaimforProof2p.Thiswasparticularlychallengingsince,havingnoverifiedexten-sionstoworkwith,ourproofcoulduseonlytheprimitiveinferences.Ourproofeffortwascarriedoutinthreephases:

20

•Phase1.Wedevelopedacollectionofprooftools(e.g.,anevaluator,aclausesplitter,arewriter)asACL2functions,andweusedACL2to“informally”provethesetoolsaresound.

•Phase2.WeusedthesetoolstobuildaProofp-styleproofofthesoundnessofProof2p.Thiseffortinvolves“translating”theACL2-styleproofsfromPhase1intoProofp-checkableobjects.

•Phase3.WecheckedtheproofsfromPhase2withoursmallcommandloopprogram.ThisprogramisindependentofACL2andcanruninmanyLispenvironments.

Phase1.WefirstfocusedoncreatingthetoolsweexpectedtoneedtoproveProof2pandotherextensionsaresound.Forexample,wedevelopedanevaluatorandarewriterwhichcanbuildProofp-checkableproofstojus-tifytheirclaims.Wecouldhavewrittenthesetoolsinanylanguage,butdevelopingtheminACL2hadtwoimportantadvantages.

First,itgaveusastraightforwardwaytoturnourtoolsintoextensionsofProofp.ThiswouldnotbeimportantifourgoalwereonlytoverifyProof2p,butweeventuallywanttodevelopausefultheoremproverwhichincludesfacilitieslikeevaluationandrewriting.WritingourtoolsinACL2,whichisalmostthesameasourlogic,willmakeiteasytointroducethesefunctionsintooursystem.IfwehadinsteadimplementedthesetoolsasCprogramsorPerlscripts,itwouldnotbenearlysostraightforwardtoreusetheminthisway.

Second,usingACL2allowedusto“informally”proveourtoolsaresound.Havingtheseproofsavailableallowedus,inPhase2,tofocusonrecreatingratherthandiscoveringproofs.Toeasethistranslationandlessenthenumberoftoolsweneededtoimplement,wedevelopedourACL2proofswithoutusingthemoresophisticatedfeaturesofACL2,andrestrictedourselvestorewritingwithlemmas,execution,destructorelimination,andinduction.OurACL2proofstyleislibrary-centric:wefocusoncreatingcollectionsofruleswhich,together,cangreatlysimplifythetermsweencounterduringproofs.LikeBevier[Bev87]wekeepourfunctiondefinitionsdisabled—thatis,thetheoremproveronlyattemptstousedefinitionswhenitisexplicitlytoldtodoso.ButunlikeBevier,wekeepourrewriterulesenabledandfocusonmakingthemworkwelltogether.Sometimesweareabletopredictusefulrulesasweintroducenewfunctions,whileothertimesweonlyrealizeweneedanewruleafterseeingafailedproofattempt.Becauseofthisapproach,our

21

ACL2proofofthesoundnessclaimforProof2poccursonlyincidentallyasonelemmaamongthousandsofotherrewriterules.

Phase2.TotranslatethesoundnessclaimforProof2pintoaProofp-styleproof,wefocusonrecreatingtheselemmalibraries.Todothis,wedevelopedatactic-styleinterfacetoourprooftoolsfromPhase1.Thisinterfacecanbedriveninteractively:wecanposenewconjectures,thenperformrewritingwithlemmas,casesplitting,destructorelimination,andsoforth.Wealsodevelopedanautotactical,whichautomaticallytriesusingthesedifferentapproachestomakeprogress.Asweproveeachlemma,ourrewriterbecomesmoreusefulbecauseitnowhasanotherruletouse.Intheend,wewereabletoconstructtheProofp-counterpartsoftheallthelemmasleadinguptoandincludingthesoundnessclaimforProof2p.

Whengeneratingproofs,wemadeuseofBoyerandHunt’s[BH06]mem-oizationandhash-consingextensionofACL2,whichgreatlyincreasedourproof-buildingspeedandmemoryefficiency.Whenwesavedproofstodisk,weusedastructure-sharingrepresentationwhererepeatedtermscanbenamedandreferredtolater.

Sometimesourproofsgrewtoolargetodealwith.Typicallythiscouldbeaddressedbychoosingmorecarefulproofstrategies,e.g.,controllingwhendefinitionsareexpandedtoavoidintroducingcaseexplosions,andbyintro-ducingintermediatelemmasasnecessary.Othertimes,ourproof-buildingtoolshadtobeimproved.Asthemostsevereexampleofthis,anearlydraftofourevaluationbuilderwaswrittenwithoutpayingattentiontoproofsizes,anditsproofoffib(2)=2wasover790millionconses;areviseddrafttookonly35,000consestobuildthesameproof.

Phase3.Finally,wecheckedthegeneratedproofstoensuretheywerevalid.WehaveimplementedasmallCommonLispprogramtorunourproofchecker.ThisprogramisisindependentfromACL2anddoesnotincludeanymemoizationcode.Itprocessesalistofinstructions,e.g.,“addthistheoremwhichisjustifiedbythisproof”and“admitthisfunctionwhoseterminationisguaranteedbythisproof.”Theproofsarecheckedinorder,onebyone.Ittook7.6hourstocheckallourlemmasusingOpenMCLastheLispenvironmentonourdevelopmentmachine(a2.2-GHzAMDOpteronsystemwith32GBofmemoryrunning64-bitLinux).Wethendouble-checkedtheproofsin4.1hoursusingCMUCLonadifferentmachine(a2.13-GHzIntelCore2processorwith4GBofmemoryrunning32-bitLinux).Forourthesis,wealsoplantocheckourproofsusingadditionalplatformstominimizeanychancethatacomputererrorhasinappropriatelycausedsomeprooftobe

22

accepted.

Howbigistheproofofthesoundnessclaim?Includingallthelemmasleadinguptoandincludingoursoundnessclaim,wehaveover200definitionsand2,000rewriteruleswhoseproofstakenearly2GBofdiskspace.Theseproofsaregeneratedbyabout6,000linesofcodewhichdriveourtacticinterface,andthisbuildprocesstakesabout50minutestocompletewhenrunninginparallelonourdevelopmentmachine(whichhas8cores).AmoredetailedbreakdownisshowninFigure9.

DirectorySourcelinesUtilities3,086Logic2,750Build389Demo132Total6,357DefsRulesBuildtime

698478.6m1311,17939.4m281146.6m64220m2342,18251mProofsize488MB1.4GB36MB57MB1.9GBStatisticsasofSVNRevision401,Aug2007.Linecountexcludescommentsandblanklines.Rulecountexcludestrivialdefinitionrules.Buildtimecomputedwithomake-j8onlhug-1.cs.utexas.eduusingACL23.2.1onOpenMCL;totaltimeisbetterthanthesumsinceaddedparallelismisavailablewhenbuildingmultipledirectories.

Figure9:Proofsizemetricsbydirectory

Whyissomuchworkneededforsuchatrivialextension?AsFigure9suggests,thevastmajorityofourproofeffortisnotrelatedtothisparticularextensionatall,butinsteadisspentlayingthegroundworkforreasoningaboutarithmetic,lists,maps,terms,formulas,substitution,andproofs(theutilitiesandlogicdirectories).

3.6Remainingwork

InSection2.6weproposeddevelopinganumberofextensions,manyofwhicharefarmorecomplicatedthanthecommutativityofor.ThemajorremainingchallengeistoshowtherestoftheseextensionsaresoundusingonlyProofpandalready-verifiedextensions.

WehavealreadyimplementedtheseextensionsinACL2,andhavecreatedACL2proofsshowingtheyaresound.Inotherwords,wehavecompletedPhase1fortheentireproject.WestillneedtotranslatetheseACL2proofsintotheproperProofp-checkable(orProof2p-checkable,etc.)form.Webelievethisshouldbepossible,asevidencedbyourabilitytoverifythe

23

commutativityoforextension.Thetoolswedevelopedtocompletethisverification,andthethousandsoflemmaswehaveprovenandcannowreuse,shouldgiveusausefulstartingpointforthiswork.Asweprogress,proofsizeshouldbecomelessofanissue,sinceintroducingnewproofmethodswillallowhigher-levelproofstobemorecompact.Nevertheless,wewilllikelyneedtofurtherimproveourprooftools,andwemayalsoneedtodevelopsomenewtactics.

Wealsoneedtoaddresstheissueofevaluation.Wewillneedtosetupanefficientevaluator(i.e.,acallofLisp’sevalfunction),fairlyearlyinthestackofextensionssothereflectivetransitionfromhigher-levelproofstoProofp-levelproofscanbedoneeffectively.Ideally,thiswouldbeourfirstextension,butproofsizeissuesmightforceustointroducesomeintermediateextensionsfirst.Ifthisprovesdifficult,analternateapproachwouldbetouseProof2pandlaterproofcheckersdirectly,insteadofextendingProofpwithareflectionrule.

4

4.1

Relatedwork

Currenttheoremprovers

Thereareseveralgeneral-purposeproofsystemsavailable,includingtheBoyer-MooreproversACL2[KM97]andNQTHM[BKM95];higher-orderlogicproverssuchasHOL4[GCM+05],HOLLight[Har96],Isabelle/HOL[NPW02],andPVS[ORSSC98];andconstructivetypetheoryproverssuchasCoq[BC04]andNuprl[TPG95].

OurlogicisaslightvariantoftheACL2logic[KM98],whichistheleastexpressiveamongthesesystems.Theothersystemsprovidequantifiersandhigher-orderfunctions,andusetypesystemstoavoidlogicalparadoxes.ThelogicsofNuprlandCoqareintuitionistic,thoughthisdoesnotseemtohavemuchimpactonhardwareandsoftwareverification.Despitetherestrictivenessofourlogic,manyformalverificationproblemscanstillbeexpressed.

IntheACL2system,proofsare“whateverthedefthmcommandaccepts.”Thisproofsearchisinfluencedbyadatabaseofimplicitrulesandalsobyexplicithints,andmayinvolverewriting,arithmeticreasoning,induction,BDDs,andothertechniques.TheseproofmethodsarehighlycomplexanddonotresembletherulesoftheACL2logic.Theprogramhasnotbeensub-24

jectedtoanyrigorous,formalanalysis,andsoundnessbugshaveoccasionallybeendiscoveredinofficialreleases(seeFigure4.1).Proofattemptscreatehuman-readablelogswhichexplainatahighlevelwhattheproverisdoing,butthesearenotsuitableforcheckingbyotherprograms.

HOLsystemshaveamoreexplicitnotionofproof.TheoremsinHOLareobjectsoftypethmandrepresentsequentsΓ󰀏twhereΓisasetofassumptionsandtisaconclusion.Thethmtypeisabstract,sotheonlywaytoconstructathmistouseprimitive,built-infunctionscorrespondingtoHOL’srulesofinference.Forexample,HOL’sreflexivityruleis:

∅󰀏t=tThecorrespondingfunction,REFL,takesaterm-typedargumenttasinputandproducesthethmwithnoassumptionsandconclusiont=t.Asanotherexample,HOL’srulefordischargingassumptionsis:

Γ󰀏t2

Γ−{t1}󰀏t1→t2

Inotherwords,ift2followsfromΓ,thent1→t2followsafterweremovet1fromΓ.Thecorrespondingfunction,DISCH,takest1andathmoftheformΓ󰀏t2asinputs,andproducesthethm,Γ−{t1}󰀏t1→t2.

Ifthetypesystemisimplementedcorrectly,theonlywaytocreateathmobjectistoinvokefunctionslikeREFLandDISCH.Asaresult,anythm-typeobjectmusthavebeencreatedentirelybyfollowingtherulesofinference.Consequently,theintermediatestepsofaproofneednotbestored,althoughsometimesproofrecordingschemeshavebeenaddedtoHOLsystems[Won95,BN00,OS06]tofacilitateprooftranslationorexternaldouble-checking.ThePVSsystem[ORS92]alsousesanabstracttypetorepresenttheo-rems,butprovidesmorepowerfulprimitivesthanHOLsystems,particularlyHOLLight[Har96].Forexample,rewritingwithlemmasisaprimitiveruleinPVS.GriffioenandHuisman[GH98]regardedPVSfavorably,butweresomewhatcriticalonthispoint:“thesedecisionproceduressometimescausesoundnessproblems...PVSstillseemstocontainalotofbugsandfrequentlynewbugsshowup.”

CoqandNuprlhaveanother,well-definednotionofproof.Certaintypesarecalledpropositions.Wheneverthetypeofanobjectxisaproposition,wesayxitselfisaproofofthatproposition.Noabstracttypeisused;instead

25

ACL2Release

October,1998(Version2.3)August,1999(2.4)June,2000(2.5)

November,2001(2.6)November,2002(2.7)

SoundnessBugsFixed

SubversiverecursionsImmediateforcemode

MetafunctionswithhypothesesLineararithmeticEvaluationinproofsFunctionalinstantiationBDDsGuards

TautologycheckingACL2arrays

ProofcheckercommandsDefiningpackagesTrackingaxioms

Typeprescriptionsinequivalences

Redundancyandsingle-threadedobjectsPackagenames

TrackingprogrammodeMacroexpansionLineararithmetic

ProgrammodeindefconstMetaruleswithlocaleventsProgrammodeinlocalLocaltableeventsPackagewitnesses

ForcinginlineararithmeticRedundancyandmeasuresUnknown/hiddenpackagesMetarules

RedefinitionandprogrammodeRawlispcodeintracing

March,2004(2.8)

October,2004(2.9)

August,2005(2.9.3)February,2006(2.9.4)June,2006(3.0)August,2006(3.0.1)December,2006(3.1)

April,2007(3.2)

Figure10:SomecorrectedACL2soundnessbugs

Source:ACL2releasenotes[KM07]

26

theproofrulesaredirectlyencodedintothetypesystemastypingrules.ThisistheCurry-Howardisomorphism:theproposition“PimpliesQ”canbeencodedasthearrowtypeoffunctionsfromPtoQ,i.e.,P→Q.

Likethethmapproach,thecorrectnessofthesesystemsdependsonarelativelysmallkernel.Thetypesystemneedstobecorrectlyimplemented,andthetypingrulesforpropositionsneedtocorrespondtothelogic.Sincewholeprooftermsarestored,thisispotentiallylessspace-efficientthantheabstractthmtypeapproach.InCoq,thisissomewhatalleviatedbyacomplexnotionoftermequalitywhereinreducibly-equivalenttermsaresaidtobeequal.Forexample,Coqcanprove2+3=5withasingleuseofitsreflexivityrule.

Inmostsystems,proofsareconstructedwithfully-expansive,goal-directedscriptscalledtactics.Ifatacticattemptstobuildatheoremwithaninvalidinference,anerrorwillbecausedandtheproofattemptwillfail.Tacticscanoftenbecombinedintostrategiesortacticals,whichcanrespondtofailurebytryingothertactics,etc.Tacticsneednotbetrustedandcanbewrittenbytheuser(whereastrustedcodemustbewrittenbythetheoremprover’sauthors)sincealltheirworkwillbecheckedbythethmconstructors.Eventhoughoursystemdoesnotuseanabstractthmtype,wecanemulatetacticsbyhavingthemconstructproofsinsteadofthms,andcheckingtheseproofswithProofp.

TheACL2systemdoesnothaveanexplicitnotionofproof,anditsversionoftacticsandtacticals,proofcheckermacros,arerarelyused.Instead,thebuilt-inrewriteriscontrolledbyaddinglemmas.Indirectadviceabouthowtousetheselemmascanalsobeadded,makingtheapproachsomewhatflexibleandautomatic:theuserfocusesonsettinguprulesthatwillworkwelltogether,andthesystemappliesthisstrategytonewproblems.Whenthedefaultstrategyisinsufficienttoproveatroublesomeconjecture,extrahintscanbegivenbytheuserorautomaticallysuggestedbyuser-developedheuristics(see,e.g.,[Dav04]).

Nothingpreventsatactic-basedsystemfromfollowingtheheuristicrewrit-ingapproach.Boulton[Bou92]hasimplementedtacticstoemulatesomeofNQTHM’sautomationinHOL,andlemma-basedsimplificationisavailableinmostprovers,e.g.,autorewriteinCoq,therewritepackageinNuprl,rewritetacinHOL4,andthesimptacticinIsabelle/HOL.Indeed,inoursystemwehaveprimarilyusedafewtacticsthatemulatesomeofACL2’sautomation.

27

4.2Embeddedproofcheckers

General-purposetheoremproversareexpressiveenoughthatnewproof-checkingprogramscanbeexpressedintheirlogics.Infact,thecurrentdraftofoursystemcanbeunderstoodasaproofcheckerwritteninsideACL2.Thishasbeendonemanytimesinvariousprojects.

Inasomewhatuniqueeffort,Shankar[Sha94]wroteaproofcheckerinNQTHMforShoenfield’sfirst-orderlogicwithCohen’sZ2axiomsinordertoproveG¨odel’sincompletenesstheorem.Hisgoalwastomechanicallycheckclassicmetamathematicaltheorems,andhedidnotintendtoproduceanewtheoremproverforeverydayuse.HeusedNQTHMtointroduceextensionsliketautologychecking,butdidnottryto“bootstrap”theseproofsintoaformhisproofcheckercouldself-check.

Morecommonly,thisapproachhasbeenusedtostudypropertiesofsimpleproofcheckingprograms.Forexample:

•J.vonWright[vW94a,vW94b]wroteaproofcheckerforhigher-orderlogicinHOL.ThisinvolveddefiningaHOLspecification,Isproof,whichdescribesthevalidproofs.Aprimitive,imperativeprogramminglanguagewasthendefinedwithinHOL,andaproofcheckingprogramwaswritteninthislanguage.HOLwasusedtoshowtheimperativeprogramimplementedthehigh-levelIsproofspecification.

•RidgeandMargetson[RM05]wroteafirstordertheoremproverasdef-initionsinIsabelle/HOLand,usingIsabelle/HOL,provedtheprogramtobesoundandcomplete.Theprogramdoessomeproofsearch,buttheymentionitsperformanceisnotcompetitivewithtypicalresolutionprovers.

•Harrison[Har06]hasmimickedtheimplementationofHOLLight,anOCamlprogram,asaHOLLightspecification.Byassuminganaddi-tionalaxiomaboutsets,hecanshowtheencodedHOLsystemiscon-sistent.Withouttheaxiom,hecanshowtheencodedsystemexceptfortheaxiomofinfinityisconsistent.Theseresultsindicate“somethingclosetotheactualimplementationofHOL”issound.

Ineachoftheseefforts,anexistingproveristrustedandisusedtoprovepropertiesaboutanewproofcheckingcore.Ourprojectiscomplementary:

28

wearewillingtotrustoursmallcore,andourinterestisintheverifica-tionofnew,extendedproofmethods.Wedonotproposetoinvestigatethesoundnessofourcoremechanically.

4.3Independentproofchecking

Therehavealsobeensomeprojectswhereonesystemisusedtochecktheworkofanother.ThisideaissomewhatlikeBoulton’ssuggestion[Bou93]ofseparatingproofsearchfromproofconstructioninHOL,butmayalsobeusefulfor“porting”resultsobtainedinonesystemtoanother.Afewsuchprojectsinclude:

•McCuneandShumsky[MS00]havewrittenACL2functionstocheckproofobjectsemittedbyOtter,aresolutionprover,forvalidity.ThemajorityoftheproofsearchcanbeoffloadedontoOtter,andtheACL2programonlychecksthatOtterdidnotmakeamistake.Noattemptismadetoverifytheresolutionprover,whichisanoptimizedCprogram,butsincetheACL2programcheckstheprooftranscript,ACL2canbeusedtoshowthecombinedsystemissound.

•CaldwellandCowles[CC02]describepreliminaryworkonindepen-dentlycheckingNuprlproofswithaprogramwritteninACL2.Astheyemphasize,“wearenotmakingclaimsaboutthecorrectnessofNuprlitself,”whichwasseenasimpracticallyhard:Nuprl’simplemen-tationapparentlyinvolvesa60,000-lineLispcoreanda40,000-lineMLinterface,with167rulesofinferencewhicharesometimescomplicated,e.g.,thearithrule.Theprojectisapparentlystillintheearlystages.•ObuaandSkalberg[OS06]haveextendedHOLLightwithaproofrecorderthattrackscallstotheproofconstructors.Acomplexstructure-sharingschemeisusedinordertocombatthesizeofproofobjects,andmanyproofscanbereadintoIsabelle/HOLandcheckedindependentlyfromHOLLight.Theauthorsspeculatethatadding“higherinfer-encerules,”suchasrewriting,mighthelptomaketheemittedproofssmaller,buthavenotapparentlytriedtoimplementsuchascheme.Ourprojecttakesadifferentapproach.Ratherthancheckingsomeun-verifiedproofmethoddidnotmakeamistakeafteritseveryuse,wewanttoverifyproofmethodssoweneednotchecktheirwork.

29

4.4Metareasoning

Oursystemwillhaveanintegratedproofcheckerdefinedinitsownlogicsowecandirectlyreasonaboutprovability.Thisallowsustoshownewprooftechniquesaresoundandcanbetrusted.

Evenwithoutanintegratedproofchecker,othertheoremprovershavesomesupportformetareasoning.Mostofthisworkfollows,withminordifferences,themetafunctionapproach[BM81],whichinvolvesfivesteps:1.Anencodingfortherelevanttermsisintroduced,

2.Asemanticfunction,meaning(term,env),isintroducedtoevaluateanencodedtermwithrespecttosomeassignmentofvariables,3.A“metafunction”,fn(term),isintroducedtosimplifyencodedterms,4.Theuserprovesmeaning(fn(term),env)=meaning(term,env),forallwell-formedencodedtermsandforallenvironments,todemonstratefncanbetrusted,and5.Someevaluationmechanismallowsfntobeusedtosimplifyencodedtermsinproofs.InACL2,astandardencoding(quoting)canbeused,andmeaningfunc-tionsforafixedsetofconceptscanbeintroducedusingthedefevaluatorfacility.Ametafunction,fn,isaregularACL2program,writtenasarecur-sivefunctionthatmanipulatesencodedterms.Abuilt-inmechanismallowsthesystemtobeginusingametafunctionafterthesoundnesstheoremisproven.

MetafunctionscanbeausefultoolforadvancedACL2users,buttheyhavelimitations.Theyaresubservienttotherewriterandcannotkeepstatebetweeninvocations,i.e.,forbuildingupdatabasesoffacts[SNG+04].Also,sincetheACL2simplifierisnotafunctionintheACL2logic,metafunctionscanonlycalluponitheuristically[HKK+05].Thatis,evenifACL2canrewritetermtoterm’,wecannotassumeterm=term󰀁whenwetrytoprovethesoundnesstheorem.

ACL2’sproofsearchiscontrolledbyalargeamountofunverifiedcode,anditisdifficulttoimagine“lifting”anysubstantialpartofthisintometa-functions.Manyfeatures,suchaslineararithmetic,aredeeplyintegratedintotherewriter[BM88],keepstateacrossinvocations,ordonotfitintothe

30

metafunctionparadigmofreplacingonetermwithanequalone(e.g.,gen-eralization).Wewouldalsofaceabootstrappingproblem:evenifwecouldcleanlyextractaprooftechniqueliketypereasoningintoametafunction,couldweprovethesoundnesstheoremwithoutusingtypereasoning?Wedonotseemuchhopeofmovinginthisdirection.

MetatheoreticextensibilityisachallengeforHOLsystems,wheretoaddanewproofprocedure“wemustsomehowripopenanabstracttype,tinkerwithittoaddanewconstructor,andthencloseitupagain.”[Har95]

Slind[Sli92]proposedaschemeforallowingmkthm,an“arbitrary”thmconstructorthatdoesnotcorrespondtoanyruleofinference,tobeusedunderrestrictedcircumstances.First,thesemanticsofMLwouldbefor-malizedinHOL,aswouldtheHOLimplementation.Then,mkthmtistobepermittedonlyifwecanprovethereissomefunctionfthatproducesausual,fully-expansiveHOLproofoft.Thisideawasneverimplemented.3

MorerecentlyChaiebandNipkow[CN05]havewrittenandverifiedaquantifier-eliminationprocedureforPresburgerarithmeticinIsabelle/HOL.TheyencodePresburgerformulaswithanewtype,anddefinetheirownmeaningfunctiontomapencodedformulasintoBooleans(theformulasofHOL).Ametafunction-likeeliminationprocedureisimplementedinasubsetofHOLwhichcanbecompiledtoMLusingaHOLcompiler[BN02].Finally,anew,experimentalruleofinferenceisaddedtothesystemsoexecutionsoftheMLprogramareallowedtobetreatedasproofsofequality.Thissystemisapparently200timesfasterforsolvingPresburgerformulasthananequivalent,tactic-basedsolution.ThistechniqueavoidstheburdenofformalizinganMLsystemandaHOLimplementationasSlindproposed,butthecodeforconstructingthmobjectsremainsseparatedfromthelogic,andasaresultwestillcannotreasonaboutthmconstructionandtheprovabilityofformulas.

MetafunctionsarealsosupportedinCoq.Gr´egoireandMahboubi[GM05]haveintroducedaprocedureforreasoningaboutequalitybetweenpolyno-mialsincommutativerings.Theydefineanewtypetorepresentencodedpolynomialsoveraringandprovideameaningfunctionasabove.Theyshowametafunction-likecanonicalizationroutinepreservesthemeaningofencodedterms,andtheirprocedurecanthenbeusedinproofsviaCoq’sevaluation/reductionfacilities.AsinChaiebandNipkow’swork,nomethodisavailableforreasoningabouttherulesofinferenceandprovabilityoffor-3

CorrespondencewithKonradSlind,August2006.

31

mulasingeneral.

WearenotawareofanysupportformetareasoninginPVS.

KnoblockandConstable[KC86]proposedtwostrategiesforaddingmetar-easoningtoNuprl.Oneapproachinvolvedahierarchyoflanguages,whereeachPRLn+1wouldincludeanencodingofthePRLnproofs.Intheother,astackoflanguageswouldnotbeneeded,andinsteadpartofPRL1wouldbedirectlyencodedintoPRL0.Theseideaswereneverimplemented.4

4

CorrespondancewithRobertConstable,August2006.

32

References

[Avi95]

[Bar01][BC04]

[Bev87][BH06]

[BKM95]

[BKM96]

[BM81]

[BM88]

AlgirdasA.Avi˘zienis.Themethodologyofn–versionprogramming.InM.R.Lyu,editor,SoftwareFaultTolerance,pages23–46.Wiley,1995.

EliBarzilay.QuotationandreflectioninNuprlandScheme.TechnicalReport2001-1832,CornellUniversity,2001.YvesBertotandPierreCast´eran.InteractiveTheoremProvingandProgramDevelopment:Coq’Art:TheCalculusofInductiveConstructions.TextsinTheoreticalComputerScience.Springer-Verlag,2004.

WilliamR.Bevier.AVerifiedOperatingSystemKernel.PhDthesis,UniversityofTexasatAustin,December1987.RobertS.BoyerandWarrenA.Hunt,Jr.Function

memoizationanduniqueobjectrepresentationforACL2functions.InACL2’06,August2006.

RobertS.Boyer,MattKaufmann,andJStrotherMoore.TheBoyer-Mooretheoremproveranditsinteractiveenhancement.ComputersandMathematicswithApplications,29(2):27–62,1995.

BishopBrock,MattKaufmann,andJMoore.ACL2

theoremsaboutcommercialmicroprocessors.InM.SrivasandA.Camilleri,editors,FormalMethodsin

Computer-AidedDesign(FMCAD’96),volume1166ofLNCS,pages275–293.Springer-Verlag,1996.

R.S.BoyerandJStrotherMoore.Metafunctions:provingthemcorrectandusingthemefficientlyasnewproof

proceedures.InR.S.BoyerandJStrotherMoore,editors,TheCorrectnessProbleminComputerScience,pages103–184.AcademicPress,1981.

R.S.BoyerandJS.Moore.Integratingdecisionproceduresintoheuristictheoremprovers:Acasestudyoflinear

33

[BM96]

[BN00]

[BN02]

[Bou92]

[Bou93]

[BT00]

[CC02]

[CN05]

arithmetic.InMachineIntelligence11,pages83–124.OxfordUniversityPress,1988.

BobBoyerandJMoore.Mechanizedformalreasoningaboutprogramsandcomputingmachines.InR.Veroff,editor,AutomatedReasoninganditsApplications,EssaysinHonorofLarryWos.MITPress,1996.

StefanBerghoferandTobiasNipkow.Prooftermsforsimplytypedhigherorderlogic.InJ.HarrisonandM.Aagaard,editors,TheoremProvinginHigherOrderLogics(TPHOLS’00),volume1869ofLNCS,pages38–52.Springer-Verlag,2000.

StefanBerghoferandTobiasNipkow.Executinghigherorderlogic.InTypesforProofsandPrograms(Types’00),volume2277ofLNCS,pages24–40.Springer-Verlag,2002.RichardJ.Boulton.Boyer-MooreautomationfortheHOLsystem.InL.J.M.ClaesenandM.J.C.Gordon,editors,HigherOrderLogicTheoremProvinganditsApplications(TPHOLS’92),volumeA-20ofIFIPTransactions,pages133–142.ElsevierSciencePublisher,September1992.RichardJohnBoulton.EfficiencyinaFully-ExpansiveTheoremProver.PhDthesis,UniversityofCambridge,December1993.

PiergiorgioBertoliandPaoloTraverso.Designverificationofasafety-criticalembeddedverifier.InComputer-AidedReasoning:ACL2CaseStudies,chapter14.KluwerAcademicPublishers,2000.

JamesL.CaldwellandJohnCowles.RepresentingNuprlproofobjectsinACL2:TowardaproofcheckerforNuprl.InDominiqueBorrione,MattKaufmann,andJMoore,editors,ACL2’02,April2002.

AmineChaiebandTobiasNipkow.VerifyingandreflectingquantifiereliminationforPresburgerarithmetic.InLogic

34

[Dav04]

[Dij82]

[DLP77]

[Fef86][Fet88]

[GCM+05]

[GH98]

[GM05]

Programming,ArtificialIntelligence,andReasoning(LPAR’05),volume3835ofLNCS,pages367–380.Springer-Verlag,2005.

JaredDavis.Finitesettheorybasedonfullyorderedlists.InMattKaufmannandJMoore,editors,ACL2’04,November2004.

EdsgerW.Dijkstra.OnthefactthattheAtlanticOceanhastwosides.InSelectedwritingsoncomputing:apersonalperspective,pages268–176.Springer-Verlag,1982.RichardA.DeMillo,RichardJ.Lipton,andAlanJ.Perlis.Socialprocessesandproofsoftheoremsandprograms.InPrinciplesofProgrammingLanguages(POPL’77),pages206–214.ACMPress,1977.

SolomonFeferman,editor.KurtG¨odel:CollectedWorks,volume1.OxfordUniversityPress,1986.

JamesH.Fetzer.Programverification:Theveryidea.CommunicationsoftheACM,31(9):1048–1063,September1988.

MikeGordon,AvraCohn,TomMelham,KonradSlind,MichaelNorrish,andetal.TheHOLsystem:Tutorial,September2005.ForHOLKananaskis-3.

DavidGriffioenandMariekeHuisman.AcomparisonofPVSandIsabelle/HOL.InJimGundyandMalcomNewey,editors,TheoremProvinginHigherOrderLogics(TPHOLS’98),volume1479ofLNCS,pages123–142.Springer-Verlag,September1998.

BenjaminGr´egoireandAssiaMahboubi.ProvingequalitiesinacommutativeringdonerightinCoq.InJ.HurdandT.Melham,editors,TheoremProvinginHigherOrder

Logics(TPHOLS’05),volume3603ofLNCS,pages98–113.Springer-Verlag,2005.

35

[G¨od31]

[Goe00]

[GWH00]

[Har95]

[Har96]

[Har06]

[HKK+05]

[Hoa69]

KurtG¨odel.Uber¨formalunentscheidbares¨atzeder

PrincipiaMathematicaundverwandtersystemeI.Monatsheftef¨urmathematikundphysik,38:173–198,1931.Englishtranslationin[Fef86],pages145–195:OnformallyundecidablepropositionsofPrincipiaMathematicaandrelatedsystemsI.

WolfgangGoerigk.Compilerverificationrevisited.InComputer-AidedReasoning:ACL2CaseStudies,chapter15.KluwerAcademicPublishers,2000.DavidGreve,MatthewWilding,andDavidHardin.High-speed,analyzablesimulators.InComputer-AidedReasoning:ACL2CaseStudies,chapter8.KluwerAcademicPublishers,2000.

JohnHarrison.Metatheoryandreflectionintheorem

proving:Asurveyandcritique.TechnicalReportCRC-053,SRICambridge,MillersYard,Cambridge,UK,1995.JohnHarrison.HOLlight:Atutorialintroduction.InM.SrivasandA.Camilleri,editors,FormalMethodsinComputer-AidedDesign(FMCAD’96),volume1166ofLNCS,pages265–269.Springer-Verlag,1996.

JohnHarrison.Towardsself-verificationofhollight.InUlrichFurbachandNatarajanShankar,editors,

InternationalJointConferenceonAutomatedReasoning(IJCAR’06),volume4130ofLNAI,pages177–191.Springer-Verlag,August2006.

WarrenA.Hunt,Jr.,MattKaufmann,RobertBellarmineKrug,JMoore,andEricWhitmanSmith.MetareasoninginACL2.InJ.HurdandT.Melham,editors,TheoremProvinginHigherOrderLogics(TPHOLS’05),volume3603ofLNCS,pages163–178.Springer-Verlag,2005.C.A.R.Hoare.Anaxiomaticbasisforcomputerprogramming.CommunicationsoftheACM,12(10):576–583,October1969.

36

[How88]

[HR05]

[HR06]

[Hun00]

[KC86]

[KM94][KM97]

[KM98][KM07]

DouglasJ.Howe.ComputationalmetatheoryinNuprl.InE.LuskandR.Overbeek,editors,Conferenceon

AutomatedDeduction(CADE’88),LNCS,pages238–257.Springer-Verlag,March1988.

WarrenA.Hunt,Jr.andErikReeber.FormalizationoftheDE2language.InCorrectHardwareDesignandVerificationMethods(CHARME’05),volume3725ofLNCS,pages20–34.Springer-Verlag,2005.

WarrenA.Hunt,Jr.andErikReeber.ApplicationsoftheDE2language.InMarySheeranandTomMelham,editors,DesigningCorrectCircuits(DCC’06).ETAPS’06,March2006.

WarrenHunt,Jr.TheDElanguage.InComputer-AidedReasoning:ACL2CaseStudies,chapter10.KluwerAcademicPublishers,2000.

ToddB.KnoblockandRobertL.Constable.Formalizedmetareasoningintypetheory.InLogicinComputerScience(LICS’86),pages237–248.IEEEComputerSociety,June1986.

MattKaufmannandJMoore.DesigngoalsofACL2.TechnicalReport101,ComputationalLogic,Inc.,1994.MattKaufmannandJStrotherMoore.Anindustrial

strengththeoremproverforalogicbasedonCommonLisp.IEEETransactionsonSoftwareEngineering,23(4):203–213,April1997.

MattKaufmannandJStrotherMoore.AprecisedescriptionoftheACL2logic,April1998.

MattKaufmannandJMoore.TheACL2user’smanual,2007.Version3.2.Availableonline:

http://www.cs.utexas.edu/users/moore/acl2/v3-2/acl2-doc-index.html.

37

[KMM00]

[LM03]

[LM04]

[LP99]

[Mac01][McC60]

[Moo98]

[MS00]

[MV06]

MattKaufmann,PanagiotisManolios,andJStrother

Moore.Computer-AidedReasoning:AnApproach.KluwerAcademicPublishers,June2000.

HanbingLiuandJStrotherMoore.ExecutableJVMmodelforanalyticalreasoning:Astudy.InInterpreters,VirtualMachinesandEmulators(IVME’03),pages15–23,2003.HanbingLiuandJStrotherMoore.JavaprogramverificationviaaJVMdeepembeddinginACL2.InKonradSlind,AnnetteBunker,andGanesh

Gopalakrishnan,editors,TheoremProvinginHigherOrderLogics(TPHOLS’04),pages184–200,2004.

LeslieLamportandLawrenceC.Paulson.Shouldyourspecificationlanguagebetyped?ACMTransactionsonProgrammingLanguagesandSystems(TOPLAS’99),21(3):502–526,May1999.

DonaldMacKenzie.MechanizingProof:Computing,Risk,andTrust.TheMITPress,October2001.

JohnMcCarthy.Recursivefunctionsofsymbolic

expressionsandtheircomputationbymachine,part1.CommunicationsoftheACM,3(4):184–195,April1960.JMoore.Symbolicsimulation:AnACL2approach.In

G.GopalakrishnanandP.Windley,editors,FormalMethodsinComputer-AidedDesign(FMCAD’98),volume1522ofLNCS,pages334–350.Springer-Verlag,November1998.WilliamMcCuneandOlgaShumsky.Ivy:Apreprocessorandproofcheckerforfirst-orderlogic.InComputer-AidedReasoning:ACL2CaseStudies,chapter16.KluwerAcademicPublishers,2000.

PanagiotisManoliosandDaronVroon.Ordinalarithmetic:Algorithmsandmechanization.JournalofAutomatedReasoning,pages1–37,2006.

38

[MZ05]

[NPW02]

[ORS92]

[ORSSC98]

[OS06]

[RF00]

[RM05]

JStrotherMooreandQiangZhang.Proofpearl:Dijkstra’sshortestpathalgorithmverifiedwithACL2.InJ.HurdandT.Melham,editors,TheoremProvinginHigherOrderLogics(TPHOLS’05),volume3603ofLNCS,pages373–384.Springer-Verlag,2005.

TobiasNipkow,LawrenceC.Paulson,andMarkusWenzel.Isabelle/HOL—AProofAssistantforHigher-OrderLogic,volume2283ofLNCS.Springer,2002.

S.Owre,J.M.Rushby,andN.Shankar.PVS:Aprototypeverificationsystem.InDeepakKapur,editor,ConferenceonAutomatedDeduction(CADE),volume607ofLectureNotesinArtificialIntelligence,pages748–752.Springer-Verlag,June1992.

S.Owre,J.M.Rushby,N.Shankar,andD.W.J.

Stringer-Calvert.PVS:Anexperiencereport.InDieterHutter,WernerStephan,PaoloTraverso,andMarkusUllman,editors,AppliedFormalMethods–FM-Trends98,volume1641ofLNCS,pages338–345.Springer-Verlag,October1998.

StevenObuaandSebastianSkalberg.ImportingHOLintoIsabelle/HOL.InUlrichFurbachandNatarajanShankar,editors,InternationalJointConferenceonAutomatedReasoning(IJCAR’06),volume4130ofLNAI,pages298–302.Springer-Verlag,August2006.

DavidM.RussinoffandArthurFlatau.RTLverification:Afloating-pointmultiplier.InComputer-AidedReasoning:ACL2CaseStudies,chapter13.KluwerAcademicPublishers,2000.

TomRidgeandJamesMargetson.Amechanicallyverified,soundandcompletetheoremproverforfirstorderlogic.InJ.HurdandT.Melham,editors,TheoremProvingin

HigherOrderLogics(TPHOLS’05),volume3603ofLNCS,pages294–309.Springer-Verlag,2005.

39

[RMT03]

SandipRay,JohnMatthews,andMarkTuttle.CertifyingcompositionalmodelcheckingalgorithmsinACL2.InACL2’03,July2003.

[RRAHMM04]J.-L.Ruiz-Reina,J.-A.Alonso,M.-J.Hidalgo,andF.-J.

[Rus98]

[Saw00]

[Sha94][Sho67][Sli92]

[SNG+04]

[TB03]

Mart´ın-Mateos.Aformallyverifiedquadraticunificationalgorithm.InMattKaufmannandJMoore,editors,ACL2’04,November2004.DavidM.Russinoff.AmechanicallycheckedproofofIEEEcomplianceofaregister-transfer-levelspecificationoftheAMD-K7floating-pointmultiplication,division,andsquarerootinstructions.LMSJournalofComputationandMathematics,1:147–200,December1998.

JunSawada.Verificationofasimplepipelinedmachinemodel.InComputer-AidedReasoning:ACL2CaseStudies,chapter9.KluwerAcademicPublishers,2000.N.Shankar.Metamathematics,Machines,andG¨odel’sProof.CambridgeUniversityPress,1994.

JosephR.Shoenfield.MathematicalLogic.TheAssociationforSymbolicLogic,1967.

KonradSlind.AddingnewrulestoanLCF-stylelogicimplementation:Preliminaryreport.InL.J.M.ClaesanandM.J.C.Gordon,editors,HigherOrderLogicTheoremProvinganditsApplications(TPHOLS’92),volumeA-20ofIFIPTransactions.ElsevierSciencePublisher,September1992.

EricSmith,SeritaNelesen,DavidGreve,MatthewWilding,andRaymondRichards.AnACL2libraryforbags.InMattKaufmannandJMoore,editors,ACL2’04,November2004.DianaTomaandDominiqueBorrione.SHAformalization.InACL2’03,July2003.

40

[TPG95]

[vW94a][vW94b]

[Won95]

CornellUniversityThePRLGroup.Implementing

mathematicswiththeNuprlproofdevelopmentsystem,October1995.

J.vonWright.Theformalverificationofaproofchecker,1994.SRIInternalReport.

J.vonWright.Representinghigher-orderlogicproofsinHOL.InThomasF.MelhamandJuanitoCamilleri,editors,HigherOrderLogicTheoremProvingandItsApplications(TPHOLS’94),volume859ofLNCS.Springer-Verlag,September1994.

WaiWong.RecordingandcheckingHOLproofs.InE.ThomasSchubert,PhillipJ.Windley,andJim

Alves-Foss,editors,HigherOrderLogicTheoremProvinganditsApplications(TPHOLS’95),volume971ofLNCS,pages353–368.Springer-Verlag,September1995.

41