Mobile Tracking Using Forward Link in Cellular Networks 在蜂窝网络中使用前向链路进行移动跟踪

AutomatingCommonSenseReasoningGopalGuptaDepartmentofComputerScienceTheUniversityofTexasatDallasPart0:AI/KRR/Introduction

PartI:CommonSenseReasoning&AnswerSetProgramming(ASP)

PartII:ExecutionofASPprograms

PartIII:ApplicationsArtificialIntelligenceIntelligentreasoningbycomputershasbeenagoalofcomputerscientistseversincecomputerswerefirstinventedinthe1950s.Intelligencehastwocomponents:Acquiringknowledge(learning):automateitmachinelearningApplyingknowledgethatisknown(reasoning)automateitautomatedreasoningOurfocus:automatedreasoningReasoningisessential:machinelearningalgorithmslearnrulesthathavetobeemployedforreasoningMachinelearningoversold?:Usedinmanyplaceswherereasoningwouldsuffice;reasoningabilityiscriticalashumansbothlearnandreason.KnowledgeRepresentationandReasoningKnowledgerepresentationandreasoningNeedalanguagetorepresentknowledge[KR]Needalanguagetoprocessthisknowledgeandqueryit[R]IdealifthelanguageforKRandRisthesame:KRlanguageis“executable”(i.e.,hasadeclarativeandanoperationalsemantics)Hornclauses(logicprogramming)constitutesuchalanguageKnowledgeisrepresentedasfactsandrules:

p.pisapropositionthatisunconditionallytrue

q:-b1,b2,b3,….,bn.qisapropositionthatisconditionallytrue

Aruleisanimplicationb1

˄b2

˄b3

˄….˄bn

qQueriesareoftheform?-b1,b2,b3,….,bn.answeredviaSLDresolution

queryansweringequalsarefutationproof,i.e.,showb1

˄b2

˄b3

˄….˄bn

falseManyotheralternatives:firstorderlogic,descriptionlogic,semanticnet,…

LogicProgramming(Prolog)Facts:father(jim,john). mother(mary,john).father(john,rob). mother(sue,rob).…. .…Rules:parent(X,Y)ifmother(X,Y).parent(X,Y)if

father(X,Y).grandparent(X,Y)ifparent(X,Z)&parent(Z,Y).anc(X,Y)ifparent(X,Y).anc(X,Y)ifparent(X,Z)&anc(Z,Y).Queries:?-anc(jim,rob).?-anc(A,rob).LogicProgramming(Prolog)Facts:father(jim,john). mother(mary,john).father(john,rob). mother(sue,rob).…. .…Rules:parent(X,Y)⇐mother(X,Y).parent(X,Y)⇐father(X,Y).grandparent(X,Y)⇐parent(X,Z)⋀parent(Z,Y).anc(X,Y)⇐parent(X,Y).anc(X,Y)⇐parent(X,Z)⋀anc(Z,Y).Queries:?-anc(jim,rob).?-anc(A,rob).LogicProgramming(Prolog)Facts:father(jim,john). mother(mary,john).father(john,rob). mother(sue,rob).…. .…Rules:parent(X,Y):-mother(X,Y).parent(X,Y):-father(X,Y).grandparent(X,Y):-parent(X,Z),parent(Z,Y).anc(X,Y):-parent(X,Y).anc(X,Y):-parent(X,Z),anc(Z,Y).Queries:?-anc(jim,rob).?-anc(A,rob).PartI:CommonSenseReasoning&AnswerSetProgramming

CommonSenseReasoningStandardLogicProg.failsatperforminghuman-stylecommonsensereasoningInfact,mostformalismshavefailed;problem:monotonicityCommonsensereasoningrequires:Non-monotonicity:thesystemcanreviseitsearlierconclusioninlightofnewinformation(contradictoryinformationdiscoveredlaterdoesnotbreakdownthingsasinclassicallogic)IfTweetyisabird,itcanfly;conclusiontoberetractedifTweetyisfoundtobeapenguinDrawconclusionsfromabsenceofinformation;humansusethis[defaultreasoning]patternallthetime:Can’ttellifitisrainingoutside.IfIseenooneholdinganumbrella,soitmustnotberainingYoutextyourfriendinthemorning;hedoesnotrespond;normallyherespondsrightaway.Youmayconclude:hemustbetakingashower.Possibleworldssemantics:beabletoworkwithmultipleworlds(non-inductivesemantics)Commonsensereasoningrequiresthatweareabletohandlenegationasfailure&supportpossibleworldsemantics

ClassicalNegationvsNegationasFailureClassicalnegation(CN)representedas-pe.g,-sibling(john,jim)%statesthatJohnandJimarenotsiblingsAnexplicitproofoffalsehoodofpredicatepisneeded-murdered(oj,nicole)holdstrueonlyifthereisanexplicitproofofOJ’sinnocence(seeninBostonairport,Nicole’sbodywasfoundinLA)Negationasfailure(NAF)representedasnot(p)e.g.,notsibling(john,jim)%statesthatnoevidenceJohnandJimaresiblingsWetrytoproveapropositionp,

ifwefail,weconcludenot(p)istrueNoevidenceofpthenconcludenot(p)not(murdered(oj,nicole))holdstrueifwefailtofindanyproofthatOJkilledNicole

FAILTOPROVE(NAF)vsEXPLICITLY

PROVINGFALSEHOOD(CN)FailureofClassicalMethodsforCommonSenseReasoningGivenasetofaxiomsA1,A2,…,An,adecisionprocedurebasedonclassicallogicgivesusamethodforprovingatheoremT.A1,A2,…,An╞

TWhatiftheproofofTfails(i.e.,wegetstuck&cannotprogress)?ClassicallogicbaseddecisionproceduresdonotgiveusanyinsightwhenaprooffailsInmanycircumstanceswemaybeabletoconcludethattheproofofTisnotpossibleandso

Tshouldhold.

Mostofcommonsensereasoningisofthisform:IfwefailtoproveT(now),thenTmustbefalse(thoughTmaybecometruelater)Dualalsotrue:ifweproveT(now),thenTistrue(thoughitmaybecomefalselater)FailureofClassicalReasoningMethodsforCSRExample:Transitiveclosure:edge(a,b).edge(b,c).edge(f,g).reach(X,Y):-edge(X,Y).reach(X,Y):-edge(X,Z),reach(Z,Y).?-reach(a,f).Queryfails(noproof);Underclassicaltheoremprovingwecan’tconcludethatfisunreachablefromnodea.Needaxiomsforunreachability,onlythenwecanconclude–reach(a,f).Thatis,wehavetoexplicitlydefinerulesfor–reach(X,Y).Failureisnotoflogicorthedecisionprocedure,ratherhowweinterprettherules.Interpretimplicationsascausalrelations:AifBmeansAiffBreach(X,Y)↔(edge(X,Y)

(edge(X,Z),reach(Z,Y))).NowwithNAFwecanwrite:unreachable(X,Y):-notreachable(X,Y).Note:whenhumanswrite“ifAthenB”,theymean“AiffB”mostofthetime;E.g.:breaks_object:-drop_objectweautomaticallymeannot_breaks_object:-not_drop_object.

abcfgNegationasFailure(NAF)HumansuseNAFallthetime;however,usingNAFdoesmakelifedifficultHard(forhumans)todealwithnestednegation:WhoallwillgotoMexico?Codethisas:

p:-nots.

s:-notr. r:-notp. r:-nots.Whatisthesemanticsofthisprogram?Individualruleseasytounderstand;extremelyhardtounderstandwhattheprogrammeansasawholePaulwillgotoMexicoifSallywillnotgotoMexicoSallywillgotoMexicoifRobwillnotgotoMexico.RobwillgotoMexicoifPaulwillnotgotoMexico.RobwillgotoMexicoifSallywillnotgotoMexico.AnswerSetProgramming(ASP)PrologextendedwithNAF;Rulesoftheform:

p:-

a1,…,am,notb1,…,notbn.m,n≥0(rule)

p.(fact)

ASPisapopularformalismfornonmonotonicreasoningAnotherreading:addptotheanswerset(modeloftheprogram)ifa１,…,am

areintheanswersetandb1,…,bnarenotTherulecouldtakemoregeneralform

p:-

a1,…,am,notb1,…,notbn,-c1,...,-ck,not-d1,…,not-di

m,n,k,i≥0(rule)

LogicprogramswithNAFgoalsinthebodyarecallednormallogicprogramsApplicationsofASPtoKR&R,planning,constrainedoptimization,etc.Semantics:lfpofaresidualprogramobtainedafter“Gelfond-Lifschitz”transformPopularimplementations:Smodels,DLV,CLASP,etc.Morethan30yearsofresearchinvestedAnswerSetProgrammingAnswersetprogramming(ASP)BasedonPossibleWorldsandStableModelSemanticsGivenananswersetprogram,finditsmodelsModel:assignmentoftrue/falsevaluetopropositionstomakeallformulastrue.ModelsarecalledanswersetsCapturesdefaultreasoning,non-monotonicreasoning,constrainedoptimization,exceptions,weakexceptions,preferences,etc.,inanaturalwayBetterwaytobuildautomatedreasoningsystems&expertsystemsCaveatsp⇐a,b.reallyistakentobep⇔a,b.Weareonlyinterestedinsupportedmodels:ifpisintheanswerset,itmustbeintheLHSofa‘successful’ruleTherulep:-q.(qp)hasamodelinwhichqisfalseandpistrue;suchmodelsarenotinterestingWhenwewritep:-q.wearestatingthatpistrueifqistrue(qbeingtruesupportspbeingtrue)Human-styleCommonSenseReasoningWhyhavewefailedtomodelhuman-stylecommonsensereasoning?NAF+anotherreason:multiplepossibleworldsFrege&Russell:Fregediscovers(naïve)settheorythatRussellfindsaproblemwith(Russell’sparadox).Problemiscausedbycircularity;Russell’ssolution:bancircularityRussell:henceforth,everystructure(includingsets)mustbeinductive,i.e.,startfromthesmallestelementandthensuccessivelybuildlargerelementsfromit;anythingnon-inductive(coinductive)isbanishedfromthelanguage.Thewholemathematics/logicenterpriseobsessedwithonlyhavinginductivestructuresThus,anytheoryinvolvingpredicatesmusthaveaninductivesemantics(singlemodel)However,circularityariseseverywhereinhumanexperiencealongwiththeoriesthathavemultiplemodels(possibleworldssemantics).

jack_eats_food:-jill_eats_food.

jill_eats_food:-jack_eats_food.Twopossibleworlds:botheatornoneeat;inductivesemantics:noneeatAutomatingCommonSenseReasoningIfweautomateCSR,wecanautomatethehumanthoughtprocessModelanyintelligenttaskthathumanscanaccomplishAchieveartificialgeneralintelligence(AGI),atleastOurgoalistosimulateanunerringhumanSofar:Weneednegation-as-failuretomodelthefactthathumansoperateinaworldwherelotofstuffisunknownWeneedpossibleworldsemantics,ashumansdonotalwaysreasoninductively,i.e.,humanscanreasonwithmultipleworldssimultaneously;eachofthesemultipleworldshastobeconsistentthough(coinductive)AnswerSetProgrammingprovidesboththesefeatures,henceisanexcellentcandidateformodelingcommonsensereasoningASPGivenananswersetprogram,wewanttofindouttheknowledge(propositions)thatitentails(answersets)Forexample,giventheprogram:p:-notq.q:-notp.thepossibleanswersetsare:

1.{p}i.e.,p=true,q=false

2

2.{q}i.e,q=true,p=falseComputedviaGelfond-LifschitzMethod(Guess&Check)GivenananswersetS,foreachpS,deleteallruleswhosebodycontains“notp”;deleteallgoalsoftheform“notq”inremainingrulesComputetheleastfixpoint,L,oftheresidualprogramIfS=L,thenSisananswersetp=TomteachesDBq=MaryteachesDBTwoworlds:TomteachesDB,MarydoesnotMaryteachesDB,TomdoesnotFindingtheAnswerSetConsidertheprogram:p:-notq.t.r:-t,s.q:-notp,r.s.h:-p,noth.ApplytheGLMethod--Ifxinanswerset,deleteallruleswithnotx inbody--Next,removeallnegatedgoalsfromthe remainingprogram--FindtheLFPoftheprogram:--Initialguess{p,r,t,s}≠{p,r,t,s,h} so{p,r,t,s}isnotastablemodel.{p,r,t,s,h}Is{p,r,t,s}theanswerset?FindingtheAnswerSetConsidertheprogram:p:-notq.t.r:-t,s.q:-notp,r.s.h:-p,noth.ApplytheGLMethod--Ifxinanswerset,deleteallruleswithnotx inbody--Next,removeallnegatedgoalsfromthe remainingprogram--FindtheLFPoftheprogram:--Initialguess{q,r,t,s}=LFP so{q,r,t,s}isastablemodel.{q,r,t,s}Is{q,r,t,s}theanswerset?r.ASP

{p,a}{}{q}{a}{a}{b}{p,a}{b}{b,d}nonenone{r}{p,r}ASP:ExamplesConsiderthefollowingprogram,A:p:-notq.t.r:-t,s.q:-notp.s.Ahas2answersets:{p,r,t,s}&{q,r,t,s}.NowsupposeweaddthefollowingruletoA:h:-p,noth.(falsifyp)Onlyoneanswersetremains:{q,r,t,s}Consideranotherprogram:

p:-nots.s:-notr.r:-notp.r:-nots.Whataretheanswersets?{p,r}PaulwillgotoMXifSallywillnotgotoMXSallywillgotoMXifRobwillnotgotoMX.RobwillgotoMXifPaulwillnotgotoMX.RobwillgotoMXifSallywillnotgotoMX.h:-p,noth.EvenloopscreatemultipleworldsOddloopskillworldsConstraintsTherulesthatcauseproblemareoftheform:

h:-p,q,r,noth.thatimplicitlydeclaresp˄q˄

rtobefalseASPalsoallowsrulesoftheform(headlessruleorconstraint)::-p,q,r.whichassertsthattheconjunctionofp,q,andrshouldbefalse.Thetwoareequivalent,exceptthatinthefirstcase,nothmaybecalledindirectly:h:-p,q,s.s:-r,noth.ConstraintsareresponsiblefornonmonotonicbehaviorAruleoftheformp:-notpwrecksthewholeknowledgebaseaspnotphasnomodel.

AnswerSetProgrammingAnswersetprogrammingsubsumesHornclauselogicprogrammingGenerate&Testparadigmrealizedviaevenloopsandoddloops/constraintsEvenloops:p:-notq.q:-notp.Oddloops/constraints:h:-r,noth.OR:-r.Evenloopscreate(multiple)worlds,oddloopskillworldsConsiderp:-notq.

q:-notp.

:-p.Evenloopscreatestwoworlds:{p,notq},{q,notp}Constraintkillsoneofthem,soonlyoneworldremains:{q,notp}

SlidefromSonTranofNMSUSlidefromSonTranofNMSUSlidefromChitaBaral(ASU)DefaultsandExceptions

AS={flies(tweety),flies(sam)}Ourreasoningisaggressive:ifwedon’tknowanythingaboutabird,itcanflyAS={flies(tweety))}flies(sam)doesnotholdanymoreClosedWorldAssumption(CWA)

CWAaboutbird,penguin,abCWA:ifwefailtoprove,thentakeitasadefiniteproofoffalsehoodHumansuseCWAallthetime;wecanmakeitexplicitinASPwithclassicalnegationOpenWorldAssumption(OWA)

CWAaboutbird,penguin,abOWAaboutfliesOWA==NoCWA;Butnowwecanbemoreselective:CWAforsomeandOWAforothers.SlidefromChitaBaral(ASU)OpenWorldAssumption

Next,removeCWAaboutbird,penguin,abAssumeourinformationabouttheseconceptsisincompleteDoesetfly?AnswerisYESButnowthatwenolongerhaveCWAaboutbeingapenguin,it’spossiblethatetmightbeapenguin.Wenowneedtobemoreconservativeinourreasoning.flies(et)willnowfail,asIfailtoestablishthatetisnotapenguinDoesetflynow?:AnswerisNOSlidefromChitaBaral(ASU)DefaultsandExceptionsTosummarize

Aggressive

Conservativeflies(X):-bird(X),notab(X).ab(X):-not-penguin(X).penguin(tweety).bird(tweety).bird(sam).-penguin(X):--bird(X).?-flies(tweety).Ans:no?-flies(sam).Ans:noflies(X):-bird(X),notab(X).ab(X):-penguin(X).penguin(tweety).bird(tweety).bird(sam).-penguin(X):-notpenguin(X).?-flies(tweety).Ans:no?-flies(sam).Ans:yesSlidefromC.Baral(ASU)Toputallthisinperspective,considerthecollegeadmissionprocess:SincewehavenoinformationaboutJohnbeingspecialor

special,botheligible(john)and

eligible(john)fail.SoJohnwillhavetobeinterviewedUniversityAdmissionASPforCommonSenseReasoningASPallowshuman-stylecommonsensereasoningtobemodeled(duetoinclusionofnegationasfailure)Negationasfailureallowsustoignoreunnecessaryinformationthatisnotrelevantatthemoment(defaults&exceptions).ASPallowsustotakeactionspredicatedonlackofinformation:use_gps_system(X):-notdirections_known(X).ASPgivesusahierarchyof(un)certaintythatwehumansemploy,givensomepropositionp(e.g.,p=itisrainingnow):pdefinitelytrue:ppmaybetrue:not–p(possiblep)punknown:not–p¬ppmaybefalse:notp(noevidenceofp)pdefinitelyfalse:-pASPhaspossibleworldsemanticswheremultipleworldscanexistAsaresult:ASPallowshumanknowledgeandreasoningtobemodeledfaithfully.ab(X):-not-penguin(X)

ab(X):-possiblyXisapenguinGenerally,wehumansdonotemployprobabilitiesinourdaytodaycommonsensereasoningIncompleteInformationConsiderthecoursedatabase:BydefaultprofessorPdoesnotteachcourseC,ifteach(P,C)isabsent.Theexceptionsarecourseslabeled“staff”.Thus:

¬

teach(P,C):-notteach(P,C),notab(P,C).ab(P,C):-teach(staff,C).Queries

?-teach(mike,pl)and

?-¬

teach(mike,pl)

willbothfail:wereallydon’tknowifmiketeachesplornot(unknown)ProfessorCoursemikeaisamdbstaffplRepresentedas:

teach(mike,ai).teach(sam,db).teach(staff,pl).CombinatorialProblems:ColoringSlidefromS.Tran(NMSU)CombinatorialProblems:ColoringSlidefromS.Tran(NMSU)CombinatorialProblems:N-QueensSlidefromS.Tran(NMSU)CombinatorialProblems:N-QueensSlidefromS.Tran(NMSU)PossibleWorldsPeoplecantalk.(inallworlds)talk(X):-people(X).Non-humananimalscan'ttalk.(inrealworld)-talk(X):-non_human_animal(X),rw.Human-likecartooncharacterscantalk.(incartoonworld)talk(X):-human_like_cc(X),cw.Fishcanswim.(inallworlds)swim(X):-fish(X).Afishisanon-humananimal.(inrealworld)non_human_animal(X):-fish(X),rw.Nemoisahuman_likecartooncharacter.(incartoonworld)human_like_cc(nemo):-cw.Nemoisafish.(inallworlds)fish(nemo).cw:-notrw.rw:-notcw.Cannemotalk??-talk(nemo).Cannemoswim??-swim(nemo).40SupposeMarybelievesthatJohnwasinHollandParksomemorningandthatHollandParkisinLondon.ThenMarycandeductivelyreasonfromthesebeliefs,toconcludethatJohnwasinLondonthatmorning.Sothereasoningcannotbeattacked.However,perfectionremainsunattainablesincetheargumentisstillfallible:itsgroundsmayturnouttobewrong.Forinstance,JanmaytellusthathemetJohninAmsterdamthatmorningaroundthesametime.WenowhaveareasonagainstMary'sbeliefthatJohnwasinHollandParkthatmorning,sincewitnessesusuallyspeakthetruth.Canweretainourbelieformustwegiveitup?TheanswertothisquestiondetermineswhetherwecanacceptthatJohnwasinLondonthatmorning.MaybeMaryoriginallybelievedthatJohnwasinHollandParkforareason.MaybeMarywentjogginginHollandParkandshesawJohn.WethenhaveareasonsupportingMary'sbeliefthatJohnwasinHollandParkthatmorning,sinceweknowthataperson'ssensesareusuallyaccurate.Butwecannotbesure,sinceJantoldusthathemetJohninAmsterdamthatmorningaroundthesametime.PerhapsMary'ssensesbetrayedherthatmorning?ButthenwehearthatJanhasareasontolie,sinceJohnisasuspectinarobberyinHollandParkthatmorningandJanandJohnarefriends.WethenconcludethatthebasisforquestioningMary'sbeliefthatJohnwasinHollandParkthatmorning(namely,thatwitnessesusuallyspeakthetruthandJanwitnessedJohninAmsterdam)doesnotapplytowitnesseswhohaveareasontolie.SoourreasoninsupportofMary'sbeliefisundefeatedandweacceptit.RepresentingKnowledgewithASP41WemapvariousstatementsintoASP,e.g.,theargument(rule)forspeakingtruth:

speaks_truth(X,Y):-person(X),person(Y),observer(E,X),theme(E,Y),notab_speaks_truth(X,Y).

ab_speaks_truth(X,Y):-may_lie(X,Y).may_lie(X,Y):-person(X),person(Y),not-lie(X,Y).

-lie(X,Y):-person(X),person(Y),notconflict_interest(X,Y).

conflict_interest(X,Y):-friends(X,Y),crime_suspect(Y),notab_conflict_interest(X).

crime_suspect(X):-person(X),robbery_suspect(X),notab_crime_suspect(X).LikewiseforMary’sinfirmityaccurate_senses(X):-person(X),notab_accurate_senses(X).

ab_accurate_senses(X,sense):-person(X),age(X,A),A=old.RepresentingKnowledgewithASPexception42Basedontheassumptionswemake,wecanprovedifferentclaims:Maryisinfirmandhaspooreyesight#abducibleage(mary,old).JanandJohnarefriends#abduciblefriends(john,jan).Johnisarobberysuspect#abduciblerobbery_suspect(john).Assumptionsaremodeledasabducibles(abductivereasoning)Givenpqandanobservationq,weabduce(assume)thatpistrueNowclaimscanbeestablishedautomaticallywithrequisiteassumptions?-claim(john_location_unknown).Assumptions:age(mary,old)˄friends(jan,john)˄robbery_suspect(john)?-claim(john_not_in_london).

Assumptions:age(mary,old)˄notfriends(jan,john).Assumptions:age(mary,old)˄friends(jan,john)˄notrobbery_suspect(john)?-claim(john_in_london).Assumptions:friends(jan,john)˄robbery_suspect(john)Assumptions:age(mary,B|B

old)˄friends(jan,john)˄robbery_suspect(john)RepresentingKnowledgewithASP43s(CASP)canproducejustificationtree(prooftree)foragivenclaim:

JohnisinLondonattime8AM,becauseMarysawJohnat7:45AM,andJohnwasatholland_parkat7:45AM,andholland_parkisinlondon,andMaryhassharpsenses.Sightinghappenedattime7:45AM,becauseJohnwasatholland_parkat7:45AM.JansawJohnat7:45AM,and...JohnwasatAmsterdamat7:45AM,andJohnisnolongerinLondonat7:45AM,becauseJansawJohnat7:45AM.MeetingeventinvolvesJohn,becauseJansawJohnat7:45AM.MeetingeventinvolvesJohn,justifiedabove,andJanmaylieaboutJohn,becauseJanhasconflictofinterestwithJohn,becauseweassumethatJanandJohnarefriends,andJohnisacrimesuspect.JustificationtreeinEnglishcanbeproducedPartII:Goal-directedExecutionofASPCurrentASPSystemsVerysophisticatedandefficientASPsystemshavebeendevelopedbasedonSATsolvers:CLASP,DLV,CModelsThesesystemsworkasfollows:Groundtheprogramsw.r.t.theconstantspresentintheprogramTransformthepropositionalanswersetprogramsintopropositionalformulasandthenfindtheirmodelsusingaSATsolverThemodelsfoundarethestablemodelsoftheoriginalprogramBecauseSATsolversrequireformulastobepropositional,programswithonlyconstantsandvariablesarefeasible(datalog)Thus,onlypropositionalanswersetprogramscanbeexecuted:whyisthat?

WhyonlypropositionalASP?Considertheevenloop:

teach_db(john):-notteach_db(mary).teach_db(mary):-notteach_db(john).Thecompletedprogramis:teach_db(john)

notteach_db(mary).teach_db(mary)

notteach_db(john).Thesearepropositionalformulas;modelsquicklyfoundusingaSATsolver:{teach_db(john)=true,teach_db(mary)=false}

{teach_db(mary)=true,teach_db(john)=false}Whatifwehave:X

YifXteachesdatabases,Ydoesnot,andviceversateach_db(X):-notteach_db(Y),XY.teach_db(Y):-notteach_db(X).Onesolutionistosimply“ground”theprogramwithallpossiblevaluesofXandY(that’stheapproachadoptedbymost)WhatifdomainsofXandYarenotknown:wewouldneedtohavequery-drivenexecutionlikeProlog

WhyonlypropositionalASP?Problem:PossibleworldsemanticsinpredicatelogichasnotbeenexploredblameRussell&Tarski’spushtokeepeverythinginductiveAllsemanticsconsideredforcomputationallogicsareleastfixedpointbased,i.e.,inductiveWeneedgreatestfixedpointbasedsemanticsaswell(coinductivesemantics)Breakthrough:coinductivelogicprogramming(ICLP2006)[LukeSimonthesis]CoinductiveLP:operationalsemanticsforcomputingelementsofthegreatestfixpointofaprogram:

Program:jack_eats_food:-jill_eats_food.

jill_eats_food:-jack_eats_food

gfp(T

)={jack_eats_food,jill_eats_food}lfp(T

)={}Possibletonowhavepredicateanswersetprogramming(withfullpredicates)

CurrentASPSystems:IssuesFiniteGroundability:ProgramhastobefinitelygroundableNotpossibletohavelists,structures,andcomplexdatastructuresNotpossibletohavearithmeticoverrealsExponentialBlowup:GroundingcanresultinexponentialblowupGiventheclause:p(X,a):-q(Y,b,c).Itturnsinto3x3,i.e.,9clausesp(a,a):-q(a,b,c).p(a,a):-q(b,b,c). p(a,a):-q(c,b,c).p(b,a):-q(a,b,c).p(b,a):-q(b,b,c). p(b,a):-q(c,b,c).p(c,a):-q(a,b,c).p(c,a):-q(b,b,c). p(c,a):-q(c,b,c).Imaginealargeknowledgebasewith1000clauseswith100variablesand100constants;UseofASPseverelylimitedtoonlysolvingcombinatorialproblems(nottoKRproblems)ProgrammershavetocontortthemselveswhilewritingASPcodeOnlyDatalog+NAF:Programscannotcontainlistsstructuresandcomplexdatastructures:resultininfinite-sizedgroundedprogramCurrentASPSystems:IssuesEntireModel:SATsolversfindtheentiremodeloftheprogramEntiremodelm