SituationCalculus
RichardB.Scherl
ComputerScienceDepartment
MonmouthUniversityWestLongBranch,NewJersey
07764-1898U.S.A.rscherl@monmouth.edu
Abstract
Aformalframeworkforspecifyinganddevelopingagents/robotsmusthandlenotonlyknowledgeandsensingactions,butalsotimeandconcurrency.Re-searchershaveextendedthesituationcalculustohandleknowledgeandsensingactions.Otherre-searchershaveaddressedtheissueofaddingtimeandconcurrentactions.Herebothofthesefea-turesarecombinedintoaunifiedlogicaltheoryofknowledge,sensing,time,andconcurrency.There-sultpreservesthesolutiontotheframeproblemofpreviouswork,maintainsthedistinctionbetweenindexicalandobjectiveknowledgeoftime,andiscapableofrepresentingthevariouswaysinwhichconcurrencyinteractswithtimeandknowledge.Furthermore,amethodbasedonregressionisde-velopedforsolvingtheprojectionproblemforthe-oriesspecifiedinthisversionofthesituationcalcu-lus.
Furthermore,specificationofanagent’sabilitytoachieveagoalingeneralinvolvesrequiringthattheagentknowwhattodotoarriveatagoalstate[Moore,1980;Lesp´eranceetal.,2000].Astheabilitytoachieveparticulargoalswillofteninvolvetheabilitytoperformconcurrentactions,theintegra-tionofknowledgeandconcurrencyisanimportantstepinfullyformalizingtheseaspectsofability.
Wedevelopourframeworkwithinthesituationcalcu-lus–afirst-orderformalismforrepresentingandreasoningabouttheeffectsofactions.ThelanguageisbaseduponthedialectofthesituationcalculususedintheCognitiveRoboticsGroupattheUniversityofToronto.Certainly,an-otherformalismcouldhavebeenused.WithinA.I.numer-ousvaryingformalismsareavailablefornrepresentingandreasoningaboutaction(tonameafew,[Shanahan,1995;Baraletal.,1997]).Knowledgehasbeenincorporatedintoanumberofthese(forexample,[Loboetal.,2001;Thielscher,2000]).OutsideofA.I.proper,thereisalso[Fa-ginetal.,1995]ontheinteractionofknowledgeandtime.Butbyworkinginthesituationcalculus,weareabletoextendpreviousworkonreasoning(byregressionandtheo-remproving)tocoverthelanguagedevelopedhereaswell.Furthermore,ourworkissuitabletobeincorporatedintotherobotprogramminglanguagesGOLOGandCONGOLOG.Itcanthenbeusedtospecifyagentsthatmustreasonabouttheinteractionsoftime,knowledge,andconcurrentactions(in-cludingsensingactions).
Thesituationcalculus[McCarthyandHayes,1969]isalanguageformodelingdynamicallychangingworlds.Changestotheworldaretheresultsofactions,whilepos-sibleworldhistoriesconsistingofsequencesofactionsarerepresentedbysituations.Thesituationcalculuscanbeusedforagentplanningviagoalregression.Reiter[Reiter,1991]proposedasimplesolutiontotheframeproblem,anapproachtoaxiomatizationwithinthesituationcalculus.Al-thoughthisapproachtotheframeproblemrequirescertainsimplifyingassumptions,ithasproventobeusefulandisthefoundationforbothgoalregressionandtheprogramminglan-guageGOLOG.GoalregressionwasextendedbyScherlandLevesque[ScherlandLevesque,2003]toapplytoanagentwhocansensepropertiesoftheexternalworld(e.g.,readnumbersonapieceofpaperordeterminetheshapeofanobject).
1Introduction
Theaimofthispaperistodevelopaunifiedapproachforaxiomatizingtheinteractionofknowledge,sensing,time,andconcurrency.Actionshavepreconditionswhichmayincludeknowledgepreconditions.Sensingactionsalterknowledge.Theknowledgeproduceddependsupontherelativetimeatwhichsensingactionsoccurandalsowhetherornotothersortsofactionsoccurconcurrently.Allofthisinteractswiththeagent’sevolvingknowledgeoftime.
Considerarobotgatheringknowledgeaboutitsenviron-ment.Itmovesaboutwhileconcurrentlypanningthecameraandatvariouspointssensestheenvironmentforthepresenceofobjectswithvariouscharacteristics.Theknowledgeob-tainedthroughsensing(positionsofobjectsofvarioussizes,shapesandcolors)dependsuponthepositionoftherobotataparticularpointintime,theangleofthecamera,etc.Formanypurposes,theresultsofsensingactionsthatoccuratthesametimeareimportant.Notonlydowehavetheneedfortwodistinctconcurrentsensingactionsinbinocularstereop-sis,butalsointhesimultaneoususeofotherfeaturessuchastexturegradientsandshadingtoachieveknowledgeofdepthrelationships.Hereitisrelative,notabsolutetime,thatisimportant.
Thispaper1[combinesandextendstheworkofScherlandLevesqueScherlandLevesque,2003]incorporatingthemodelofconcurrencyandtimepresentedbyReiter[Re-iter,2001].Atthesametime,Reiter’ssimplesolutiontotheframeproblemispreserved.Therealdifficultyistoper-formthesynthesisinsuchawaythattheimportantdistinc-tionbetweenindexicalandobjectivetime[Lesp´eranceandLevesque,1995]ispreserved.
Iftheagentcurrentlyknowstheabsolutetime,thenheknowstheabsolutetimeafterexecutinganaction.Butifhedoesn’tknowtheabsolutetime,thenheonlyknowsthathebeganexecutingtheactionsomenumberoftimeunitsago,unlessofcoursehereadsaclock.Whilemaintainingtheseproperties,theresultspresentedhereallowtherepresentationofthevariouswaysinwhichactions(includingsensingac-tionsandpossiblyotherconcurrentactions)interactwithtimeandknowledge.Themethodofregressionisalsoextendedtoworkwiththisaugmentedlanguage.
Section2givesaquickintroductiontothesituationcalcu-lusandSection3doesthesameforthefoundationalaxioms.Therepresentationofknowledgeandsensingactionsarecov-eredinSection4.Concurrencyisintegratedintotheframe-workinSection5.Section6coverssomeadditionalcon-structsofthelanguageandillustratestheirrepresentationalpower.Anumberofpropertiesoftheformulationaredis-cussedinSection7.RegressioniscoveredinSection8.Fi-nally,Section9istheconclusion.
2SituationCalculusandtheFrameProblem
Spacedoesnotpermitafullexpositionofthebackground
material[onthesituationcalculus.TheframeworkdevelopedinReiter,[2001]isfollowedandfulldetailsmaybefoundthereorinScherl,2003].Weassumethattheframeproblemhasbeenhandledbyutilizingsuccessorstateaxioms.
3FoundationalAxioms
Following[LinandReiter,1994;Reiter,2001]thefounda-tionalaxiomsforthesituationcalculusareutilized.Theseaxiomsprovideuswithadefinitionofss,whichsaysthatthereisasequenceofzeroormoreexecutableactionsthatmovefromsituationstosituations.Again,spacedoesnotpermitfulldevelopmentofthismaterialhere.Fulldetailsmaybefoundin[Reiter,2001;Scherl,2003].
4AnEpistemicFluent
ScherlandLevesque[ScherlandLevesque,2003]adaptthestandardpossible-worldmodelofknowledgeto]thesituationcalculus,asfirstdonebyMoore[Moore,1980.Informally,onecanthinkoftherebeingabinaryaccessibilityrelationoversituations,whereasituationsisunderstoodasbeingaccessiblefromasituationsifasfarastheagentknowsinsit-uations,hemightbeinsituationsinsifitistrueineverysaccessible.Sofromsomethings,andconverselyisknownsomethingisnotknownifitisfalseinsomeaccessiblesitua-tion.
1
Anearlierversionofsomeofthisworkhasappearedin[Zim-merbaumandScherl,2000].
Totreatknowledgeasafluent,theyintroduceabinaryrela-tionK(s,s),readas“sisaccessiblefroms”andtreatitthesamewaywewouldanyotherfluent.Inotherwords,fromthepointofviewofthesituationcalculus,thelastargumenttoKistheofficialsituationargument(expressingwhatisknowninsituations),andthefirstargumentisjustanauxiliaryliketheyinBROKEN(y,s).2
ThenotationKnows(P(now),s)(readasPisknowninsituations)canthenbeintroducedasasanabbreviationforaformulathatusesK.Forexample
Knows(BROKENdef
→B(y,nows),)s.
)=∀sK(s,s)
ROKEN(y,Thespecialindexicalnowisinstantiatedwithasituationvari-ableuponexpansion.
Theapproachalsohandlesactionsthatmakeknownthedenotationofaterm.Forthiscase,oneneedsthenotationKref(T(now),s)definedasfollows:
Kref(T(now),s)def
where=xdoes∃xKnowsnotappear(T(nowin)=x,s)
T.Ingeneral,theremaybemanyknowledge-producingac-tions,aswellasmanyordinaryactions.Tocharacterize[allofthese,wehave]followingthepresentationinScherlandLevesque,2003,afunctionSR(forsensingresult),andforeachactionα,asensing-resultaxiomoftheform:
SR(α(x),s)
=r≡φα(x,r,s)(1)
Thisresultis“YES”if“Q”istrueand“NO”otherwise.The
symbolsaregiveninquotestoindicatethattheyarenotflu-ents.ThesensingresultfunctionforSENSEQisaxiomatizedasfollows:
SR(SENSE∨(Qr,=s)“=r≡(r=“YES”∧Q(s))
NO”∧¬Q(s))(2)
Forordinaryactions,theSRresultisalwaysthesame,withthespecificresultnotbeingsignificant.Forexample,wecouldhave:
SR(PICKUP(x),s)
=r≡r=“OK”(3)
InthecaseofaREADwouldτactionthatmakesthedenotationofthetermτknown,wehave:
SR(READτ,s)
=r≡r=τ(s)(4)
Therefore,τhasthesamedenotationinallworldsssuchthatK(sistrue.
,DO(READτ,s)),andsoKref(τ,DO(READτ,s))TheformofthesuccessorstateaxiomforKwithoutcon-currencyisasfollows:
K(s,((DO∃s(a,∧)ss))K=≡
DO(a,∧(s,s)∧s)Ps)
=OSS(a,a,s(5)
s)SR(a,SR()
TherelationKataparticularsituationDO(a,s)iscompletelydeterminedbytherelationatsandtheactiona.
2
NotethatusingthisconventionmeansthattheargumentstoKarereversedfromtheirnormalmodallogicuse.
5Concurrency
Asoriginallydefinedinthesituationcalculus[McCarthyandHayes,1969],actionshadtooccursequentially,withoneactioncompletedbeforeanothercouldbegin.Furthermore,therewasnofacilitytodealwiththecontinuouspassageoftime.Thiscontrastedwithotherformalismssuchastheeventcalculuswhichcouldnaturallyhandleconcurrentactionsandcontinuoustime.
5.1ConcurrencywithKnowledge
TheworkofPinto[Pinto,1994]andReiter[Reiter,2001]proposedanapproachtodealingwithconcurrency,naturalactionsandcontinuoustimewhilestill[maintainingtheso-lutiontotheframeproblem.ReiterReiter,2001]definedanewsortconcurrent,setsofsimpleactions.Variablesa,sorta,..concurrentrepresent.theInReiter’ssortactionsnotation,andthec,ctime,...ofrepresentanaction’stheoccurrenceisthevalueofthataction’stemporalargument.ThusanactionhastheformA(x,t)andforeachactionanaxiomoftheformTIME(A(x,t))=tisrequiredtoindicatethetimeoftheaction.
Concurrentactionsaresetsofordinaryactionsthataretakentorepresentinstantaneousacts.Anactionwithdura-tionisrepresentedbytwoinstantaneousactions—astartac-tionandanendaction.Additionally,thefoundationalaxiomsaremodifiedtoruleoutthepossibilityofprioractionshavinglatertimes.
SoifwewanttorepresentaPRESSINGactionwithduration(asinpressingabuttonthatkeepsalighton),theapproachistodefinetwoactions;STARTPRESSandENDPRESS.WealsomustintroduceafluentPRESSING.Theneededsucces-sorstateaxiomisasfollows:
PRESSING(DO(a,s))≡
a=(STARTPRESSPRESSING(s)∨
∧a=ENDPRESS)
(6)
Thisapproachtorepresentingactionswithdurationissome-thingthatwemakeuseofhere.
But,theuseofatemporalargumentforactionsisproblem-aticinthepresenceofknowledge.GivenoursuccessorstateaxiomforK,itwouldrequiretheagenttoknowthetimeafteranyaction,evenifitwasunknownintheprevioussituation.Toavoidthis,wecannotrepresenttimeasanargumenttotheinstantaneousactions.
Instead,werepresenttheinstantaneousactionsandasso-ciatedtimesasatupleoftheform ACTION( a,t>)=t (8) Thesepairs,representedbyvariablesp,pthesortaction-timepairs.ConcurrentActions,...areareelementsnowasetofofsuchtuples.Thesortactioncontainsactionswithoutatemporalargument. Wealsohavethefollowing START(DO(p,s)) =TIME(p)(9) whichisneededtorelatethetimeoftheaction/timepairtothestartofasituation.TheremayalsobeanaxiomgivingthestarttimeoftheinitialsituationS0.Wealsodefineavariantnotation: TIME(DO(p,s))=TIME(p)(10) Weadopt,withoutsignificantchange,Reiter’srequirementthatconcurrentactionsbecoherent,thatisthereisatleastoneaction-timepairpinthecollection,andthetimeofallpairsinthecollectionisthesame: COHERENT(∃(pc)) p≡ c∧(∃t)(∀p)[pc→TIME(p)=t(11) ]. Asetofaction-timepairsarecoherentifeachofthemhavethesametimecomponent. Thedefinitionoftimecanreadilybeextendedtosetsofconcurrentactionsandthisallowsustodefinethefunctionstartofasituationresultingfromtheexecutionofaconcur-rentaction. COHERENT[(c)→ ∧TIME(c)=do(tc,≡s))∃p=(p∈c∧TIME(p)=t)] START(TIME(c)].(12) ThepredicatePOSS(c,s)meansthatitispossibletoexe-cuteconcurrentactioncinsituations. POSS(ACTION→P(p),s)), ∧TIME(p)>TIME(s) OSS(p,s(13) POSS(p,s)→POSS({p},s),(14) POSS(c,s)→COHERENT(c)∧(∀p)[pc→POSS(p,s)]. (15) Ifitispossibletoexecuteaconcurrentactions,thenitisco-herentandeachofthesimpleactionsispossible. Weimplicitlyassumeanadditionalsortrangingovertimepointswhichcanbeintegers,rationalsorreals;dependingonhowonewantstomodeltime.ThestandardArabicnumeralsareusedtorepresenttimepoints.Additionally,thesymbolsforadditionandsubtractionareinterpretedastheusualoper-ationsonnumbers(integers,realsetc.) 5.2PreconditionInteractions Weneedtobeabletoconcludewhenaparticularconcurrentactioncispossibleinasituationcinorderforthemachinerybeingdevelopedintherestofthispapertowork.Unfortu-nately,Sentence15doesnotsuffice.Theconditionalcannotbechangedtoabiconditionalbecauseofthepreconditionin-teractionproblem[Pinto,1994;1998]. Thisissueneedstobehandledbytheaxiomatizerofthedomain.Forexample,theaxiomatizermightprovidethefol-lowingaxiom: POSS({pP1,p2},s)≡ OSS¬P(ACTION(a1),s)∧POSS(ACTIONp(a2),s)∧RECINT(a1,a2)∧COHERENT({1,p2}) (16) Asdiscussedin[Pinto,1994;1998],theaxiomatizationofPRECINTisdomaindependentandcanbedoneatincreasinglevelsofdetail. Forthepurposesofthispaper,thepointhereisthatwhat-eversolutionisusedforthepreconditioninteractionproblemintheordinarysituationcalculuscarriesovertothecaseofknowledgeandsensing. 5.3 SuccessorStateAxiomforKwithConcurrency TheSuccessorStateAxiomforKusingconcurrencycanbestatedinseveralalternativewaysdependingonwhatcondi-tionsonewishestoapplyregardingtheagent’sknowledgeoftime.WecontinuetorequirethattherelationKataparticularsituationDO(c,s)iscompletelydeterminedbytherelationatsandThethefollowingsetofconcurrentsuccessoractionsstateaxiomc. modelsanagentwhoknowsanaccuratehowclock. muchtimeispassing3.ThisisanagentwhohasK(s,(DO((∃c,ss,))c)≡ s∧(∀p)p=cDO(∃p(c)p,sc )∧K(s,s)∧POSS(c,s∧)∧ACTION(∀p)p(cpp())∃==pACTION(p)∧)pc ACTION(ACTION(p∧) ∧START(∀p)p(sc)→ =START(s)+(TIME(c)−START(s))SR(ACTION(p),s)=SR(ACTION(p),s ) (17) Afterexecutingasetofconcurrentactionscinsituations,asfarastheagentknows,itcouldbeinasituationsiffsistheresultofperformingcinsomepreviouslyaccessiblesituations,providedthatcispossibleinsandthatsisidenticaltosintermsofwhatisbeingsensed.Furthermore,itisrequiredthattheconcurrentactioncbeingperformedinallsituationsaccessiblefromsbeidenticaltocintermsoftheindividualactionsthatmakeuptheset. NotethatitisnotrequiredthattheTIMEoftheactionsinalltheaccessiblesituationsbeidentical.Ifthiswerethecase,itwouldforcetheagenttoknowtheobjectivetimeafterexecut-inganyaction.Rather,itisonlyrequiredthatthedifferencebetweenthestartofthecurrentsituationandthestartoftheprevioussituationbethesameinallaccessiblesituations(in-cludingtheactualsituation).Thisrequirementdoesensurethattheagentknowshowmuchtimeispassing,buttheob-jectivetimeisonlyknownifitwasknownbeforetheactionhasoccurred. 5.4ConcurrencyandSensing Onecanreadilyimaginecasesofsensingactionswherethedesiredresultofsensing(knowingwhetherornotsomepropositionholds)dependsuponsomeotheractionoccurringconcurrently.Forexample,thelightneedstobeturnedonwhilethecameraisclicked.Ifthelightisoff,thensensingproducesnoknowledge. Considerrepresenting,therequirementthatthelightswitchbepressedwhileSENSEwhetherornotPholdsPoccursfortheknowledgeoftoresultfromtheexecutionofSENSEP.WeneedtodefineapredicateSCOND. SCOND(SENSEP,s)≡PRESSING(s) (18) 3 Otherpossibilitiesareconsideredin[Scherl,2003]. toNowincludetheSsuccessoraswell. stateaxiomforKneedstobemodifiedCONDK(s,(DO∧(∀((∃c,pss),))pc)≡ cs(∃=pDO)p(c,s)∧K(s,s)∧POSS(c,s∧)∧(∀p)pc()∃=c ACTION(pp)ACTIONpc (p)∧ACTION(p)=ACTION(p∧) ∧START(s)=START(s)+(TIME(c)−START(s((S∀p)pc∧ ))COND(ACTION(sp)),=s)∧SCOND(ACTION(p),s()→ SRACTION(p),SR(ACTION(p),s ) (19) ForeveryactionanappropriateSCONaxiomneedstobewritten.Formostactions,theactionissimply: SCOND(a,s)≡T (20) 6TheLanguageandExamples 6.1 FurtherConstructs Weneedsomewaytorefertothecurrenttimewithoutspeci-fyingthevalueofthecurrenttime.Toachievethisweusethespecialindexicaltermnow.Uponexpansionthetermisre-placedwiththeappropriatesituationterm.So,START(now)canbeusedtorefertothecurrenttime.Hereweillustratebyexample.Theagent’sknowingtheobjectivetimeisexpressedas∃tKnow(start(now)=t,s).Thisexpandsinto ∃t∀s(K(s,s)→START(s)=t). Weaugmentourlanguagewithanumberofadditionalex-pressions.ThesearebasedonideasdevelopedbyLesperanceandLevesque[Lesp´eranceandLevesque,1995]andrequiretheuseofthenotionofprecedenceofsituationsasdefinedearlier.Notethatwedistinguishbetweenthe Happeneddef ∧(t,Act,s)=(∃c,s,s)s=DO(c,s)∧∃pc ACTIONs(sp)∧=sAct≺s∧ TIME(p)=t∧ (21) Itspecifiesthatanactionoccurredpriortosanditwastimetatsomepointduringtheaction’sduration. ThemacroWasatisintroducedtoallowonetoassertthatafluentwastrueataparticularpointintime. Wasat(t,def=P(then),s)=(∃s)P(then){st/then}∧ ¬(START∃s)s(s≺)∨st≺>sSTART∧(s∧) START(s)≤t ItspecifiesthatPheldatsandtwasthetimeofsors (22) pre-cededtandnoothersituationaftersprecededt.Hereweintroduceanotherspecialindexicalthenwhichisneededtoensurethatthecorrectsituationissubstitutedintothesitua-tionargumentofthepredicatewhichisthemiddleargumenttoWasat. 7PropertiesoftheFormulation Firstofall,weshowthatthedistinctionbetweenindexicalandobjectivetimeispreserved. Proposition1(PersistenceofIgnoranceofObjectiveTime)Forallsituationss,if¬∃tKnow(START(now)=t,s)thenindo(c,s)wherecisanyconcurrentactionitisalsothecasethat¬∃tKnow(START(now)=t,s)unlessthereissomea∈cwithanSRaxiomequivalenttothefollowing:SR(a,s)=r≡r=TIME(s) Proposition2(PersistenceofKnowledgeofObjectiveTime)8Reasoning AregressionoperatorRisdefinedrelativetoasetofsuc-cessorstateaxiomsΘ.Spacelimitationshereonlyallowasketchoftheregressionoperators.Fulldetailsmaybefoundin[Scherl,2003]. Theoperatorssatisfythefollowingregressiontheorem:Theorem1ForanygroundsituationtermsgrandformulaG: F|=G(sgr)iffF−Fss|=R∗Θ[G(sgr)] Forallsituationss,if∃tKnow(start(now)=t,s)thenindothat(c,∃st)Knowwhere(cstartisany(nowconcurrent)=t,s) actionitisalsothecaseEvenifagentsdonotknowtheobjectivetime,theydoknowhowmuchtimehaspassedsincethelastoccurrenceofapar-ticularactionorthelasttimeatwhichaparticularfluentwastrue. Proposition3(KnowledgeofIndexicalTime1)For∃tKnowsevery,((∃t ActsuchthatActoccursins, TIME(nowHappened)−t=(t,ts,) Act,now)∧ Proposition4(KnowledgeofIndexicalTime2)ForeveryP∃suchtKnowsthat(there∃tissomes≺ssuchthatP(s)holds,(TIME(nowWasat)−(tt,=P(t,thens) ),now)∧ Additionally,thecrucialresultsof[ScherlandLevesque,2003]carryovertothecaseconsideredhere.TheseincludeProposition5(DefaultPersistenceofIgnorance)Foranactionαandasituations,if¬Knows(P,s)holdsandtheaxiomatizationentails ∀sP(s)≡P(DO(α,s)) and ∀y¬Knows((POSS(α)∧SR(α)=y)→P,s)then ¬Knows(P,DO(α,s)) holdsaswell. Proposition6(KnowledgeIncorporation)Foraknowledge-producingactionα,afluentorthenegationofafluentF,afluentorthenegationofafluentP,andasituations,iftheaxiomatizationentails ∃yKnows(F≡SR(α)=y,s) andalso F(s),POSS(α,s), and Knows(F→P,s) hold,then Knows(P,DO(α,s)) holdsaswell. Proposition7(Memory)ForallfluentsPandsituationss,ifKnows(P,s)holdsthenKnows(P,DO(α,s))holdsaslongastheaxiomatizationentails ∀sP(s)≡P(DO(α,s)) Theseresultsensurethatactionsonlyaffectknowledgeintheappropriateway. HereFistheinitialaxiomatizationofthedomainandFthesetofsuccessorstateaxioms. ssis 8.1RegressionOperators TheregressionoperatorRisdefinedrelativetoasetofsuc-cessorstateaxiomsΘ.ThefirstfourpartsofthedefinitionoftheregressionoperatorRΘconcernordinary(i.e.notknowledge-producing)actions[Reiter,2001].Theyareex-actlythesameasthosein[Reiter,2001].Additionally,itisnecessarytocorrectlyregresstheequalitypredicateasdis-cussedin[ScherlandLevesque,2003;Reiter,2001]. Additionalstepsareneededtoextendtheregressionop-eratortoknowledge-producingactions.Twodefinitionsareneededforthespecificationtofollow.Whenϕisanarbitrarysentenceandsasituationterm,thenϕ[s]isthesentencethatresultsfrominstantiatingeveryoccurrenceofnowinϕwiths.Thereverseoperationϕ−1istheresultofinstantiatingeveryoccurrenceofsinϕwithnow. StepvcoversthecaseofregressingtheKnowsoperatorthroughanon-knowledge-producingaction.StepvicoversthecaseofregressingtheKnowsoperatorthroughaknowl-edgeproducingaction.Inthedefinitionsbelow,sisanewsituationvariable. v.Whenevercdoesnotcontainaknowledge-producingac-tion, RRΘ[Knows[(W,DO(c,s))]=Knows(POSS(c)→Θ[WDO(trans(c),s)]]−1,s).vi.WheneverR∃y[Knowscdoes(W,containaknowledge-producingaction, ΘDO(c,s))]=SRRKnows(SENSE[((Pi,s)=)y∧ OSS(c∧1SR(SENSE,s)i)=y)→Θ[WDO(trans(c))]]−Thespecialfunctiontransreplacescwithacthathastheidenticalactionineachoftheaction-timepairs.Butitre-placesthetimeportionwitharelativetime.Thisisanex-pressionoftheform(3=TIME(now)).So,ifcoccursinasituationtermoftheformDO(c,s)andTIME(c)is7andSTART(s)is4,thenthe7inthetimepartofeveryaction-timepairincwouldbereplacedby(3=TIME(now)).Theseareproperlyhandledbytheoperatorsforregressingequalitypredicates. TheregressionoperatorsforHappenedandWasatfollow:viii. R[Happened(∨Happened(t,Act,DO∃pc((t,(Act,c,s))]s)= ∧t≤START(s)) ACTION(p)=Act∧t=START(DO(c,s))) [Loboetal.,2001]JorgeLobo,GiselaMendez,andStuartTaylor.KnowledgeandtheactiondescriptionlanguageA.R[Wasat(t,W,DO(c,s))]= JournalofLogicProgramming,1(2):129–184,2001.(Wasat(t,W,s)∧t Theendresultofregressionisasentence(possiblymuch larger)inalanguagewithoutactions.Thelanguageisa modallanguagewithbothtemporalandepistemicoperators. 9Conclusions TheresultsreportedinthispapercanbecombinedwithConcurrent,TemporalGologorRGolog[Reiter,2001][or CONGOLOGGiacomoetal.,1997]tospecifyandcontrol anagent(suchastherobotdiscussedinSection1)thatcon-currentlymovesaboutitsenvironmentandperformsvarious actionsincludingsensingactions.Futureworkwilladdress theissueofdevelopingagoodtheoremprovingmethodforthelanguageresultingfromregression.Thismethodneedstocombinemodaltheoremprovingwithamethodforsolvingintegerconstraints.AcknowledgmentsNumeroushelpfuldiscussionshavebeenheldwithYves Lesp´eranceonmanyofthetopicscoveredinthispaper.Use-fulsuggestionsmadebyPatrickDoherty,DanieleNardi,and anumberofanonymousreviewersofearlierversionsofthis paperhavebeenincorporated.Additionalthanksaredueto SteveZimmerbaumwithwhomtheinitialstagesofthisworkwerecarriedout.ThisresearchwaspartiallysupportedbyNSFgrantsSES-9819116andCISE-9818309.References[Baraletal.,1997]ChittaBaral,MichaelGelfond,andAlessandroProvetti.Representingactions:Laws,obser-vationsandhypotheses.JournalofLogicProgramming,31(1-3):201–243,1997. [Faginetal.,1995]R.Fagin,J.Y.Halpern,Y.O.Moses,andM.Y.Vardi.ReasoningaboutKnowledge.MITPress,Cambridge,Mass,1995. [Giacomoetal.,1997]G.DeGiacomo,Y.Lesp´erance,andH.J.Levesque.Reasoningaboutconcurrentexecution,prioritizedinterrupts,andexogeneousactionsinthesitua-tioncalculus.InProceedingsoftheFifteenthInternational JointConferenceonArtificialIntelligence,Nagoya,Japan, 1997. [Lesp´eranceandLevesque,1995]YvesLesp´eranceandHectorLevesque.Indexicalknowledgeandrobotaction—alogicalaccount.ArtificialIntelligence,73(1-2):69–115, February1995. [Lesp´eranceetal.,2000]YvesLesp´erance,HectorJ.Levesque,FangzhenLin,andRichardB.Scherl.Abilityandknowinghowinthesituationcalculus.StudiaLogica,66(1),2000.[LinandReiter,1994]FangzhenLinandRaymondReiter.Stateconstraintsrevisited.JournalofLogicandCompu-tation,4(5):655–678,1994.Somephilosophicalproblemsfromthestandpointofar-tificialintelligence.InB.MeltzerandD.Michie,editors, MachineIntelligence4,pages463–502.EdinburghUni-versityPress,Edinburgh,UK,1969. [Moore,1980]R.C.Moore.Reasoningaboutknowledgeandaction.TechnicalNote191,SRIInternational,October 1980.[Pinto,1994]J.A.Pinto.TemporalReasoningintheSit-uationCalculus.PhDthesis,DepartmentofComputerScience,UniversityofToronto,Toronto,Ontario,1994.AvailableastechnicalreportKRR-TR-94-1.[Pinto,1998]JavierA.Pinto.Concurrentactionsandinter-actingeffects.InPrinciplesofKnowledgeRepresentationandReasoning:ProceedingsoftheSixthInternationalConference(KR-98),pages292–303.MorganKaufmann Publishing,1998. [Reiter,1991]RaymondReiter.Theframeprobleminthe situationcalculus:Asimplesolution(sometimes)andacompletenessresultforgoalregression.InVladimirLifs-chitz,editor,ArtificialIntelligenceandMathematicalThe-oryofComputation:PapersinHonorofJohnMcCarthy,pages359–380.AcademicPress,SanDiego,CA,1991.[Reiter,2001]RaymondReiter.KnowledgeinAction:Logi-calFoundationsforSpecifyingandImplementingDynam-icalSystems.TheMITPress,Cambridge,Massachusetts, 2001. [ScherlandLevesque,2003]RichardScherlandHectorLevesque.Knowledge,action,andtheframeproblem.Ar-tificialIntelligence,144:1–39,2003.[Scherl,2003]RichardScherl.Axiomatizingtheinteractionofknowledge,time,andconcurrencywiththesituation calculus.journalversioninprogress,2003.[Shanahan,1995]MurrayShanahan.Acircumscriptivecal-culusofevents.ArtificialIntelligence,77(2):249–284, September1995.[Thielscher,2000]MichaelThielscher.Representingtheknowledgeofarobot.InA.Cohn,F.Giunchiglia, andB.Selman,editors,ProceedingsoftheInternational ConferenceonPrinciplesofKnowledgeRepresentation andReasoning(KR),pages109–120.MorganKaufmann, 2000.[ZimmerbaumandScherl,2000]StephenZimmerbaumandRichardScherl.Knowledge,time,andconcurrencyinthe situationcalculus.InC.CastelfranchiandY.Lesp´erance, editors,IntelligentAgentsVII:Proceedingsofthe2000WorkshoponAgentTheories,Architectures,andLan-guages(ATAL-2000),LNAI,Berlin,2000.Springer-Verlag. 因篇幅问题不能全部显示，请点此查看更多更全内容