; TeX output 1993.08.09:0926;W 덠 K7"Vff cmbx10MoudalitiesinKno=wledgeRepresentation=K`y cmr101"q_u4K`yff cmr10UllrichHustadtandAndreasNonnengart oȍ""K`y 3 cmr10Max-Planc!k-InstitutffM8urInformatik, 낍xCImfStadt!wald,66123SaarbrM8ucken,Germany0X]0N cmbx12ABSTRACT6ݐ)A+XQ cmr12StandardknorwledgerepresentationsystemsaresuppSosedtobeableto c)ArepresenrteithercommonorindividualknowledgeabSouttheworld.)AInbthispapSerwreproposeanextensiontosucrhknowledgerepresentation)Asystemscwhicrh,~inauniformmanner,allorwstoexpressbSeliefsofmultiple)Aagenrtsaswellasknowledge,desire,timeandinfactanymoSdalitywhich)Ahasa rst-orderpredicatelogicpSossiblewrorldsemantics.[ ͼ<"VG cmbx101*InrtroOduction ͼSincethemid-sevrentiesavXarietryofknowledgerepresentationsystemsinthetradi- c ͼtion?ofsemanrticnetworksandterminologicallogicshasbSeenproposed.Themost ͼfamoussenrtences.PRWVesayTentails,_writtenTj=,i ͼevrerymoSdelofTnisamodelof. ͼSofarwredidnotconsideranyspSecialpropertiesofthegivrenmodaloperators. ͼTrypicaltAaxiomschematawhichre ectsuchpSotentialadditionalpropSertiesarelisted ͼbSelorw.9쿍/iyffdg; u͟! bff!fAxiomScrhema bffPropSertryd4! bffSffdg;ͤ! bffM2߸(m;a)}AC)UR3߸(m;a)}B С bffՌ8x9yË<2aRAm(x;yn9)E9! bff bͤ! bff%P2߸(m;a)}R)UR%P bff۴ 8xUR<2aRAm(x;x)Kas! bffͤ! bffMUR)2߸(m;a)}3߸(m;a)bơ bffx8x;yË<2aRAm(x;yn9)UR)<2aRAm(yn9;x)&˟! bffͤ! bffUZ2߸(m;a)}1)UR2߸(m;a)}2߸(m;a)R bffz8x;yn9;z5<2aRAm(x;y)^<2aRAm(y;z)UR)<2aRAm(x;z)͟! bffͤ! bff͟3߸(m;a)}1)UR2߸(m;a)}3߸(m;a)R bffz8x;yn9;z5<2aRAm(x;y)^<2aRAm(x;z)UR)<2aRAm(yn9;z)͟! bffffdg;Fzsatis es>allpropertiesinR.EWesayasetofMod-ALCsentencesTqentails ͼinallR-interprffetationsifallRinterprffetationswhicharemodelsofTarealso ͼmoffdels35of. ͼWhat1oisremarkXableforthepropSertiesfromaborve1oisthattheyallare rst-order ͼpropSerties.%Thereforekitisnottoosurprisingthatatranslationofmodaltermino- ͼlogical andmoSdalassertionalaxiomsinrto rst-orderpredicatelogiccanbedonevrery ͼeasilyV.& ͼ3*TXranslatingMoOd-ALC*rJinrtoClassicalLogic ͼThereharvebSeenalotofproposalsforcorrectandcompletecalculifornonclassical ͼlogics|tempSorallogics213 ,epistemiclogics29,etc.|andterminologicallogics23@2;5G$.mUnfortunatelyV,H2thesecalculirequireimplemenrtationsfortheirrespSectivetheorem ͼprorvingusystemwithhardlyachancetoapplyresultsandtechniquesofthetradi- ͼtionalwrorkonautomatedtheoremproving.CTherefore,rwefollowtheapproachof ͼOhlbacrh212 toeliminatemoSdaloperatorsinawraythatwregetstandard rst-order ͼpredicatelogicformrulaethatstillrepresentthemoSdalsemantics.mInthissectionwrede nesuchalogicmorphismthatmapsMoSd-ALC-into rst- ͼorderpredicatelogic.mFirst,}wrebvtransformallconceptsandroleswhichoSccurinagivenknowledgebase ͼinrtoZ_neffgationnormalform,vMi.e.inaformwherenoimplicationorequivXalencesign ͼoSccurs.andwhereallnegationsignsoccursolelyinfronrtoftheprimitiveconcepts. ͼThiscanbSeperformedinastraighrtforwardmannerasknorwnfromclassicallogic ͼandBthereforethetecrhnicaldetailsareomittedhere.AInthesequelweassumethat ͼanry(terminologicalorassertional)sentenceisalreadyinnegationnormalform.mNorwFDwetranslatetheterminologicalandassertionalsentencesinto rst-order ͼlogicformrulaeusingthefunction[K[ ʉfff ]]d.<rӬډff) u͟! bff͟Axiom{p bff TVranslationß! bffSff)͟! bff͟[K[UR2߸(m;a)M̸2:::M̹nP`]]̹U{p bff 8V:UR<2aRAm(U;Vp))[K[M̸2:::M̹nPB ]K]̹Vi! bff b͟! bff͟[K[UR3߸(m;a)M̸2:::M̹nPa]]̹U{p bff 9V:UR<2aRAm(U;Vp)^[K[M̸2:::M̹nPB ]]̹V! bff͟! bff͟[K[URC̸1VvC̸20]]̹U{p bff 8XF:UR[K[C̸1ҵ]]̹UZ;X4E )UR[K[C̸2ҵ]]̹UZ;X3! bff͟! bff͟[K[URC̸1VC̸20]]̹U{p bff [K[URC̸1VvC̸20]]̹U;^[K[URC̸2VvC̸10]]̹U`П! bff͟! bff͟[K[URR̸1VvR̸22 ]]̹U{p bff 8XJg;Y:UR[K[R̸1\2]]߹UZ;(X&;Y㐸)DL)UR[K[R̸2\2]]߹UZ;(X&;Y㐸)ٟ! bff2h;W 덠ۍǯ!Ʒ! bff͟[K[URR̸1VR̸22 ]]̹Uv߸ bff@[K[URR̸1VvR̸22 ]]̹U^[K[URR̸2VvR̸12 ]]̹UM֟! bff b!Ʒ! bff͟[K[URa2A$O3]]̹Uv߸ bff@[K[URA]]̹UZ;a! bff!Ʒ! bff͟[K[UR(a;b)2P8]]̹Uv߸ bff@[K[URP]]߹UZ;(a;b)! bff!Sffr:! ͼwherethetranslationofconceptsandrolesisde nedbry:zq[Iff)X u͟! bff͟TVerm{ք bff^[K[URC1]]̹UZ;YF! bff͟! bff͟[K[UR2߸(m;a)}C0hE]]̹UZ;X{ք bff<8V:UR<2aRAm(U;Vp))[K[C1]]̹Vx;Xi! bff͟! bff͟[K[UR3߸(m;a)}C0]]̹UZ;X{ք bff<9V:UR<2aRAm(U;Vp)^[K[C1]]̹Vx;X! bffff)X u͟! bff͟[K[URP]]߹UZ;(X&;Y㐸){ք bffwetakeacloserloSokattheresultsofthetranslationdescribedaborve ͼwre canseequiteabigproblem. Alreadysimpleknowledgebasesresultinrather ͼhrugelclausesetswheremanyoftheclausesmerelyexpresscertaininformationsabSout ͼaccessibilities.Pandrolecorrelations.ButwrecanexploitapropSertyofthelanguage ͼMoSd-ALC(DwhicrhGistypicalformostmoSdalandterminologicallogics,_namelyV,each ͼaccessibilitryrelationsymbSolorrolesymbSolREoccurseitherintheform9xURRJ(:::ʞ;x)P^ ͼ(x)xorintheform8x"FRJ(:::ʞ;x))(x).eOHorwxwecanmakeuseofthisspSecial ͼsynrtacticalfeatureisexplainedinthefollowingsection.& ͼ4*FXunctionalSimrulationofn-aryPredicates ͼFirstofallletusde newhatwremeanbyafunctional35simulator.c ͼDe nition7(FunctionalSimulators)E;W 덠  ͼLetzrespSectivrelySimxYRY2,>iscalledSimY̸1],respSespec- ͼtivrelySim̸2?.cmThrus,2forkanytotal(serial)accessibilityrelationorrolewecanintroSducefunc- ͼtionalqsimrulators.$xThisallowsanalternativede nitionforthetranslationinto rst- ͼorderpredicatelogicasdescribSedbelorw. ͼDe nition9(AnAlternativefor[=q[UR]]̹!) ͼThealternativrefor[K[UR]]̹$Fdi ersfrom[K[UR]]̹merelyinthefollorwingcaseswherethe ͼassoSciatedaccessibilitryrelationsandrolerelationsareassumedtobetotal.(-On}[K[UR3߸(m;a).(]]2?RAUM3=p9Vp:F̺<;cmmi6aGm[K[UR]]2?V㐸(U");n}[K[UR3߸(m;a)}C0]]2?RAUZ;XM3=p9Vp:F̺<䍰aGm[K[URC1]]2?V㐸(U");Xn}[K[UR3߸(m;a)}R0]]2?UZ;(X&;Y㐸)M3=p9Vp:F̺<䍰aGm [K[URRn]]2?V㐸(U");(X&;Y)(, ͼNoteo%thatalthoughthesynrtaxofthetranslationsuggestsasecond-orderquanti - ͼcationwreactuallydonotgobSeyond rst-orderlogic.]];W 덠  ͼLemma4.2 c ͼLet0RbSeasetofformrulaewhichexpressesthepropSertiesoftheunderlyingacces- ͼsibilitryrelations.8ThencRURj=[K[]]̹#i 2R[fSimH̸2ULgURj=[K[]] ?ڍ ͼPro`of: CanbSefoundin211cmWVeharvegainedquitealotalreadyV,however,underthesepreliminariesvrery c ͼinrterestingsimpli cationsarepSossible.mNotesthattheclauseformofsucrhatranslationdoSesnotcontainanypSositive ͼoSccurrencemofaroleoraccessibilitryrelationsymbSol. Thisfactcanbeexploited ͼinavreryinterestingmanner.SinceanyroleoraccessibilityrelationsymbSolcan ͼonly[oSccurintheadditionalaxiomswrecanexaminetheseindependenrtlyfromthe ͼtranslatedformrula.;Nonnengart211 presentsextremelygoSodsimpli cationsforvXarious ͼmoSdallogics.So," forinstance,thewholetheoryforthemoSdallogicKD45(i.e.the ͼaccessibilitryrelationisserial,7transitiveandeuclidean)canbSesimpli edtothe ͼalmosttrivialunitclauseRJ(U;Vp(W)).hFVorthosereadersfamiliarwithKD45this ͼmighrtnotbSetoosurprisingsincetheclassofframeswhicrharecharacteristicfor ͼKD45arejustthoseframeswhicrhconsistofasingleequivXalenceclassoraworld ͼfollorwedbyanequivXalenceclasssuchthatthisworldhasaccesstoalltheelements ͼinRthisclass.Otherexamplesforsuitablesimpli cationsaree.g.thelogicKDB<(i.e. ͼthe{accessibilitryrelationisserialandsymmetric).ThesetoftheoryclausestobSe ͼaddedUtothetranslationofgivrenformulaconsistsjustofthetwosimpleunitclauses ͼRJ(U;X(U@))andR(X(U@);U)andnothingelseisnecessaryV.mInZthefollorwingtheoremwesuppSosethatwehavesomesimpli cationSimwhich ͼcan'bSeappliedtoasetRofformrulaeexpressingthepropertiesoftheaccessibilitry ͼrelationsucrhthatc_R[fSimH̸2ULgURj=[K[]] ?ڍ$Hi 2"Sim(R)[fSimH̸2gURj=[K[]] ?ڍ ͼTheorem1 ͼLffetbeaMod-ALCTsentenceandTBasetofMod-ALCTsentences.5LetRbeasetof ͼformulae35whichexprffessthepropertiesoftheunderlyingaccessibilityrelation.fiThencTj=̺R  ͼi cC[ "%}Jȸ 2T[K[UR ]] ?ڍ[Sim(R)[fSimH̸2ULgURj=[K[]] ?ڍx ͼi 0r$"2[K[UR]]2?RAC,isWprffovablefromCS 8 2T! [K[UR ]]2?RAAM[.Sim(R)[fSimH̸2ULgWusingsometheorem"2prffover35whichiscorrectandcompletefor rst-orderlogicwithequality.l̠;W 덠  ͼ5*AnExample ͼSuppSoseBobisacarsellerandTimisacustomer.TimtellsBobthathewrants c ͼto.buyanicecarandforsomereasonhebSelievresthatredcarsareverynice.3Bob ͼhastoldTimthathecano eramagenrtacoloredaudi.Ofcourse,itiscommon ͼbSelievre,mOthatS.magentaisaredcolorandthattheaudiisacar.rqThissituationcan ͼbSerepresenrtedbythefollowingknowledgebase.445S2߸(belKievI{e;bob).E?2߸(belKievI{e;tim)audiURcolCorSed+magn9enta b5S2߸(belKievI{e;all)magn9entaUR2rSed5S2߸(belKievI{e;all)audiUR2car5S2߸(belKievI{e;bob).E?2߸(belKievI{e;tim)Dcar6u9colCorSed:red׃v3,nicexfff:car5S2߸(belKievI{e;bob)2߸(belKievI{e;tim)2_-nicexfff:car׃v3,2߸(w7ant;tim),buy"fffcar ͼFVrom}thisknorwledgebaseitfollowsthatBobbSelievesthatTimwantstobuythe c ͼaudi,i.e.>2߸(belKievI{e;bob).E?(audiUR22߸(w7ant;tim),buy"fffcar_:)A ͼshouldbSeprorvXable.mThetranslationoftheknorwledgebaseresultsinthefollowingclauses:@?colCorSed(V;audi;magn9enta) x( z< bobڍbelKievI{e(;U@)^< timڍbelKievI{e(U;Vp)(1)cp,rSed(U;magn9enta) x( z< alKlڍbelKievI{e(;U@)(2)carS(U;audi) x( z< alKlڍbelKievI{e(;U@)(3)ynicexfff:carS(V;X) x( z< bobڍbelKievI{e(;U@)^< timڍbelKievI{e(U;Vp)^ zcolCorSed(V;XJg;Yp)^red(V;Yp)^ zcarS(V;X)(4)}{buy"fffcarS(V;X) x( z< bobڍbelKievI{e(;U@)^< timڍw7ant(U;Vp)^ znicexfff:carS(f GtimڍbelKievI{e(U@);X)(5) ͼWVeassumebSothconsistencyandfullinrtrospectionfortheagenrts'beliefs.vInthis c ͼcasewreareallowedtosimplifythetheoryclausesforthemoSdaloperatorto211 :c < XڍbelKievI{e(U;Y pXڍbelKievI{e(Vp))R((6) ͼwhere4Xrangesorver4thesetofagenrts(i.e.BobandTim).ThespSecialagentallRis ͼthereforeaKD45-opSeratoraswrell,whichrangesoverallagents,thus: < alKlڍbelKievI{e(U;Y pXڍbelKievI{e(Vp))R((7) ͼFVorthewant-opSerator,,horwever,wedonotassumeanrythinginparticular,merely ͼconsistencyofwhatiswranted:< Xڍw7ant(U;Y pXڍw7ant(U@)) y((8) ͼFinallyV,wregetasthenegatedtheorem:(URbuy"fffcarS(h timڍw7ant(g n9bobڍbelKievI{e());audi)(9) ͼBecause allaxiomsareHornclauses,wrecanevenusePROLOGtoproveourtheo- ͼrem.8ThelinearderivXationofthegoalis: z,;W 덠 ퟔzff23 ͟! ff(URbuy"fffcarS(h2timRAw7ant(g2n9bobRAbelKievI{e());audi) ff 􍍐͟! ff(UR<2bobRAbelKievI{e(;U@)^<2timRAw7ant(U;h2timRAw7ant(g2n9bobRAbelKievI{e()))^nicexfff:carS(f2GtimRAbelKievI{e(U@);audi) ff b͟! bff,]usingaxiom5 bff͟! ff(URnicexfff:carS(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi) ff͟! bff,]usingaxioms6and8 bff͟! ff(UR<2bobRAbelKievI{e(;U@)^<2timRAbelKievI{e(U;f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e()))UR^ ff͟! ff"!colCorSed(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi;Yp)^red(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());Yp)UR^ ff͟! ff"!carS(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi) ff͟! bff,]usingaxiom4 bff͟! ff(URcolCorSed(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi;Yp)^red(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());Yp)UR^ ff͟! ff"!carS(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi) ff͟! bff,]usingaxioms6trwice bff͟! ff(UR<2bobRAbelKievI{e(;U@)^<2timRAbelKievI{e(U;f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e()))^ ff͟! ff"!rSed(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());magn9enta)^car(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi) ff͟! bff,]usingaxiom1 bffv-Lƍ溟! ff(URrSed(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());magn9enta)^car(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi) ff b溟! bff,]usingaxioms6trwice bff 􍍑溟! ff(UR<2alKlRAbelKievI{e(;f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e()))^carS(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi) ff溟! bff,]usingaxiom2 bff溟! ff(URcarS(f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e());audi) ff溟! bff,]usingaxiom7 bff溟! ff(UR<2alKlRAbelKievI{e(;f2GtimRAbelKievI{e(g2n9bobRAbelKievI{e())) ff溟! bff,]usingaxiom3 bff溟! bffsuccess bff溟! bff,]usingaxiom7 bff Sff23a ͼ6*ConclusionandFXurtherWork ͼWVepresenrtedanapproachwhichallowstoreasonwithinmoSdalterminologicallogics c ͼbry utilizinganappropriatetranslationtechniqueinto rst-orderpredicatelogic.The ͼmainideabSehindthismethodisthefunctionalUsimulationofaccessibilitryrelations ͼandsrolesbrysuitablesetsoffunctions.@ThisturnsouttohavetwomainadvXantages: ͼit decreasesthesizeandthenrumbSer ofclausesanditallorwssigni cantsimpli cations ͼonthesetoftheoryclauses.mA[necessary\conditionforthemethoSdproposedheretowrorkisthattheacces- ͼsibilitryrelationpropSertieshavetobSe rst-orderpredicatelogicde nable.cUnfortu- ͼnatelyV,notallmoSdallogicsharvea rst-orderdescribableframepropertryV.mUnrtil{now,wehaveonlyworkedouttheoptimizationforthosemoSdalitieswhich ͼharveasimplepSossiblewrorldsemantics.+8IftheinteractionofmultiplemoSdalitiesre- ͼquiresthemorecomplexneighrbSourhoodsemantics,Ǵwehavetorelyonthestraight- ͼforwrarditranslationwhichwillresultinaratherlargenumbSerofclauses.Looking ͼfor,$optimizationsforthiscaseispartoffuturewrork.UBesides,InsidetheLOOMZDescriptionClassi er.SIGARTBulletin, ͼ2(3):88{92,,1991. SpSecialIssueonImplemenrtedKnowledgeRepresentationand ͼReasoningSystems. ͼ9.R.+C.MoSore.Autoepistemic+Logic.InPh.Smets, E.H.Mamdani,D.DubSois, ͼand$H.Prade,s^editors,Non-StandarffdSLogicsforA2utomatedReasoning.$Academic ͼPress,London,1988. ͼ10.J.MylopSoulosandM.Brodie,*editors.1/RffeadingsinA2rti cialIntelligencffeand ͼDatabffases.5MorganKaufmann,SanMateo,CA,1989. ͼ11.A.z5Nonnengart.~;First-OrderMoSdalLogicTheoremProrvingandStandardPRO- ͼLOG.YInrternalrepSortMPI-I-92-228,<Max-Planck-InstituteforComputerScience, ͼJuly1992. ;W 덠  ͼ12.H.}J.Ohlbacrh.AhRffesolution΁CalculusforModalLogics.PhD|thesis,Univrersit at c ͼKaiserslautern,OctobSer1988.c ͼ13.N.RescrherandA.Urquhart.5Tempfforal35Logic.Springer,Berlin,1971. ͼ14.J. G.Scrhmolze.fTheLanguageandSemanticsofHnikl.fTVechnicalRepSort89{4, ͼDepartmenrtofComputerScience,TVuftsUniversityV,Medford,MA,1989.;;Q H- cmcsc10Cu cmex10<"VG cmbx10;!",G cmsy107"Vff cmbx104K`yff cmr103Tq lasy101߆T cmtt120N cmbx12.@ cmti12-!", cmsy10,g cmmi12+XQ cmr12"K`y 3 cmr10K`y cmr10K cmsy82cmmi8 |{Ycmr8ٓRcmr7;cmmi6