; TeX output 1995.08.10:1236 3ڍE&3ڍL+>K`y p cmr10RuleBasedUp }datesonSimpleKnolwledgeBases# 4K`y ff cmr10ChittaBaral DepartmentofComputerScience UniversityofTexasatElPaso "ElPaso,Texas79968,U.S.A. echitta@cs.ep.utexas.edutA r'"V 3 cmbx10AbstractG@"K`y 3 cmr10In2thispapMerw!econsiderupdatesthatarespeciedasrulesandconsider 79qsimple8kno!wledgebasesconsistingofgroundatoms.SWeepresentatransla-79qtionoftherulebasedupMdatespecicationstoextendedlogicprogramsusing79qsituation,calculusnotationsoastocomputetheupMdatedkno!wledgebase.79qWee sho!wthattheupMdatedknowledgebasethatwecomputesatisestheup-79qdateFspMecicationsandy!etisminimallydierentfromtheoriginaldatabase.79qWeefthenexpandourapproac!htoincompleteknowledgebases. 79qWee@relateourapproac!htothestandardrevisionandupMdateoperators,Hthe79qformalizationofactionsanditseectsusingsituationcalculusandthefor-79qmalizationfofdatabaseev!olutionusingsituationcalculus.,Ѝ+XQ cmr12|||||||{WrORKINGPVAPER(CommentsWVelcome)|||||||( <"V G cmbx101Inrtro Oductionb#MostbwrorkonbSeliefrevisionintheliteraturefocusonupdatingtheoriesbrysentencesinthe theory؟itself.Sevreraldierent\upSdate"operators(update,revision,conrtraction,erasure,forgetetc)[KM89,GM88$Y]andtherelationbSetrweenthemharvebeenstudied[KM92]andpSostulatesharvebSeensuggestedforsomeoftheseoperators[GM88],KM92#T].InUthispapSer2 |{Y cmr81wreconsiderupdatesthatarespeciedasrules[MT94b%](similartorulesina#logicprogram)andpresenrtmethoSdstocomputeupdatedknorwledgebaseswhenknowledgebasesconsistofasetofgroundatoms.ThefollorwingexampleillustratesthekindofupSdatesthatweconsider.Considerxaknorwledgebaseconsistingofthreeemployees:SJohn,wPeterandCarl;whichrepresenrt?acertaindepartment,g cmmi12Dinanorganisation./DuringanoraganisationalshakeupthedepartmenrthastobSeupdatedbasedonthenewknorwledgethat\IfJohnremainsinthe!departmenrtDugthenPeterhastoleavethedepartmentDugandifCarlremainsinthedepartmenrtvthenJohnhastostayinthedepartment".zWVealsohavetheassumptionthat pÉ ff - ^ٓR cmr71 K`y cmr10SuppGortedUUbythegrantsNSF-IRI-92-11-662andNSF-CDA90-15-006. 1 *3ڍE&3ڍ&anryՉchangesmadetotheinitialknowledgebasemustbSeexplCicitlyCdictatedbrytheupSdated knorwledge.TheJinrtendedmeaning[MT94a$]oftherststatementisdierentfromthestatement\eitherCJohnlearvesCthedepartmenrtorPeterleavesthedepartment".TherststatementcanexplicitlydictatetheremorvXalofPeterbutcannotdictatetheexplicitremovXalofJohn. IfthenewknorwledgeisspSeciedinpropositionaltheoryorinrstorderlogictheywrouldbSeequivXalenrt.The\if 8"and\then"inthestatemenrt\IfJohnremainsinthedepartmentDbKthenPeterhas\tolearve\thedepartmenrtDS"aretreateddierentlyfromtherstorderimplication.(Ourinrtent istogivreahigherpriorityto\JohnthantoPeter".ThisisnecessarybSecausewemighrtliketohavethelanguagethatspSeciesupdatestoharvepropSertieswhicharedierentfromtheonesheldbrythelanguageofthedatabase.TVospSecifysucrhrulesMarekandTruszczynski[MT94a$]inrtroSducethenotionof.@ cmti12rffevisionprffograms.8InthispapSerwrerefertothemasupffdate35specications. 0N cmbx12Denition 1K[MT94b$R]35AnupffdaterulecanbSeofthefollorwingtwoformssZTin(p)UR-!", cmsy10 in(q̸1);:::ʜ;in(q2 cmmi8m);out(s̸1);:::ʜ;out(s̹nP)ƽ(1) pout(p)UR in(q̸1);:::ʜ;in(q̹m);out(s̸1);:::ʜ;out(s̹nP)ƽ(2)wherep,q̹id'sands̹jf 'sareatoms. AcollectionofupSdaterulesiscalledaupdatespecication. 3Tq lasy102 They6ddeneP-justiedrevisionofsimpleknorwledgebasesbyarevisionprogram. Inthis˞papSerwreshowhowtocomputeP-justiedrevisionsofknowledgebasesusingextendedlogicprogramsandsituationcalculus.IMarekandTVruszczynski'sdenitionofP-justiedrevision`$isonlylimitedtothecasewhentheCWA`isassumedabSouttheinitialknorwledgebase.3WVeLextendtheideaofP-justiedrevisiontoknorwledgebasesthatcouldbSeincompleteandpresenrtanextendedlogicprogramthatcomputestherevisedknowledgebasewhentheinitialknorwledgebasemaybSeincomplete.WVethenconsiderupSdaterulesthatexplicitlyrelatestheinitialknorwledgebasetotherevisedHknorwledgebaseandshowhowrevisionscanbSecomputedforsuchupSdates.SuchrulesarebSeyrondthescopeofMarekandTVruszczynski'srevisionprograms.Our̴approacrhofcomputingtherevisedknowledgebaseissimilartotheformalizationof databaseevrolution[Rei92]butusesextendedlogicprograms[GL91O]insteadofrstorderlogic. vInitsuseofsituationcalculusandextendedlogicprogramsourapproacrhtreatsrevisionspSecicationsas\actions"andaknorwledgebaseasa\situation"andhassimilarityto^theformalizationofactionsandtheireectsin[GL92O].-OurapproacrhisdierentthantheV0evrentcalculusapproachin[Kow92"I]andconsidersmorecomplexrevisionsthandiscussedinit. 2 3ڍE&3ڍ&2RevisionSp Oecicationsb#InthissectionwrereviewtheconceptofrevisionspSecications22 UandP-justiedrevisionas denedin[MT94b%].LetGU0+bSeadenrumerableset.FItselementsarereferredtoasatoms.FAFknowledgebaseisanryksubsetofU@.By:Uwemeanthesetf:ab:a1N2U@g.ElementskofUC[:Uarecalledliterals.AlrevisionspSecicationusesasynrtaxsimilartologicprogramsexceptthatithastwospSecialPoperators\in"and\out".FVoranryatomatheintuitivemeaningin(a)isthattheatom|aispresenrtintherevisedknowledgebase."|Similarlythemeaningofout(a)isthattheatom^=aisabsenrtintherevisedknowledgebase.FVoranyatompinU@,{"in(p)anout(p)arereferredtoasr-literalsofU@.Theilstatemenrt\IfJohnremainsinthedepartmentDthenPeterhastoleavethedepart-menrtDS"iswrittenastherevisionrule: out(peterS)UR in(j ohn) WVenorwformallydenetherevisionspSecicationsandP-justiedrevision. Denition 2K[MT94b$R]35ArffevisionrulecanbSeofthefollorwingtwoformssZTin(p)UR in(q̸1);:::ʜ;in(q̹m);out(s̸1);:::ʜ;out(s̹nP)ƽ(3)pout(p)UR in(q̸1);:::ʜ;in(q̹m);out(s̸1);:::ʜ;out(s̹nP)ƽ(4)wherep,q̹id'sands̹jf 'sareatoms. AcollectionofrevisionrulesiscalledarevisionspSecication. ('2 Aknorwledge'baseB'-isar-moffdelof(satises)anr-literalin(p)(out(p)respSectively)ifpn2B(p62B ,CrespSectivrely).eBisar-moSdelofthebodyofaruleifitsatiseseacrhr-literalofzthebSodyV.Biszar-moSdelofaruleCWcifthefollorwingconditionshold: wheneverBsatisesthe0bSodyofC ܞ,ArthenBsatisestheheadofC. +Bisar-moSdelofarevisionspecicationPifBsatiseseacrhruleinP.Denition 3K[MT94b$R]KGLetTPbSearevisionspecication.Bynorm(P)wredenotethedeniteprogramobtainedfromPbryreplacingeachoSccuranceofin(a)byaandeachoSccuranceofout(b)bryb2K cmsy809.nTheneffcessaryCchangeforPgisthepair(I ;OS)whereIel=sfa:a2leastmoSdelof norSm(P)gandOj=fb:b20Y2 leastmodelofnorm(P)g.=Pwithnecessarycrhange(I ;O)issaidtobSecffoherentifI+\O=UR;.m2݉ ff - ^2 MarekkandT*ruszczynskiusedtheterm ': cmti10r}'evisionlprogramskinsteadofrevisionspGecications. WebGelieve itZtobGemoreofaspecicationlanguage(similartothelanguage!", cmsy10A[GL92]forspecifyingeectsofactions)thatUUcanbGeimplementedinalogicallanguageofchoice,ratherthanaprogramminglanguage. 3 3ڍE&3ڍ&Denition 4K[MT94b$R]5LetNPbSearevisionspecicationandD̹IandD̹R betrwoNknowledge bases. @P̹DX.; cmmi6Ris(KtherevisionprogramobtainedfromPbryeliminatingfromPevreryruleofthetypSe1or2sucrhthatq̹i,62URD̹R ;ors̹j\2D̹R.P̹DX.R :jD̹I istherevisionprogramobtainedfromP̹DX.RMbryeliminatingfromthebSodyofeachruleinP̹DX.Rqin(a)ifaUR2D̹Iandout(a)ifaUR62D̹IM.If$P̹DX.R :jD̹Iqwithnecessarycrhange(I ;OS)iscoherentandD̹R w=D̹I[^InOYthen$D̹R iscalledzP-justieffd35revisionofD̹IM,andwrewriteD̹IgPg $ y!LD̹R. R2InrtuitivelyV,@P̹DX.RisHthesetofrulesobtainedfromPbryremovingallrulesinPwhosebSodyNisnotsatisedbryD̹R;andP̹DX.R :jD̹IisthesetofrulesobtainedfromP̹DX.Rpbyremovingallr-literalsthatsatisfyD̹IfromthebSodiesofrulesinP̹DX.R :.Example 1DUQLetD̹I$=URfa;bgandP̸1bSetherevisionspecication ލc dout(b)UR in(a) f`Cu cmex10Co>P̸1cLetD̹R ;bSefag.E P̸1RٟL̹DX.R8is<%sameasP̸1)andP̸1L̹DX.RjD̹I$=URfout(b)gandhenceiscoherenrtwiththenecessarychangez(;;fbg)andD̹R H=URD̹Iy[;nfbg.8Hence,D̹IgPg $ y!LD̹R. @LetP̸2bSeՍd out(b)UR in(a) out(a)UR in(b) $f\C)P̸2iItiseasytoseethatP̸2-justiedrevisionsofD̹Iarefagandfbg.LetP̸3bSed out(b)UR in(a) out(a) $f\C)P̸3iItiseasytoseethatP̸3-justiedrevisionsofD̹IZisfbg..InrtuitivelywecanconsiderP̸1Kasthe logicprogramfout x ff f:bUR not'Fout̹agandP̸3asthelogicprogramout x ff f:bUR not'Fout x ff faout x ff f:aUR LetP̸4bSed Jin(a)UR in(a) Jin(c)UR in(c)f\C)VP̸4iItiseasytoseethatP̸4-justiedrevisionsofD̹Iisfa;bg. q2Prop` osition 1U[MT94b$R]IfJaknorwledgebaseDtsatisesarevisionspSecicationPthenD isauniqueP-justiedrevisionofDS.2Prop` osition 2U[MT94b$R]kLet(4PbSearevisionspecicationandD̹Ibeaknorwledgebase.IfaknorwledgebaseD̹R ;isaP-justiedrevisionofD̹IM,thenD̹Risar-moSdelofP.3 22 4 )3ڍE&3ڍ&Prop` osition 3U[MT94b$R]kLet(4PbSearevisionspecicationandD̹Ibeaknorwledgebase.If D̹R 8isaP-justiedrevisionofD̹IM,thenD̹R :D̹IsisminimalinthefamilyfDo5D̹Iy:D3isar-moSdelcofP)g, wheredenotesthesymmetricdierence.6i.e.ABX=UR(AnB )[(B4nA).2?ItlshouldbSenotedthattheaborvelpropositionjustsarysP-justiedrevisionsarer-modelsoftherevisionspSecicationthatareminimallydierenrtfromtheoriginaldatabase.7Itdoesnot|"sarythatr-moSdelsoftherevisionspecicationthatareminimallydierenrtfromtheoriginalAdatabaseareP-justiedrevisions.<3InExample1bSothfagandfbgarer-modelsofP̸1minimallydierenrtfromD̹I7butonlyfagisaP̸1-justiedrevision.,ThisissimilartothelogicYprogramaUR notbYwhicrhhastwominimalmoSdelsfagandfbg,vbuthastheonlystablemoSdelfag.'⍍3TXranslatingj~Revisionsp OecicationstoExtendedLogic Programsb#InthissectionwretranslaterevisionspSecicationstoextendedlogicprogramsandshowthattheanswrersetsofthetranslatedprogramcorrespSondtotheP-revisions.TheS+extendedlogicprogram(P[D̹IM)wherePistherevisionspSecicationandD̹I "xisthe1initialknorwledgebase,IusesvXariablesofthreesorts:6%situationvariabless;s209;:::ʞ,IfGlCuentvXariablesf ;fG208;:::ʞ,andrSevn9ision23vXariablesrr;rS20!;:::ʞ.Theprogram(P[s9D̹IM)consistsofthetranslationsoftheindividualrevisionrulesandtheinitialknorwledgebaseinPjandcertainotherrules.MWVenowpresentthetranslation(P[ZD̹IM)where"sisthesituationcorrespSondingtotheinitialknorwledgebaseD̹IM, rcorrespondtotherevisiondictatedbrytherevisionspSecicationPGandres(rr;s)isthesituationcorrespondingto|"theknorwledgebaseobtainedbyrevisingtheinitialknowledgebasewiththerevisionspSecicationP.?Algorithm 1MR[Trffanslating35RevisionSpecications{withCWAabouttheinitialdatabase]卍1.fiInitial35Databffase fe `/*IfpispropSositionintheinitialdatabasethen(PLn[D̹IM)conrtains(1.1)holCds(p;s)andtherule(1.2):holCds(FS;s)UR notholds(FS;s)whicrhencoSdestheCWAabouttheinitialdatabase.2.fiInertia35R2ule fe M"Q(2.1)holCds(FS;res(rr;s))UR holCds(FS;s);notab(F;rr;s)ThisruleismotivXatedbrytheminimalityconsiderationthatonlychangesthathappSenstotheinitialknorwledgebasearetheonesdictatedbytherevisionspSecication. l ff - ^3 The~revisionvqariablescorrespGondtotheactionvariablesinsituationcalculusandinthetranslationof theUUlanguageAtoextendedlogicprogramsin[GL92] 5 7p3ڍE&3ڍ&3.fiTrffanslating35therevisionrules fe 3(a)EacrhrevisionruleofthetypSe(1)Kistranslatedtotherule(3.a.1)holCds(p;rSes(rr;s))UR holCds(q̸1;rSes(rr;s));:::ʜ;holds(q̹m;rSes(rr;s)); =:holCds(s̸1;rSes(rr;s));:::ʜ;:holds(s̹nP;rSes(rr;s))(b)EacrhrevisionruleofthetypSe(2)out(p)UR in(q̸1);:::ʜ;in(q̹m);out(s̸1);:::ʜ;out(s̹nP)istranslatedtotherules:(3.b.1):holCds(p;rSes(rr;s))UR holCds(q̸1;rSes(rr;s));:::ʜ;holds(q̹m;rSes(rr;s)); =:holCds(s̸1;rSes(rr;s));:::ʜ;:holds(s̹nP;rSes(rr;s))(3.b.2)ab(p;rr;s)UR holCds(q̸1;rSes(rr;s));:::ʜ;holds(q̹m;rSes(rr;s)); =:holCds(s̸1;rSes(rr;s));:::ʜ;:holds(s̹nP;rSes(rr;s))Sincetheinertiarule(2.1)isonlyforthepSositivrefactswedonotneedaruledeningabnormalitryycorrespSondingto(3.a.1),ObutwedoneedsucharulecorrespSondingto(3.b.1)tobloScrktheinertiaruleandavoidinconsistencyV.4.fiCompleting35therffevised35database fe 8TVoencoSdetheCWAw.r.t.8thereviseddatabase(PLn[D̹IM)conrtainstherule(4.1):holCds(FS;res(rr;s))UR notholCds(FS;res(rr;s)) )T2+Example 2DUQConsider5D̹I aandP̸2 R9fromExample1./thetranslation(P̸2[D̹IM)consistsofthefollorwingrules:UTO)g[|holCds(a;s)[|holCds(b;s)[|:holCds(b;rSes(r̸1;s))UR holds(a;rSes(r̸1;s))[|ab(b;r̸1;s)UR holCds(a;rSes(r̸1;s))[|:holCds(a;rSes(r̸1;s))UR holds(b;rSes(r̸1;s))[|ab(a;r̸1;s)UR holCds(b;rSes(r̸1;s)[|1:2[|2:1[|4:1֍8UhC9 8Uh> 8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh= 8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh>8Uh;E(P̸2j[D̹IM)N~؍2,Theorem 1ELet