An abductive event calculus planner

1AnAbductiveEventCalculusPlannerMurrayShanahanDepartmentofElectricalandElectronicEngineering,ImperialCollege,ExhibitionRoad,LondonSW72BT,[e-mail]1998RevisedApril19992ndrevisionSeptember1999AbstractIn1969CordellGreenpresentedhisseminaldescriptionofplanningastheoremprovingwiththesituationcalculus.ThemostpleasingfeatureofGreen'saccountwasthenegligiblegapbetweenhigh-levellogicalspecificationandpracticalimplementation.Thispaperattemptstoreinstatetheidealofplanningviatheoremprovinginamodernguise.Inparticular,thepapershowsthatifweadopttheeventcalculusasourlogicalformalismandemployabductivelogicprogrammingasourtheoremprovingtechnique,thenthecomputationperformedmirrorscloselythatofahand-codedpartial-orderplanningalgorithm.Soundnessandcompletenessresultsforthislogicprogrammingimplementationaregiven.Finallythepapershowsthat,ifweextendtheeventcalculusinanaturalwaytoaccommodatecompoundactions,thenusingthesameabductivetheoremprovingtechniqueswecanobtainahierarchicalplanner.IntroductionIn1969,Greenofferedalogicalcharacterisationofplanningcouchedintermsofthesituationcalculus,inadditiontoanimplementationbasedonaresolutiontheoremprover[Green,1969].WhatmakesGreen’streatmentsoattractiveistheclosecorrespondencebetweenimplementationandspecification.Theverysameaxiomsthatfeatureintheformaldescriptionoftheplanningtaskformthebasisoftherepresentationdeployedbytheimplementedplanner,andeachcomputationstepperformedbytheplannerisastepintheconstructionofaproofthatasuitableplanexists.However,Green’sseminalwork,thoughmuchadmired,hashadlittleimpactonsubsequentworkinplanning,owingtothewidespreadbeliefthatatheoremprovercannotformthebasisofapracticalplanningsystem.Thefollowingquotefrom[Russell&Norvig,1995]exemplifiesthewidelyheldbeliefthatplanningviatheoremprovingisimpractical.Unfortunatelyagoodtheoreticalsolutiondoesnotguaranteeagoodpracticalsolution....Tomakeplanningpracticalweneedtodotwothings:(1)Restrictthelanguagewithwhichwedefineproblems....(2)Useaspecialpurposealgorithm...ratherthanageneral-purposetheoremprovertosearchforasolution.Thetwogohandinhand:everytimewedefineanewproblem-descriptionlanguage,weneedanewplanningalgorithmtoprocessthelanguage....Theideaisthatthealgorithmcanbedesignedtoprocesstherestrictedlanguagemoreefficientlythanaresolutiontheoremprover.[Russell&Norvig,1995,page342]2Theaimofthepresentpaperistodemonstratethatagoodtheoreticalsolutioncanindeedco-existwithagoodpracticalsolution,throughtheprovisionofalogicalaccountofpartial-orderandhierarchicalplanninginthespiritofGreen’swork.However,whereGreen’saccountwasbasedontheformalismofthesituationcalculus,thepresentpaperadoptstheeventcalculus[Kowalski&Sergot,1986],[Shanahan,1997a].Furthermore,whileGreenregardedplanningasadeductiveprocess,planningwiththeeventcalculusismostnaturallyconsideredasanabductiveprocess.Wheneventcalculusformulaearesubmittedtoasuitablytailoredresolutionbasedabductivetheoremprover,theresultisasoundandcompletepurelylogicalplanningsystemwhosecomputationsmirrorcloselythoseofahand-codedplanningalgorithm.Thepaperisorganisedasfollows.Section1presentstheeventcalculususingfullfirst-orderpredicatecalculuswithcircumscription.Section2presentsalogicaldefinitionofeventcalculusplanning.Section3describesanumberoftechniquesforrenderingthisspecificationintoalogicprogrammingimplementationviaanabductivemeta-interpreter,anddrawsattentiontothecorrespondencestoexistingpartial-orderplanningalgorithms.Section4offerssoundnessandcompletenessresultsforasimpleversionoftheplanner.Section5showshowtheprecedingmaterialcanbeextendedtocoverhierarchicalplanning.FinallySection7addressesefficiencyissuesandpresentssomebenchmarkresults.Ashorterversionofthispaperwaspresentedin[Shanahan,1997b].1ACircumscriptiveEventCalculusTheformalismforreasoningaboutactionusedinthispaperisderivedoriginallyfromKowalskiandSergot’seventcalculus[Kowalski&Sergot,1986],butisbasedonmany-sortedfirst-orderpredicatecalculusaugmentedwithcircumscription[Shanahan,1997a].Thissectionpresentsthebareoutlinesoftheformalism.1Anexampleoftheuseoftheformalism,whichshouldmakethingsclearertothoseunfamiliarwithit,appearsinthenextsection.Foramorethoroughtreatment,consult[Shanahan,1997a].Table1presentstheessentialsofthelanguageofthecalculus,whichincludessortsforfluents,actions(events),andtimepoints.Wehavethefollowingaxioms,whoseconjunctionisdenotedEC.2HoldsAt(f,t)←InitiallyP(f)∧¬Clipped(0,f,t)(EC1)HoldsAt(f,t3)←(EC2)Happens(a,t1,t2)∧Initiates(a,f,t1)∧t2t3∧¬Clipped(t1,f,t3)Clipped(t1,f,t4)↔(EC3)∃a,t2,t3[Happens(a,t2,t3)∧t1t3∧t2t4∧[Terminates(a,f,t2)∨Releases(a,f,t2)]]¬HoldsAt(f,t)←InitiallyN(f)∧¬Declipped(0,f,t)(EC4)1[Shanahan,1997a]showshowthecalculuscanbeusedtohandledomainconstraints,continuouschange,andnon-deterministiceffects.Indeed,theplannerdescribedinthispapercanhandlemanytypesofdomainconstraintwithoutfurthermodification.2Variablesbeginwithlower-caseletters,whilefunctionandpredicatesymbolsbeginwithupper-caseletters.Allvariablesareuniversallyquantifiedwithmaximumpossiblescopeunlessotherwiseindicated.3¬HoldsAt(f