÷
ƒ’À;����è TeX output 1993.08.09:0926‹���
������������������������������������ÿÿÿÿ ´î; ýW
 Šõ덠ýš
‘KàÙó7ò"V�ff�
���cmbx10âMouÂdalities–…in“KnošŠ=wledge“Represen˜tationŸúÆ=óKñ`y�
���
���cmr10Ä1ŽŽŽŸ"q‘_u‰ó4Kñ`y�ff�
���cmr10ßUllric™˜h–ÌÍHustadt“and“Andreas“NonnengartŽŸ
oȍ’�Œ"Ÿó"Kñ`y�
ó3�
���cmr10ÍMax-Planc²!k-Institut–¦ffMÞ‘ú8ˆur“Informatik,ŽŸ낍‘xCýIm›¦fStadt•²!w“ald,˜66123˜SaarbrMÞ‘ú8ˆuc“k“en,˜German“yŽŸ0¥‚’�¼X]ó0ÂÖN �������cmbx12ÛABSTRA �CTŽŸ6¢ŸÝ‘)A¤ó+X«Q�������cmr12ÖStandard–’€knoš¬rwledge“represen˜tation“systems“are“suppšSŽosed“to“b˜e“able“toŽ¤
Æc‘)A¤represenš¬rt–ê¨either“common“or“individual“kno˜wledge“abSŽout“the“w˜orld.Ž¡‘)A¤In–Übthis“papšSŽer“w¬re“prop˜ose“an“extension“to“sucš¬rh“kno˜wledge“representationŽ¡‘)A¤systems–c³whic¬rh,›~±in“a“uniform“manner,˜alloš¬rws“to“express“bSŽeliefs“of“m˜ultipleŽ¡‘)A¤agenš¬rts–žàas“w˜ell“as“kno˜wledge,–®desire,“time–žàand“in“fact“an˜y“moSŽdalit˜y“whic˜hŽ¡‘)A¤has–ê¨a“rst-order“predicate“logic“pSŽossible“wš¬rorld“seman˜tics.ŽŽŽŸ[£‘ͼó<ò"V�G®�
���cmbx10ç1Ž‘*œŠIn‘ÿr°tro‘�OductionŽ©¨†‘ͼÖSince–æthe“mid-sev•¬ren“ties–æa“v‘ÿXäarietš¬ry“of“kno˜wledge“represen˜tation“systems“in“the“tradi-Ž¤
Æc‘ͼtion–?of“semanš¬rtic“net˜w˜orks“and“terminological“logics“has“bšSŽeen“prop˜osed.‘ü¤The“mostŽ¡‘ͼfamous–<±example“is“óHŒ-ø����
���cmcsc10ëHKL-ONEŸû¥2ó
|{Y�������cmr8¸3Ž‘	üµÖwhicš¬rh“rst“appSŽeared“in“1977“in“R.“J.“Brac˜hman'sŽ¡‘ͼPh.D.–ê¨thesis.‘8àOther“examples“are“ëHKR‘þó3YPTONŸû¥2¸2Ž‘ÀÖ,“ëHNIKLŸû¥2¸14Ž‘	�Ö,“ëHLOOMŸû¥2¸8Ž‘ª¬Öand“ó-!",š����
���cmsy10ØK,`RI‘�âÈSŽ‘&ývŸú÷y¸1Ž‘+½zÖ.Ž¡‘m°All–€™these“systems“can“bSŽe“used“to“represenš¬rt“common“or“individual“kno˜wledgeŽ¡‘ͼabšSŽout–À¨the“w•¬rorld.‘ºàRecen“tly‘ÿV,‘ö(terminological–À¨logics“ha•¬rv“e–À¨b˜een“extended“to“allo¬rw“theŽ¡‘ͼrepresenš¬rtation–ZEof“the“kno˜wledge“or“the“bSŽeliefs“of“m˜ultiple“agen˜ts“in“one“kno˜wledgeŽ¡‘ͼbaseŸû¥2¸4Ž‘@Ÿû¥2ó×
2�������cmmi8¹;‘꨸7ŽŽ‘G$Ö.Ž¡‘m°In–Œthis“papSŽer,‘0øwš¬re“in˜v˜estigate“suc˜h“an“extension“whic˜h“allo˜ws“not“only“to“represen˜tŽ¡‘ͼeither–—Kknoš¬rwledge“or“bSŽeliefs“of“m˜ultiple“agen˜ts“but“a“h˜uge“v‘ÿXäariet˜y“of“mošSŽdal“op˜eratorsŽ¡‘ͼfor–ê¨mš¬rultiple“agen˜ts.Ž¡‘m°The–àapproacš¬rh“describSŽed“is“implemen˜ted“in“the“ëHMOTEL‘ÖÖkno˜wledge“represen˜ta-Ž¡‘ͼtion–
,system.‘|mëHMOTEL‘�åÖwš¬ras“dev˜elopSŽed“at“the“Max-Planc˜k-Institute“for“ComputerŽ¡‘ͼScience–ê¨and“is“currenš¬rtly“used“at“the“Univ˜ersit˜y“of“SaarbrSŽ‘ùÌvuc˜k˜enŸû¥2¸6Ž‘ÀÖ.ŽŸ&ÒW‘ͼç2Ž‘*œŠSyn›ÿr°tax–Ÿ¼and“Seman˜tics“for“Mo‘�Od-ó;!",š�G®�
���cmsy10æALCŽ¦‘ͼÖW‘ÿVe–Њassume“four“disjoin¬rt“alphabSŽets,›ÕÃthe“ó.›»ˆ@�������cmti12Ùprimitive‘3c–ÿffonc“epts‘ÎgØC‘�³5Ö,˜the‘ЊÙprimitive‘3r“oles‘ÎgØRÖ,Ž¡‘ͼthe–œ¶set“ØM“Öof“Ùmo–ÿffdal›Ößop“er“ator˜names‘�ýÝÖ,‘É:and–œ¶the“individual“ob‘�§jects“ØOUVÖ.‘O
In“particular,Ž¡‘ͼthere–+is“a“distinguished“subset“ØA“Öof“the“individual“ob‘�§jects,‘Ìcalled“the“set“of“ÙagentsÖ,Ž¡‘ͼconš¬rtaining–
xthe“spSŽecial“agen˜t“Ùal‘�™™l“Öwhic˜h“is“suppSŽosed“to“denote“the“union“of“all“theŽ¡‘ͼagenš¬rts–½…in“order“to“bSŽe“able“to“express“m˜utual“bSŽelief.‘±xThe“tuple“(ØOUVó,·ág£�������cmmi12×;–
ÿþØA×;“ØM×;“ØC‘�³5×;“ØRÖ)‘½…isŽ¡‘ͼcalled–ê¨the“Ùsignatur‘ÿffeÖ,“denoted“b¬ry“.Ž‘ͼŸ
8q‰��ff�ª¶ÄŸ��‘
ƒŸü^ÿóÙ“ R�������cmr7³1ŽŽ‘�ÄT‘ÿ*ªo–UUappšGear“in“\Pro˜ceedings“of“the“1993“Australian“Joinš¸ãt“Conference“on“Articial“In˜telligence"ŽŽŽŒ‹������������������������������������������* ´î; ýW
 Šõ덠ýš
‘m°ÖThe–Ä7set“of“Ùc–ÿffonc“ept›æ|terms–Ä7Ö(or“just“Ùc–ÿffonc“eptsÖ)–Ä7and“Ùr‘ÿffole˜terms“Ö(or“just“Ùr‘ÿffolesÖ)“isŽ¤
Æc‘ͼinductivš¬rely–É¿dened“as“follo˜ws.‘-èEv˜ery“primitiv˜e“concept“is“a“concept“term“and“ev˜eryŽ¡‘ͼprimitivš¬re–^role“is“a“role“term.‘¿
No˜w“assume“that“×C‘�ÜžÖ,–"‹×CŸ
Ì̸1Ž›ÀÖ,“and–^×CŸ
Ì̸2Ž‘×bÖare“concepts,–"‹×RJÖ,“×RŸ
Ì̸1Ž˜Ö,Ž¡‘ͼand–­9×RŸ
Ì̸2Ž‘m=Öare“roles,‘¹‚×m“Öis“a“mošSŽdal“op˜erator“name,‘¹‚×a“Öis“an“agen¬rt's“name.‘$fThen“×CŸ
Ì̸1Ž‘í0Øu‘-,×CŸ
Ì̸2Ž‘ÀÖ,Ž¡‘ͼ×CŸ
Ì̸1Ž‘ŸØt‘Z›×CŸ
Ì̸2Ž‘ÀÖ,‘ËMØ:×CŽ‘ùÖ,‘ËMØ8‘
ÿþ×RJ:CŽ–"	Ö,‘ËMØ9‘
ÿþ×RJ:CŽ“Ö,‘ËMó3TqÔ����
���lasy10Þ2Ÿ
Ý߸(¹m;a¸)Ž‘}×CŽ‘-ˆîÖ,›ËMand‘ÃwÞ3Ÿ
Ý߸(¹m;a¸)Ž‘}×CŽ‘1ÍÖare–Ãwconcept“terms,˜and“×RŸ
Ì̸1Ž‘ŸØu‘Z›×RŸ
Ì̸2Ž‘ÀÖ,Ž¡‘ͼ×RJŸû¥2ó¾KÈ�������cmsy8º�¸1Ž‘uÆÖ,‘ê¨×RJŸ›„�º��ÆŽ‘�ÜП×xCŽŽŽ‘ý­Ö,‘ê¨Þ2Ÿ
Ý߸(¹m;a¸)Ž‘}×RŽ‘1YÖand‘ê¨Þ3Ÿ
Ý߸(¹m;a¸)Ž‘}×RŽ‘1á§Öare–ê¨role“terms.Ž¡‘m°Th•¬rus›ZÖw“e˜are˜no“w˜able˜to˜describSŽe˜the˜sen“tences˜of˜our˜language˜MoSŽd-ØALC‘Öwhic“hŽ¡‘ͼare–ê¨divided“in¬rto“Ùterminolo–ÿffgic“al›35sentenc“es‘è…Öand‘ê¨Ùassertional˜sentenc“esÖ.Ž¡‘ͼIf–AÒ×CŸ
Ì̸1Ž›
ÖÖand“×CŸ
Ì̸2Ž˜Öare“concepts“and“×RŸ
Ì̸1Ž˜Öand“×RŸ
Ì̸2Ž˜Öare“roles“then“×CŸ
Ì̸1Ž–VØv›UR×CŸ
Ì̸2Ž‘ÀÖ,‘c—×CŸ
Ì̸1Ž“ؘ×CŸ
Ì̸2Ž‘ÀÖ,‘c—×RŸ
Ì̸1Ž“Øv˜×RŸ
Ì̸2Ž‘ÀÖ,Ž¡‘ͼ×RŸ
Ì̸1Ž‘VØ‘UR×RŸ
Ì̸2Ž‘ª¬Öare–ê¨terminological“sen¬rtences.Ž¡‘ͼIf–Åý×C‘¢›Öis“a“concept,›ÍS×R‘ßGÖis“a“role,˜and“×OSŽÖ,˜×OŸ
Ì̸1Ž‘ÀÖ,˜and“×OŸ
Ì̸2Ž‘†
Öare“individual“ob‘�§jects“then“×O‘¨àØ2‘UR×CŽ¡‘ͼÖand›¾û(×OŸ
Ì̸1Ž–À×;‘
ÿþOŸ
Ì̸2Ž“Ö)–rwØ2“×R‘ØEÖare˜assertional˜sen•¬rtences.‘
µÚMoreo“v“er,‘4if˜˜is˜a˜terminologicalŽ¡‘ͼ(respSŽectivš¬rely–z%assertional)“sen˜tence“and“if“×m“Öis“a“mošSŽdal“op˜erator“name“and“×a“Öis“anŽ¡‘ͼagenš¬rt's–name“then“Þ2Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽ‘/#–and“Þ3Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽ‘/¬#are“terminological“(respSŽectiv˜ely“assertional)Ž¡‘ͼsen¬rtences.Ž¡‘m°So–‰far“the“syn¬rtax“of“MošSŽd-ØALC‘žÖhas“b˜een“describ˜ed.‘°‚Noš¬rw“w˜e“ha˜v˜e“to“pro˜vide“itsŽ¡‘ͼseman¬rtics.Ž©ø÷‘ͼÛDenition–€�1“(ÖÛ-Structures)ŽŽŽ¡‘ͼÖAs–Ææusual“wš¬re“dene“a“Ù-structur‘ÿffe“Öas“a“pair“(ØDUV×;‘
ÿþØI‘�âÈÖ)“whic˜h“consists“of“a“domain“ØD‘<ÖandŽ¡‘ͼan–ºðinš¬rterpretation“function“ØI‘¸Öwhic˜h“maps“the“individual“ob‘�§jects“to“elemen˜ts“of“ØDUVÖ,Ž¡‘ͼprimitivš¬re–ê¨concepts“to“subsets“of“ØD‘?þÖand“the“primitiv˜e“roles“to“subsets“of“ØD‘ÿþ‘ª¨DUVÖ.ŽŸ´~‘ͼÛDenition–€�2“(F‘þà�rames“and“In �terpretations)ŽŽŽ¡‘ͼÖBy–ê¨a“frame“ØFŽ‘õNÖwš¬re“understand“an˜y“pair“(ØWŽ‘××;‘
ÿþØ<Ö)“whereŽ¦‘M«ØŽŽŽ‘*-¨WŽ‘:ï^Öis–ê¨a“non-emptš¬ry“set“(of“w˜orlds).ŽŸ¤&‘M«ØŽŽŽ‘*-¨<–\_Ö=“Ÿ÷ÿüóCú±u�
���
���cmex10ëCUŽ‘
±¶Ÿ€¹mº2M¹;aº2AŽ‘:Õ†Ø<Ÿû¥2¹aŽŸRAmŽŽ‘
 ^Öwhere–šthe“Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ's“are“binary“relation“on“ØWŽ‘ò¨Ö,‘gÖthe“so-calledŽ¡‘*-¨Ùac–ÿffc“essibility‘35r“elations›ê¨ÖbSŽet•¬rw“een˜w“orlds.Ž¦‘ͼBy–ê¨a“-inš¬rterpretation“Ø=“Öbased“on“ØFŽ‘õNÖw˜e“understand“an˜y“tuple“(ØDŽ‘	—×;‘
ÿþØFŽ‘ü×;‘
ÿþØ=Ÿ
Ì̸lo<rcŽŽ‘Ê´×;‘
ÿþÖ)“whereŽ¦‘M«ØŽŽŽ‘*-¨DŽ‘7¯^Ödenotes–ê¨the“common“domain“of“all“-structures“in“the“range“of“Ø=Ÿ
Ì̸lo<rcŽŽ‘µ^Ö.Ž¤¤&‘M«ØŽŽŽ‘*-¨×–ê¨Ödenotes“the“actual“wš¬rorld“(the“curren˜t“situation)Ž¡‘M«ØŽŽŽ‘*-¨FŽ‘78NÖis–ê¨a“frameŽ¡‘M«ØŽŽŽ‘*-¨=Ÿ
Ì̸lo<rcŽŽ‘C“æÖmaps–›ˆwš¬rorlds“to“-structures“with“common“domain“ØDŽ‘ÎÖwhic˜h“in˜terpretŽ¤
Æc‘*-¨agen¬rts'–ê¨names“equally‘ÿV.ŽŸ´~‘ͼÛDenition–€�3“(In �terpretation“of“T‘þà�erms)ŽŽŽ¡‘ͼÖLet›‹þØ=–URÖ=“(ØDŽ‘	—×;‘
ÿþØFŽ‘ü×;‘
ÿþØ=Ÿ
Ì̸lo<rcŽŽ‘Ê´×;‘
ÿþÖ)˜bSŽe˜a˜-in¬rterpretation˜and˜let˜Ø=Ÿ
Ì̸lo<rcŽŽ‘V´Ö(×Ö)“=“(ØDUV×;‘
ÿþØI‘�âÈÖ).‘RW‘ÿVe˜dene˜theŽ¡‘ͼinš¬rterpretation–ê¨of“terms“inductiv˜ely“o˜v˜er“their“structure:ŽŸ,òoŸë±‘7­ÎØ=Ö(×C‘�ÜžÖ)Ž‘{!u=Ž’�ŽDýØI‘�âÈÖ(×C‘�ÜžÖ)ŽŽŽ¤
Æb‘7­ÎØ=Ö(×RJÖ)Ž‘{!u=Ž’�ŽDýØI‘�âÈÖ(×RJÖ)ŽŽ¡‘7­Îif–ê¨×C‘ÇFÖ(×RJÖ)“is“a“primitiv¬re“concept“(role)ŽŽŽ¡‘7­ÎØ=Ö(×CŸ
Ì̸1Ž‘j¬Øu‘ª¨×CŸ
Ì̸2Ž‘ÀÖ)Ž‘{!u=Ž’�ŽDýØ=Ö(×CŸ
Ì̸1Ž›ÀÖ)–ª¨Ø\“=Ö(×CŸ
Ì̸2Ž˜Ö)ŽŽŽŽŽŽŒ‹�����������������������������������������
Ò ´î; ýW
 Šõ덠ýÜÍ0ŸºáZ‘1`ÈØ=Ö(×CŸ
Ì̸1Ž‘j¬Øt‘ª¨×CŸ
Ì̸2Ž‘ÀÖ)Ž‘wu*=Ž’�Š˜²Ø=Ö(×CŸ
Ì̸1Ž›ÀÖ)–ª¨Ø[“=Ö(×CŸ
Ì̸2Ž˜Ö)ŽŽ¤
Æb‘1`ÈØ=Ö(Ø:×CŽ‘D¬Ö)Ž‘wu*=Ž’�Š˜²ØDŽ’�–Úhn‘ª¨=Ö(×C‘�ÜžÖ)ŽŽ¡‘1`ÈØ=Ö(Ø8‘
ÿþ×RJ:CŽ‘=µÖ)Ž‘wu*=Ž’�Š˜²Øf×d–URØ2“DŽ‘A²j“×e“Ø2“=Ö(×C‘�ÜžÖ)–ê¨for“all“×e“Öwith“(×d;‘
ÿþeÖ)–URØ2“=Ö(×RJÖ)Ž’�È	ØgŽŽ¡‘1`È=Ö(Ø9‘
ÿþ×RJ:CŽ‘=µÖ)Ž‘wu*=Ž’�Š˜²Øf×d–URØ2“DŽ‘A²j“×e“Ø2“=Ö(×C‘�ÜžÖ)–ê¨for“some“×e“Öwith“(×d;‘
ÿþeÖ)–URØ2“=Ö(×RJÖ)Ž’�šæïØgŽŽ¡‘1`È=Ö(Þ2Ÿ
Ý߸(¹m;a¸)Ž‘}×CŽ‘)½¡Ö)Ž‘wu*=Ž’�Š˜²Øf×d–URØ2“DŽ‘A²j“×d“Ø2“=Ö[×Ö](×C‘�ÜžÖ)–ê¨for“all“דÖwith“Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×;‘
ÿþÖ)Ž‘wkùØgŽŽ¡‘1`È=Ö(Þ3Ÿ
Ý߸(¹m;a¸)Ž‘}×CŽ‘*F.Ö)Ž‘wu*=Ž’�Š˜²Øf×d–URØ2“DŽ‘A²j“×d“Ø2“=Ö[×Ö](×C‘�ÜžÖ)–ê¨for“some“דÖwith“Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×;‘
ÿþÖ)Ž’�„ŠßØgŽŽ¡‘1`È=Ö(×RŸ
Ì̸1Ž‘j¬Øu‘ª¨×RŸ
Ì̸2Ž‘ÀÖ)Ž‘wu*=Ž’�Š˜²Ø=Ö(×RŸ
Ì̸1Ž›ÀÖ)–ª¨Ø\“=Ö(×RŸ
Ì̸2Ž˜Ö)ŽŽ¡‘1`ÈØ=Ö(×RJŸû¥2º�¸1Ž‘uÆÖ)Ž‘wu*=Ž’�Š˜²ØfÖ(×x;‘
ÿþyšn9Ö)–URØ2“DŽ–—‘ª¨DŽ“j–URÖ(×y˜;‘
ÿþxÖ)“Ø2“=Ö(×RJÖ)ØgŽŽ¡‘1`È=Ö(×RJŸ›„�º��ÆŽ‘�ÜП×xCŽŽŽ‘Ö)Ž‘wu*=Ž’�Š˜²ØfÖ(×x;‘
ÿþyn9Ö)–URØ2“=Ö(×RJÖ)“Øj“×y‘ËØ2“=Ö(×C‘�ÜžÖ)ØgŽŽ¡‘1`È=Ö(Þ2Ÿ
Ý߸(¹m;a¸)Ž‘}×RŽ‘)ƒÊÖ)Ž‘wu*=Ž’�Š˜²ØfÖ(×x;›
ÿþyn9Ö)–URØj“Ö(×x;˜yn9Ö)“Ø2“=Ö[×Ö](×RJÖ)–ê¨for“all“דÖwith“Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×;˜Ö)Ž‘wkùØgŽŽ¡‘1`È=Ö(Þ3Ÿ
Ý߸(¹m;a¸)Ž‘}×RŽ‘*WÖ)Ž‘wu*=Ž’�Š˜²ØfÖ(×x;›
ÿþyn9Ö)–URØj“Ö(×x;˜yn9Ö)“Ø2“=Ö[×Ö](×RJÖ)–ê¨for“some“דÖwith“Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×;˜Ö)Ž’�„ŠßØgŽŽŽŽŸYC‘ͼÖwhere‘ê¨Ø=Ö[×Ö]–UR=“(ØDŽ‘	—×;‘
ÿþØFŽ‘ü×;‘
ÿþØ=Ÿ
Ì̸lo<rcŽŽ‘Ê´×;‘
ÿþÖ)Ž©Æc‘ͼÛDenition–€�4“(Satisabilit �y)ŽŽŽ¤
Æc‘ͼÖLet›ªØ=–URÖ=“(ØDŽ‘	—×;‘
ÿþØFŽ‘ü×;‘
ÿþØ=Ÿ
Ì̸lo<rcŽŽ‘Ê´×;‘
ÿþÖ)˜bSŽe˜a˜-in•¬rterpretation.‘#YW‘ÿVe˜dene˜the˜satisabilit“y˜relation˜Øj‘þ�Ö=Ž¡‘ͼinductiv•¬rely›ê¨o“v“er˜the˜structure˜of˜MoSŽd-ØALCŽ‘ËÖsen“tences:ŽŸIn܍ŸÏŠí‘QžoØ=–URj‘þ�Ö=“×CŸ
Ì̸1Ž‘VØv“×CŸ
Ì̸2ŽŽ’�¨_[ÖiŽŽ’�¼}Ø=Ö(×CŸ
Ì̸1Ž›ÀÖ)–URØ“=Ö(×CŸ
Ì̸2Ž˜Ö)ŽŽ¤
Æb‘QžoØ=–URj‘þ�Ö=“×CŸ
Ì̸1Ž‘VØ“×CŸ
Ì̸2ŽŽ’�¨_[ÖiŽŽ’�¼}Ø=Ö(×CŸ
Ì̸1Ž›ÀÖ)–UR=“Ø=Ö(×CŸ
Ì̸2Ž˜Ö)ŽŽ¡‘QžoØ=–URj‘þ�Ö=“×RŸ
Ì̸1Ž‘VØv“×RŸ
Ì̸2ŽŽ’�¨_[ÖiŽŽ’�¼}Ø=Ö(×RŸ
Ì̸1Ž›ÀÖ)–URØ“=Ö(×RŸ
Ì̸2Ž˜Ö)ŽŽ¡‘QžoØ=–URj‘þ�Ö=“×RŸ
Ì̸1Ž‘VØ“×RŸ
Ì̸2ŽŽ’�¨_[ÖiŽŽ’�¼}Ø=Ö(×RŸ
Ì̸1Ž›ÀÖ)–UR=“Ø=Ö(×RŸ
Ì̸2Ž˜Ö)ŽŽ¡‘QžoØ=–URj‘þ�Ö=“×x“Ø2“×CŽ’�¨_[ÖiŽŽ’�¼}ØI‘�âÈÖ(×xÖ)–URØ2“=Ö(×C‘�ÜžÖ)ŽŽ¡‘QžoØ=–URj‘þ�Ö=“(×x;‘
ÿþyn9Ö)“Ø2“×RŽ’�¨_[ÖiŽŽ’�¼}(ØI–�âÈÖ(×xÖ)×;‘
ÿþØI“Ö(×yn9Ö))–URØ2“=Ö(×RJÖ)ŽŽ¡‘QžoØ=–URj‘þ�Ö=“Þ2Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽŽ’�¨_[iŽŽ’�¼}Ø=Ö[×Ö]–URØj‘þ�Ö=“–ê¨for“ev¬rery“דÖwith“Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×;‘
ÿþÖ)ŽŽŽ¡‘QžoØ=–URj‘þ�Ö=“Þ3Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽŽ’�¨_[iŽŽ’�¼}Ø=Ö[×Ö]–URØj‘þ�Ö=“–ê¨for“some“דÖwith“Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×;‘
ÿþÖ)ŽŽŽŽŽŸJn܍‘ͼÛDenition‘€�5ŽŽŽ¡‘ͼÖLet–_gØ=“ÖbšSŽe“an“in¬rterpretation“and“let““b˜e“a“Mo˜d-ØALCŽ‘?×Ösen¬rtence“with“Ø=–	j‘þ�Ö=“.‘—ThenŽ¡‘ͼwš¬re–2call““Ùsatisable‘ÄÖand“w˜e“call“Ø=“Öa“Ùmo‘ÿffdel‘p§Öfor“.‘#If“all“in˜terpretations“are“moSŽdelsŽ¡‘ͼfor–’c“then“wš¬re“call““a“Ùthe–ÿffor“emÖ.‘0An˜y–’csen˜tence“for“whic˜h“no“moSŽdel“exists“is“calledŽ¡‘ͼÙunsatisableÖ.‘8àTh¬rus,–ꨓis“a“theorem“i“its“negation“is“unsatisable.Ž¡‘m°Let–GÎ×T‘é”ÖbšSŽe“a“set“of“Mo˜d-ØALCŽ‘(>Ösenš¬rtences.‘PRW‘ÿVe“sa˜y“×T‘é”Ùentails“Ö,›_written“×T‘•¥Øj‘þ�Ö=‘óß,˜iŽ¡‘ͼev¬rery–ê¨mošSŽdel“of“×T‘ŒnÖis“a“mo˜del“of“.Ž¦‘ͼSo–‘Ãfar“wš¬re“did“not“consider“an˜y“spšSŽecial“prop˜erties“of“the“giv¬ren“mo˜dal“op˜erators.Ž¡‘ͼTš¬rypical–tAaxiom“sc˜hemata“whic˜h“re
ect“suc˜h“pSŽoten˜tial“additional“propSŽerties“are“listedŽ¡‘ͼbSŽelo¬rw.ŽŸ9쿍‘/ÿiŸÓy§‰��ff
dg;¤	¤uÌÍŸ!í„�
Æb��ff‘!ƒfŸûÞAxiom‘ê¨Sc¬rhemaŽ’�¹„�
Æb��ffŽ’�ã®PropSŽert¬ryŽ’
d4Ÿ!í„�
Æb��ffŽŽ©ˆS‰��ff
dg;¡Ìͤ!í„�
Æb��ff‘MŸûÞÞ2Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽ‘A˜CŸûÞØ)‘URÞ3Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽ‘B С„�
Æb��ffŽ’�ÕŒ”Ø8×xØ9×y‘ËØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×x;‘
ÿþyn9Ö)‘E9çŸ!í„�
Æb��ffŽŽ¤
ÆbÌͤ!í„�
Æb��ff‘%ÎPŸûÞÞ2Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽ‘RŸûÞØ)‘URÖ‘%ÎP¡„�
Æb��ffŽ’�Û´ Ø8×x‘URØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×x;‘
ÿþxÖ)‘KasŸ!í„�
Æb��ffŽŽ¡Ìͤ!í„�
Æb��ff‘MŸûÞ–URØ)“Þ2Ÿ
Ý߸(¹m;a¸)Ž–}Þ3Ÿ
Ý߸(¹m;a¸)Ž“ÖŽŽ‘b™Æ¡„�
Æb��ffŽ’�¶ôxØ8×x;–
ÿþy‘ËØ<Ÿû¥2¹aŽŸRAmŽŽ›ÄÖ(×x;“yn9Ö)–URØ)“<Ÿû¥2¹aŽŸRAmŽŽ˜Ö(×yn9;‘
ÿþxÖ)‘&¡ËŸ!í„�
Æb��ffŽŽ¡Ìͤ!í„�
Æb��ff‘UZŸûÞÞ2Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽ‘1 ŸûÞØ)‘URÞ2Ÿ
Ý߸(¹m;a¸)Ž–}Þ2Ÿ
Ý߸(¹m;a¸)Ž“ÖŽŽ‘R¡„�
Æb��ffŽ’�•zØ8×x;–
ÿþyšn9;“z‘Þ5Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×x;“y˜Ö)–ª¨Ø^“<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×y˜;›
ÿþz‘�ˆãÖ)–URØ)“<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×x;˜z‘�ˆãÖ)‘ÌÍŸ!í„�
Æb��ffŽŽ¡Ìͤ!í„�
Æb��ff‘ÌÍŸûÞÞ3Ÿ
Ý߸(¹m;a¸)Ž‘}ÖŽ‘1 ŸûÞØ)‘URÞ2Ÿ
Ý߸(¹m;a¸)Ž–}Þ3Ÿ
Ý߸(¹m;a¸)Ž“ÖŽŽ‘R¡„�
Æb��ffŽ’�•zØ8×x;–
ÿþyšn9;“z‘Þ5Ø<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×x;“y˜Ö)–ª¨Ø^“<Ÿû¥2¹aŽŸRAmŽŽ›ÄÖ(×x;‘
ÿþz‘�ˆãÖ)–URØ)“<Ÿû¥2¹aŽŸRAmŽŽ˜Ö(×yn9;‘
ÿþz‘�ˆãÖ)‘ÌÍŸ!í„�
Æb��ffŽŽ¦‰��ff
dg;ŽŽŸ<B‘i¿oT‘ÿVable–ê¨1:‘8àPropSŽerties“of“the“accessibilit¬ry“relationŽŽŽŒ‹�����������������������������������������_ ´î; ýW
 Šõ덠ýš
‘ͼÖHistorically‘ÿV,–ê¨these“propšSŽerties“are“called“×D˜Ö,“×T‘
¡ÆÖ,“×B‘�›Ö,“4,“and“5“resp˜ectiv¬rely‘ÿV.Ž¤
Æc‘m°If–Ädw¬re“consider“mošSŽdal“op˜erators“for“b˜elief,›:Ói.e.“Þ2Ÿ
Ý߸(¹belKievI{e;a¸)Ž‘-+úÖand“Þ3Ÿ
Ý߸(¹belKievI{e;a¸)Ž‘'g–Ö,˜thenŽ¡‘ͼ4–…¸and“5“are“axioms“of“in•¬rtrospSŽection.‘

In“tuitiv“ely‘ÿV,‘ì{they›…¸sa“y˜that˜the˜agen“t˜×a˜ÖhasŽ¡‘ͼcomplete–´¼insighš¬rt“what“his“o˜wn“bšSŽeliefs“are“concerned.‘
—Prop˜ert¬ry“×T‘V‚Öis“one“of“theŽ¡‘ͼma‘�§jor–5ƒc¬rharacteristics“of“mošSŽdal“op˜erators“for“kno¬rwledge,‘Y½i.e.“Þ2Ÿ
Ý߸(¹k6…now7s;a¸)Ž‘)X¹Öand“Þ3Ÿ
Ý߸(¹k6…now7s;a¸)Ž‘&#6Ö,Ž¡‘ͼbšSŽecause–ÍŸit“enables“us“to“deduce“a“fact“ab˜out“the“real“wš¬rorld“from“an“agen˜t's“kno˜wledgeŽ¡‘ͼabSŽout–ê¨the“w¬rorld.Ž©Æc‘ͼÛDenition‘€�6ŽŽ‘XoÙL›ÿffet–ù¬ØR“Ùb˜e“a“set“of“pr˜op˜erties“of“the“ac˜c˜essibility“r˜elation.‘S;A³2n“interpr˜e-Ž¡‘ͼtation–¢Ø=“Ùis“c–ÿffal‘�™™le“d–¢a“ØRÖ-in¬rterpretation“Ùif“the“ac–ÿffc“essibility›¢r“elation˜Ø<˜Ùof˜the˜underlyingŽ¡‘ͼfr›ÿffame‘Ï>ØFŽ‘¾zÙsatises–Ï>al‘�™™l“pr˜op˜erties“in“ØRÙ.‘EWe“say“a“set“of“Mo˜d-ØALCŽ‘¯®Ùsentenc˜es“×T‘qÙentailsŽ¡‘ͼÖ–éÙin“al›�™™l“ØRÙ-interpr‘ÿffetations“if“al˜l“ØR“Ùinterpr›ÿffetations“which“ar˜e“mo˜dels“of“×T‘ŠÌÙar˜e“alsoŽ¡‘ͼmo‘ÿffdels–35of“ÖÙ.Ž¦‘ͼÖWhat–1ois“remark‘ÿXäable“for“the“propšSŽerties“from“ab˜o•¬rv“e–1ois“that“they“all“are“rst-orderŽ¡‘ͼpropšSŽerties.‘¼%Therefore–k¿it“is“not“to˜o“surprising“that“a“translation“of“mo˜dal“termino-Ž¡‘ͼlogical–
¨and“mošSŽdal“assertional“axioms“in¬rto“rst-order“predicate“logic“can“b˜e“done“v¬reryŽ¡‘ͼeasily‘ÿV.ŽŸ&û¸‘ͼç3Ž‘*œŠT‘þXranslating–Ÿ¼Mo‘�Od-æALCŽ‘*rJçin‘ÿr°to“Classical“LogicŽŸ¨†‘ͼÖThere›üØha•¬rv“e˜b•SŽeen˜a˜lot˜of˜prop“osals˜for˜correct˜and˜complete˜calculi˜for˜nonclassicalŽ¡‘ͼlogics–ê¨|“tempSŽoral“logicsŸû¥2¸13Ž‘	�Ö,“epistemic“logicsŸû¥2¸9Ž‘ÀÖ,“etc.“|“and“terminological“logicsŸû¥2¸3Ž‘@Ÿû¥2¹;“¸5ŽŽ‘G$Ö.Ž¡‘m°Unfortunately‘ÿV,‘H2these–”calculi“require“implemenš¬rtations“for“their“respSŽectiv˜e“theoremŽ¡‘ͼproš¬rving–u­system“with“hardly“a“c˜hance“to“apply“results“and“tec˜hniques“of“the“tradi-Ž¡‘ͼtional–˜äwš¬rork“on“automated“theorem“pro˜ving.‘C“Therefore,‘Ärw˜e“follo˜w“the“approac˜h“ofŽ¡‘ͼOhlbac¬rhŸû¥2¸12Ž‘
¢ãÖto–¢Ûeliminate“mošSŽdal“op˜erators“in“a“w•¬ra“y–¢Ûthat“w¬re“get“standard“rst-orderŽ¡‘ͼpredicate–ê¨logic“formš¬rulae“that“still“represen˜t“the“moSŽdal“seman˜tics.Ž¡‘m°In–½this“section“wš¬re“dene“suc˜h“a“logic“morphism“that“maps“MoSŽd-ØALCŽ‘ó-Öin˜to“rst-Ž¡‘ͼorder–ê¨predicate“logic.Ž¡‘m°First,‘}³wš¬re–bvtransform“all“concepts“and“roles“whic˜h“oSŽccur“in“a“giv˜en“kno˜wledge“baseŽ¡‘ͼin¬rto›Z_Ùne‘ÿffgation–™änormal“formÖ,‘vMi.e.˜in˜a˜form˜where˜no˜implication˜or˜equiv‘ÿXäalence˜signŽ¡‘ͼošSŽccurs–.úand“where“all“negation“signs“o˜ccur“solely“in“fronš¬rt“of“the“primitiv˜e“concepts.Ž¡‘ͼThis–¸÷can“bšSŽe“p˜erformed“in“a“straigh•¬rtforw“ard–¸÷manner“as“kno¬rwn“from“classical“logicŽ¡‘ͼand–Bçtherefore“the“tecš¬rhnical“details“are“omitted“here.‘AžIn“the“sequel“w˜e“assume“thatŽ¡‘ͼanš¬ry–ê¨(terminological“or“assertional)“sen˜tence“is“already“in“negation“normal“form.Ž¡‘m°No•¬rw›FDw“e˜translate˜the˜terminological˜and˜assertional˜sen“tences˜in“to˜rst-orderŽ¡‘ͼlogic–ê¨form¬rulae“using“the“function“[–þK…[‘	ʉ��ff�†fŽŽ‘
å‚]“]Ž‘õd.ŽŸ<¹Œ‘±rŸÓ¬Ú‰��ff
…)¤	¤uÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞAxiomŽ‘{p§„�
Æb��ffŽ’�€×
T‘ÿVranslationŽ’
„œÃŸ!í„�
Æb��ffŽŽŸˆS‰��ff
…)¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞ[–þK…[‘URÞ2Ÿ
Ý߸(¹m;a¸)Ž‘×MŸ
Ì̸2Ž‘À×:–
ÿþ:“:Ž‘Š MŸ
Ì̹nŽ‘¨PÖŽ‘`]“]Ÿ
Ì̹UŽŽ‘{p§„�
Æb��ffŽ’�€×
Ø8×V‘ñÂÖ:–URØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×Uò¬;›
ÿþV‘œpÖ)“Ø)“Ö[‘þK…[“×MŸ
Ì̸2Ž‘À×:˜:˜:Ž‘Š MŸ
Ì̹nŽ‘¨PÖŽ‘B]‘þK…]Ÿ
Ì̹VŽŽ’�©çiŸ!í„�
Æb��ffŽŽ¤
ÆbÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘URÞ3Ÿ
Ý߸(¹m;a¸)Ž‘×MŸ
Ì̸2Ž‘À×:–
ÿþ:“:Ž‘Š MŸ
Ì̹nŽ‘¨PÖŽ‘a‘]“]Ÿ
Ì̹UŽŽ‘{p§„�
Æb��ffŽ’�€×
Ø9×V‘ñÂÖ:›URØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×Uò¬;‘
ÿþV‘œpÖ)–ª¨Ø^“Ö[–þK…[˜×MŸ
Ì̸2Ž‘À×:–
ÿþ:“:Ž‘Š MŸ
Ì̹nŽ‘¨PÖŽ‘B]“]Ÿ
Ì̹VŽŽ’�®’Ÿ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[–UR×CŸ
Ì̸1Ž‘VØv“×CŸ
Ì̸2ŽŽ‘0úÁÖ]“]Ÿ
Ì̹UŽŽ‘{p§„�
Æb��ffŽ’�€×
Ø8‘
ÿþ×X‘FÕÖ:–UR[›þK…[“×CŸ
Ì̸1ŽŽ‘ÒµÖ]˜]Ÿ
Ì̹UèZ;XŽŽ‘4E
Ø)–URÖ[›þK…[“×CŸ
Ì̸2ŽŽ‘ÒµÖ]˜]Ÿ
Ì̹UèZ;XŽŽ’�©‹3Ÿ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[–UR×CŸ
Ì̸1Ž‘VØ“×CŸ
Ì̸2ŽŽ‘0úÁÖ]“]Ÿ
Ì̹UŽŽ‘{p§„�
Æb��ffŽ’�€×
Ö[–þK…[–UR×CŸ
Ì̸1Ž‘VØv“×CŸ
Ì̸2ŽŽ‘0úÁÖ]“]Ÿ
Ì̹UŽŽ’�Å;òØ^‘ª¨Ö[–þK…[–UR×CŸ
Ì̸2Ž‘VØv“×CŸ
Ì̸1ŽŽ‘0úÁÖ]“]Ÿ
Ì̹UŽŽ’�·`П!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[–UR×RŸ
Ì̸1Ž‘VØv“×RŸ
Ì̸2ŽŽ‘2
»Ö]“]Ÿ
Ì̹UŽŽ‘{p§„�
Æb��ffŽ’�€×
Ø8–
ÿþ×XJg;“Y‘ñÂÖ:–UR[›þK…[“×RŸ
Ì̸1ŽŽ‘\2Ö]˜]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘DLØ)–URÖ[›þK…[“×RŸ
Ì̸2ŽŽ‘\2Ö]˜]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ’�‹¦ÙŸ!í„�
Æb��ffŽŽŽŽŽŽŒ‹�����������������������������������������2h ´î; ýW
 Šõ덠ý¥æۍŸñǯ‘!Æ·Ÿ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[–UR×RŸ
Ì̸1Ž‘VØ“×RŸ
Ì̸2ŽŽ‘2
»Ö]“]Ÿ
Ì̹UŽŽ‘v߸„�
Æb��ffŽ’�ž@Ö[–þK…[–UR×RŸ
Ì̸1Ž‘VØv“×RŸ
Ì̸2ŽŽ‘2
»Ö]“]Ÿ
Ì̹UŽŽ’�ã·çØ^‘ª¨Ö[–þK…[–UR×RŸ
Ì̸2Ž‘VØv“×RŸ
Ì̸1ŽŽ‘2
»Ö]“]Ÿ
Ì̹UŽŽ’�¶MÖŸ!í„�
Æb��ffŽŽ¤
Æb‘!Æ·Ÿ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[–UR×a“Ø2“×AŽ‘$O3Ö]“]Ÿ
Ì̹UŽŽ‘v߸„�
Æb��ffŽ’�ž@Ö[›þK…[–UR×A“Ö]˜]Ÿ
Ì̹UèZ;aŽŽ’
¢¾Ÿ!í„�
Æb��ffŽŽ¡‘!Æ·Ÿ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[–UR(×a;‘
ÿþbÖ)“Ø2“×PŽ‘8áÖ]“]Ÿ
Ì̹UŽŽŽ‘v߸„�
Æb��ffŽ’�ž@Ö[–þK…[‘UR×P‘÷Ö]“]Ÿ
Ýß¹UèZ;¸(¹a;b¸)ŽŽŽ’
¢¾Ÿ!í„�
Æb��ffŽŽ‘!ùꟈS‰��ff
€r:ŽŽŸ!²‘ͼÖwhere–ê¨the“translation“of“concepts“and“roles“is“dened“b¬ry:ŽŸzqÿ‘ž[Ÿ•I»‰��ff
…)X¤	¤uÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞT‘ÿVermŽ‘{–Ö„�
Æb��ffŽ’�€ý<T‘ÿVranslationŽ’
„ÂòŸ!í„�
Æb��ffŽŽ©ˆS‰��ff
…)X¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞ[–þK…[‘UR×AŸ
Ì̸1ŽŽ‘9‘Ö]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<×AŸ
Ì̸1Ž‘ÀÖ(×Uò¬;‘
ÿþX‘�ñƒÖ)’�Õ07Ÿ!í„�
Æb��ffŽŽ¤
ÆbÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞ[–þK…[‘URØ:×AŸ
Ì̸1ŽŽ‘9’Ö]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ø:×AŸ
Ì̸1ŽŽ’�–Œ*Ö(×Uò¬;‘
ÿþX‘�ñƒÖ)’�Í06Ÿ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞ[–þK…[‘UR×CŸ
Ì̸1Ž‘j¬Øu‘ª¨×:–
ÿþ:“:Ž‘ðØu‘ª¨×CŸ
Ì̹kŽŽ‘IÓ–Ö]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ö[–þK…[‘UR×CŸ
Ì̸1ŽŽ‘ÒµÖ]“]Ÿ
Ì̹UèZ;XŽŽ’�±BJØ^‘ª¨×:–
ÿþ:“:Ž‘ðØ^‘ª¨Ö[–þK…[‘UR×CŸ
Ì̹kŽŽ‘6CÖ]“]Ÿ
Ì̹UèZ;XŽŽ’�°`¶Ÿ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘UR×CŸ
Ì̸1Ž‘j¬Øt‘ª¨×:–
ÿþ:“:Ž‘ðØt‘ª¨×CŸ
Ì̹kŽŽ‘IÓ–Ö]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ö[–þK…[‘UR×CŸ
Ì̸1ŽŽ‘ÒµÖ]“]Ÿ
Ì̹UèZ;XŽŽ’�±BJØ_‘ª¨×:–
ÿþ:“:Ž‘ðØ_‘ª¨Ö[–þK…[‘UR×CŸ
Ì̹kŽŽ‘6CÖ]“]Ÿ
Ì̹UèZ;XŽŽ’�°`¶Ÿ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘URØ8‘
ÿþ×RJ:CŽ‘$èYÖ]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ø8×Y‘ñÂÖ:–UR[›þK…[“×R‘nœÖ]˜]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘?x’Ø)–URÖ[›þK…[“×C‘1ðÖ]˜]Ÿ
Ì̹UèZ;YŽŽ’�¡›îŸ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘URØ9‘
ÿþ×RJ:CŽ‘$èYÖ]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ø9×Y‘ñÂÖ:–UR[›þK…[“×R‘nœÖ]˜]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘>ÍèØ^‘ª¨Ö[–þK…[‘UR×C‘1ðÖ]“]Ÿ
Ì̹UèZ;YŽŽ’�¦F™Ÿ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘URÞ2Ÿ
Ý߸(¹m;a¸)Ž‘}×CŽ‘0hEÖ]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ø8×V‘ñÂÖ:–URØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×Uò¬;‘
ÿþV‘œpÖ)“Ø)“Ö[›þK…[“×C‘1ðÖ]˜]Ÿ
Ì̹Vxä;XŽŽ’�©çiŸ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘URÞ3Ÿ
Ý߸(¹m;a¸)Ž‘}×CŽ‘0ðÒÖ]“]Ÿ
Ì̹UèZ;XŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ø9×V‘ñÂÖ:›URØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×Uò¬;‘
ÿþV‘œpÖ)–ª¨Ø^“Ö[–þK…[˜×C‘1ðÖ]“]Ÿ
Ì̹Vxä;XŽŽ’�®’Ÿ!í„�
Æb��ffŽŽ¦‰��ff
…)XŸ	¤uÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘UR×P‘÷Ö]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<×P‘
¡ÆÖ(×Uò¬;–
ÿþXJg;“Y‘œpÖ)’�Ë€qŸ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞ[–þK…[‘UR×RŸ
Ì̸1Ž‘j¬Øu‘ª¨×:–
ÿþ:“:Ž‘ðØu‘ª¨×RŸ
Ì̹lŽŽ‘HäÆÖ]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ö[–þK…[‘UR×RŸ
Ì̸1ŽŽ‘\2Ö]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ’�ÁŒØ^‘ª¨×:–
ÿþ:“:Ž‘ðØ^‘ª¨Ö[–þK…[‘UR×RŸ
Ì̹lŽŽ‘½öÖ]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ’� †tŸ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘UR×RJŸû¥2º�¸1ŽŽ‘ôÖ]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ö[–þK…[‘UR×R‘nœÖ]“]Ÿ
Ýß¹UèZ;¸(¹Yxä;X‘�ŸÒ¸)ŽŽ’
„ÂòŸ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘UR×RJŸ›„�º��ÆŽ‘�ÜП×xCŽŽŽ‘½©Ö]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ö[–þK…[‘UR×R‘nœÖ]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ’�¼uÒØ^‘ª¨Ö[–þK…[‘UR×C‘1ðÖ]“]Ÿ
Ì̹UèZ;YŽŽ’�ÀMŸ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘URÞ2Ÿ
Ý߸(¹m;a¸)Ž‘}×RŽ‘0.nÖ]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ø8×V‘ñÂÖ:–URØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×Uò¬;‘
ÿþV‘œpÖ)“Ø)“Ö[›þK…[“×R‘nœÖ]˜]Ÿ
Ýß¹Vxä;¸(¹X&î;Y‘
㐸)ŽŽ’�©çiŸ!í„�
Æb��ffŽŽ¡ÌÍŸ!í„�
Æb��ff‘ÌÍŸûÞÖ[–þK…[‘URÞ3Ÿ
Ý߸(¹m;a¸)Ž‘}×RŽ‘0¶ûÖ]“]Ÿ
Ýß¹UèZ;¸(¹X&î;Y‘
㐸)ŽŽŽ‘{–Ö„�
Æb��ffŽ’�€ý<Ø9×V‘ñÂÖ:›URØ<Ÿû¥2¹aŽŸRAmŽŽ‘ÄÖ(×Uò¬;‘
ÿþV‘œpÖ)–ª¨Ø^“Ö[–þK…[˜×R‘nœÖ]“]Ÿ
Ýß¹Vxä;¸(¹X&î;Y‘
㐸)ŽŽŽ’
„ÂòŸ!í„�
Æb��ffŽŽ¦‰��ff
…)XŽŽŸ{«‘ͼÖTh•¬rus›fägiv“en˜an“y˜MoSŽd-ØALCŽ‘àpÖ-form“ula˜,‘…ôthe˜result˜of˜the˜abSŽo“v“e˜translation,‘…ô[›þK…[–UR“]˜]Ÿ
Ì̹ŽŽ‘%¨ÊÖisŽ¤
Æc‘ͼa–tYrst-order“predicate“logic“formš¬rula“whic˜h“can“easily“bSŽe“transformed“in˜to“clauseŽ¡‘ͼnormal–Žform“with“the“help“of“the“w•¬rell-kno“wn–Žstandard“tec¬rhniques.‘†“The“translationŽ¡‘ͼof–O(a“knoš¬rwledge“base“is“completed“b˜y“adding“a“suitable“set“ØK‘{ˆÖof“propSŽerties“from“tableŽ¡‘ͼ1.Ž¡‘m°In–xTorder“to“pro•¬rv“e–xTthat“a“mošSŽdal“terminological“or“mo˜dal“assertional“axiom““isŽ¡‘ͼsatisable–¯in“anš¬ry“moSŽdel“of“a“kno˜wledge“base“ØB]mÖ,‘»w˜e“ha˜v˜e“to“sho˜w“the“unsatisabilit˜yŽ¡‘ͼof‘ô·[–þK…[‘URØB‘²¿Ö]“]Ž‘µ;Ø[–±K‘Ýá[“Ö[–þK…[‘URØ:ÖŽ‘']“]Ÿ
Ì̹ŽŽ‘'mtÖ.‘WEvidenš¬rtly‘ÿV,‘÷;this–ô·can“bSŽe“done“v˜ery“easily“with“the“help“of“an˜yŽ¡‘ͼsound–Jzand“complete“theorem“pro¬rving“methoSŽd“for“classical“rst-order“predicate“logic.Ž¡‘m°Ho•¬rw“ev“er,‘aMif›>öw“e˜tak“e˜a˜closer˜lo•SŽok˜at˜the˜results˜of˜the˜translation˜describ“ed˜ab“o•¬rv“eŽ¡‘ͼwš¬re–Ícan“see“quite“a“big“problem.‘àAlready“simple“kno˜wledge“bases“result“in“ratherŽ¡‘ͼhš¬ruge–Ælclause“sets“where“man˜y“of“the“clauses“merely“express“certain“informations“abSŽoutŽ¡‘ͼaccessibilities–.Pand“role“correlations.‘×But“wš¬re“can“exploit“a“propSŽert˜y“of“the“languageŽ¡‘ͼMoSŽd-ØALCŽ‘(DÖwhicš¬rh–GÔis“t˜ypical“for“most“moSŽdal“and“terminological“logics,–_namely‘ÿV,“eac˜hŽ¡‘ͼaccessibilitš¬ry–Ãûrelation“sym˜bSŽol“or“role“sym˜bšSŽol“×R‘ÝEÖo˜ccurs“either“in“the“form“Ø9×x‘URRJÖ(×:–
ÿþ:“:Ž‘Êž;‘
ÿþxÖ)PÅØ^Ž¡‘ͼÖ(×xÖ)–ùxor“in“the“form“Ø8×x–"FRJÖ(×:–
ÿþ:“:Ž‘Êž;‘
ÿþxÖ)“Ø)“Ö(×xÖ).‘eOHo•¬rw›ùxw“e˜can˜mak“e˜use˜of˜this˜spSŽecialŽ¡‘ͼsynš¬rtactical–ê¨feature“is“explained“in“the“follo˜wing“section.ŽŸ&û¸‘ͼç4Ž‘*œŠF‘þXunctional–Ÿ¼Sim‘ÿr°ulation“of“n-ary“PredicatesŽŸ¨†‘ͼÖFirst–ê¨of“all“let“us“dene“what“wš¬re“mean“b˜y“a“Ùfunctional‘35simulatorÖ.ŽŸÆc‘ͼÛDenition–€�7“(F‘þà�unctional“Sim �ulators)ŽŽŽŽŽŒ‹�����������������������������������������E¸ ´î; ýW
 Šõ덠ýš
‘ͼÖLet–z€Ø<“ÖbSŽe“an“n-ary“relation.‘}A‘zdset“ó1߆µT�������cmtt12ÜFŸ
Ì̺<Ž‘
Öof“functions“is“called“a“Ùfunctional–Ìsimulator“forŽ©
Æc‘ͼØ<–ê¨Öif“for“an¬ry“×xŸ
Ì̸1Ž‘À×;–
ÿþ:“:“:Ž‘Êœ;‘
ÿþxŸ
Ì̹nŽŽ¤Æc‘=âÜØ<Ö(×xŸ
Ì̸1Ž–À×;–
ÿþ:“:“:Ž‘Êœ;›
ÿþxŸ
Ì̹nŽ‘¨PÖ)–ê¨i“there“exists“aŽ‘Z6„×f‘QØ2‘URÜFŸ
Ì̺<Ž‘
Ž<ÖwithŽ‘%Q¸×f‘
GÿÖ(×xŸ
Ì̸1Ž“×;˜:˜:˜:Ž‘Êœ;˜xŸ
Ì̹nº�¸1Ž‘„ÌÖ)–UR=“×xŸ
Ì̹nŽŽ¡‘ͼÖIn–ôãparticular,›&
if“Ø<“Öis“total,˜i.e.“for“anš¬ry“×xŸ
Ì̸1Ž‘À×:–
ÿþ:“:Ž‘Š xŸ
Ì̹nº�¸1Ž‘y¯Öthere“is“a“×xŸ
Ì̹nŽ‘3Ösuc˜h“that“Ø<Ö(×xŸ
Ì̸1Ž‘À×;–
ÿþ:“:“:Ž‘Êœ;‘
ÿþxŸ
Ì̹nŽ‘¨PÖ)Ž¦‘ͼthen–ê¨eac¬rh“function“in“ÜFŸ
Ì̺<Ž‘
Ž<Öis“total,“toSŽo.Ž¤Æc‘m°I.e.–Òêa“functional“simš¬rulator“for“some“relation“×R‘ì4Öis“a“set“of“functions“whic˜h“is“ableŽ¦‘ͼto–	;takš¬re“o˜v˜er“the“respSŽonsibilities“of“×RJÖ.‘í¼The“follo˜wing“lemma“sho˜ws“that“its“cardinalit˜yŽ¦‘ͼdoSŽes–ê¨not“exceed“the“cardinalitš¬ry“of“w˜orlds“under“consideration.Ž¡‘ͼÛLemma‘€�4.1ŽŽŽ¦‘ͼÖLet›ÿØ<–x“×SŸ
Ì̸1Ž‘x˜Ø‘¸”×:–
ÿþ:“:Ž‘;ÈØ‘¸”×SŸ
Ì̹nŽ‘	§jÖwhere˜eac•¬rh˜×SŸ
Ì̹iŽ‘côÖdenotes˜a˜coun“table˜sort.‘v7Then˜there˜exists˜aŽ¦‘ͼcounš¬rtable–ê¨functional“sim˜ulator“for“Ø<Ö.Ž¦‘ͼÛPro`�of:‘¿øÖSeeŸû¥2¸11Ž‘	�Ö.Ž¡‘ͼWhat–Áa“functional“simš¬rulator“is“on“the“meta-lev˜el“are“the“sim˜ulator“axioms“on“theŽ¦‘ͼob‘�§ject‘ê¨lev¬rel.Ž¡‘ͼÛDenition–€�8“(Sim �ulator“Axioms“for“T‘þà�otal“Predicates)ŽŽŽ¦‘ͼÖAccording–ê¨to“Denition“7“wš¬re“call“the“t˜w˜o“axiomsŽ¤ ÷@Ÿøލ‘F‰"SimŽŸú÷x‘Zj¹RŽŸÿû‘Zj¸1ŽŽŽ‘kýÖ=Ž‘~5…Ø8×uŸ
Ì̹iŽ›dÚ×;–
ÿþv‘ËRJÖ(×:“:“:Ž‘Êž;“uŸ
Ì̹iŽ˜×;“:“:“:Ž‘Êœ;“vn9Ö)–URØ)“9×f–
GÿÖ:›
ÿþÜFŸ
Ì̹RŽ‘
Hå×f“Ö(×:˜:˜:Ž–Êž;˜uŸ
Ì̹iŽ‘dÚ×;˜:˜:˜:Ž“Ö)–UR=“×vŽŽŸ¡ì‘F‰"ÖSimŽŸú÷x‘Zj¹RŽŸÿû‘Zj¸2ŽŽŽ‘kýÖ=Ž‘~5…Ø8×uŸ
Ì̹iŽ›dÚØ8×f‘
GÿÖ:–
ÿþÜFŸ
Ì̹RŽ‘
Hå×RJÖ(×:“:“:Ž‘Êž;“uŸ
Ì̹iŽ˜×;“:“:“:Ž‘Êœ;“f‘
GÿÖ(×:“:“:Ž‘Êž;“uŸ
Ì̹iŽ˜×;“:“:“:Ž‘ÊžÖ))ŽŽŽŽ¡‘ͼthe–MÙsimulator‘Žaxioms‘KlÖfor“the“total“predicate“×RJÖ.‘a•Note“that“in“the“case“of“non-totalŽ¦‘ͼpredicates–
ythe“denition“of“SimŸû¥2¹RŽŸRA¸2ŽŽ‘
þÖneeds“to“bšSŽe“c¬rhanged“b˜ecause“in“this“case“wš¬re“ha˜v˜eŽ¦‘ͼto–ê¨bSŽe“able“to“deal“with“partial“functions“instead“of“total“functions.Ž¦‘m°The–.collection“of“all“axioms“SimŽŸú÷x‘ÃY¹RŽŸÿû‘ÃY¸1ŽŽ›¶ìÖ,‘>ërespSŽectiv¬rely“SimŽŸú÷x‘ÃY¹RŽŸÿû‘ÃY¸2ŽŽ˜Ö,›>ëis“called“SimŽ‘ÃYŸ
Ì̸1Ž‘ƒ]Ö,˜resp•SŽesp“ec-Ž¦‘ͼtiv¬rely‘ê¨SimŽ‘ðŸ
Ì̸2Ž‘?ôÖ.Ž¤Æc‘m°Th•¬rus,‘‹2for›kan“y˜total˜(serial)˜accessibilit“y˜relation˜or˜role˜w“e˜can˜in“troSŽduce˜func-Ž¦‘ͼtional–­qsimš¬rulators.‘$xThis“allo˜ws“an“alternativ˜e“denition“for“the“translation“in˜to“rst-Ž¦‘ͼorder–ê¨predicate“logic“as“describšSŽed“b˜elo¬rw.Ž¡‘ͼÛDenition–€�9“(An“Alternativ �e“for“Ö[›þ=q[–UR“]˜]Ÿ
Ì̹ŽŽ‘!ÊÛ)ŽŽŽ¦‘ͼÖThe–£ªalternativ¬re“for“[›þK…[–UR“]˜]Ÿ
Ì̹ŽŽ›$FÖdiers“from“[›þK…[–UR“]˜]Ÿ
Ì̹ŽŽ˜Ömerely“in“the“follo¬rwing“cases“where“theŽ¦‘ͼassošSŽciated–ê¨accessibilit¬ry“relations“and“role“relations“are“assumed“to“b˜e“total.ŽŸ(ª-ŸðOœ‘n}Â[–þK…[‘URÞ3Ÿ
Ý߸(¹m;a¸)Ž‘ÖŽ‘.(•]“]Ÿû¥2¹?ŽŸRAUŽŽŽŽ’�ÒM3Ö=Ž’�åp»Ø9×V‘œpÖ:‘
ÿþÜFŸ
Ì̺<Ÿý¸äó;Î�������cmmi6°aŽŸGmŽŽŽ‘äÖ[›þK…[–UR“]˜]Ÿû¥2¹?ŽŸ™”V‘
㐸(¹U‘�Ú"¸)ŽŽŽŽŽ¤ã;‘n}ÂÖ[–þK…[‘URÞ3Ÿ
Ý߸(¹m;a¸)Ž‘}×CŽ‘0ðÒÖ]“]Ÿû¥2¹?ŽŸRAUèZ;XŽŽŽŽ’�ÒM3Ö=Ž’�åp»Ø9×V‘œpÖ:‘
ÿþÜFŸ
Ì̺<Ÿý¸ä°aŽŸGmŽŽŽ‘äÖ[–þK…[‘UR×C‘1ðÖ]“]Ÿû¥2¹?ŽŸ™”V‘
㐸(¹U‘�Ú"¸)¹;XŽŽŽŽŽ¡‘n}ÂÖ[–þK…[‘URÞ3Ÿ
Ý߸(¹m;a¸)Ž‘}×RŽ‘0¶ûÖ]“]Ÿû¥2¹?ŽŸ™”UèZ;¸(¹X&î;Y‘
㐸)ŽŽŽŽ’�ÒM3Ö=Ž’�åp»Ø9×V‘œpÖ:‘
ÿþÜFŸ
Ì̺<Ÿý¸ä°aŽŸGmŽŽŽ‘
³’Ö[–þK…[‘UR×R‘nœÖ]“]Ÿû¥2¹?ŽŸ™”V–
㐸(¹U‘�Ú"¸)¹;¸(¹X&î;Y“¸)ŽŽŽŽŽŽŽŸ(ª,‘ͼÖNote–o%that“although“the“synš¬rtax“of“the“translation“suggests“a“second-order“quan˜ti-Ž¦‘ͼcation–ê¨wš¬re“actually“do“not“go“bSŽey˜ond“rst-order“logic.ŽŽŽŒ‹�����������������������������������������]] ´î; ýW
 Šõ덠ýš
‘ͼÛLemma‘€�4.2ŽŽŽ¤
Æc‘ͼÖLet–0ñØR“ÖbSŽe“a“set“of“formš¬rulae“whic˜h“expresses“the“propSŽerties“of“the“underlying“acces-Ž¡‘ͼsibilit¬ry‘ê¨relations.‘8àThenŽ¤Æc’�‡ðÊØR–URj›þ�Ö=“[›þK…[““]˜]Ÿ
Ì̹ŽŽ‘#ûìÖiŽ‘2ÆØR–ª¨[“fÖSimŽ‘•HŸ
Ì̸2Ž‘ULØg–URj˜Ö=“[›þK…[““]˜]Ÿû™¹?ŽŸëڍŽŽŽŽ¡‘ͼÛPro`�of:‘¿øÖCan–ê¨bSŽe“found“inŸû¥2¸11ŽŽ©Æc‘m°ÖW‘ÿVe›®ãha•¬rv“e˜gained˜quite˜a˜lot˜already‘ÿV,›ñho“w“ev“er,˜under–®ãthese“preliminaries“v¬reryŽ¤
Æc‘ͼin¬rteresting–ê¨simplications“are“pSŽossible.Ž¡‘m°Note–ésthat“the“clause“form“of“sucš¬rh“a“translation“doSŽes“not“con˜tain“an˜y“pSŽositiv˜eŽ¡‘ͼoSŽccurrence–m’of“a“role“or“accessibilitš¬ry“relation“sym˜bšSŽol.‘	ÁŸThis“fact“can“b˜e“exploitedŽ¡‘ͼin–üa“vš¬rery“in˜teresting“manner.‘ØÝSince“an˜y“role“or“accessibilit˜y“relation“sym˜bSŽol“canŽ¡‘ͼonly–[©ošSŽccur“in“the“additional“axioms“w¬re“can“examine“these“indep˜enden¬rtly“from“theŽ¡‘ͼtranslated›ž¹form•¬rula.‘Ê;NonnengartŸû¥2¸11Ž‘žÁÖpresen“ts˜extremely˜go•SŽo“d˜simplications˜for˜v‘ÿXäariousŽ¡‘ͼmoSŽdal–ölogics.‘½ÉSo,›"	for“instance,˜the“whole“theory“for“the“moSŽdal“logic“KD45“(i.e.“theŽ¡‘ͼaccessibilitš¬ry–ÁÁrelation“is“serial,‘7‡transitiv˜e“and“euclidean)“can“bSŽe“simplied“to“theŽ¡‘ͼalmost–ˆ€trivial“unit“clause“×RJÖ(×Uò¬;‘
ÿþV‘œpÖ(×W‘
¡ÆÖ)).‘hF‘ÿVor“those“readers“familiar“with“KD45“thisŽ¡‘ͼmigh¬rt–ïnot“bšSŽe“to˜o“surprising“since“the“class“of“frames“whicš¬rh“are“c˜haracteristic“forŽ¡‘ͼKD45–¾Ñare“just“those“frames“whicš¬rh“consist“of“a“single“equiv‘ÿXäalence“class“or“a“w˜orldŽ¡‘ͼfollo•¬rw“ed›µb“y˜an˜equiv‘ÿXäalence˜class˜suc“h˜that˜this˜w“orld˜has˜access˜to˜all˜the˜elemen“tsŽ¡‘ͼin–”Rthis“class.‘Other“examples“for“suitable“simplications“are“e.g.“the“logic“KDB‘”<(i.e.Ž¡‘ͼthe–{¦accessibilit¬ry“relation“is“serial“and“symmetric).‘ëÛThe“set“of“theory“clauses“to“bSŽeŽ¡‘ͼadded–U¡to“the“translation“of“givš¬ren“form˜ula“consists“just“of“the“t˜w˜o“simple“unit“clausesŽ¡‘ͼ×RšJÖ(×Uò¬;‘
ÿþX‘�ñƒÖ(×U‘
@äÖ))–ê¨and“×R˜Ö(×X‘�ñƒÖ(×U–
@äÖ)×;‘
ÿþU“Ö)–ê¨and“nothing“else“is“necessary‘ÿV.Ž¡‘m°In–Zthe“folloš¬rwing“theorem“w˜e“suppSŽose“that“w˜e“ha˜v˜e“some“simplication“×S‘�²×im“Öwhic˜hŽ¡‘ͼcan–'óbšSŽe“applied“to“a“set“ØR“Öof“form¬rulae“expressing“the“prop˜erties“of“the“accessibilit¬ryŽ¡‘ͼrelation–ê¨suc¬rh“thatŽŸÆc‘_‡ØR–ª¨[“fÖSimŽ‘•HŸ
Ì̸2Ž›ULØg–URj‘þ�Ö=“[›þK…[““]˜]Ÿû™¹?ŽŸëڍŽŽŽ‘$ÌHÖiŽ‘2Õ"×S‘�²×imÖ(ØRÖ)–ª¨Ø[“fÖSimŽ‘•HŸ
Ì̸2Ž˜Øg–URj‘þ�Ö=“[›þK…[““]˜]Ÿû™¹?ŽŸëڍŽŽŽŽ¦‘ͼÛTheorem‘€�1ŽŽŽ¡‘ͼÙL›ÿffet– äÖ“Ùb˜e“a“Mo˜d-ØALCŽ‘TÙsentenc˜e“and“×T‘BªÙa“set“of“Mo˜d-ØALCŽ‘TÙsentenc˜es.‘5¤L˜et“ØR“Ùb˜e“a“set“ofŽ¡‘ͼformulae–35which“expr›ÿffess“the“pr˜op˜erties“of“the“underlying“ac˜c˜essibility“r˜elation.‘fiThenŽ¤Æc’�Î×T‘÷Øj‘þ�Ö=Ÿ
Ì̺RŽ‘¡×Ž¡‘ͼÙiŽ¤
Æc’�€ð®ŸõÿüëC[ŽŽŸ"%‘}Jȸ	º2¹TŽŽ’�‘³Ö[›þK…[–UR	“]˜]Ÿû™¹?ŽŸëڍŽŽŽ’�²‘Ø[–ª¨×S‘�²×imÖ(ØRÖ)“Ø[“fÖSimŽ‘•HŸ
Ì̸2Ž‘ULØg–URj‘þ�Ö=“[›þK…[““]˜]Ÿû™¹?ŽŸëڍŽŽŽŽŸxÁ‘ͼÙiŽŸã0Ÿùr$‘"2‡Ö[›þK…[–UR“]˜]Ÿû¥2¹?ŽŸRAŽŽŽ‘C¢,Ùis–ãWpr›ÿffovable“fr˜om“Ÿ÷ÿüëCSŽ‘8®Ÿ€¸	º2¹TŽ‘! ëÖ[›þK…[–UR	“]˜]Ÿû¥2¹?ŽŸRAŽŽŽ‘AMƒØ[–
ù.×S‘�²×imÖ(ØRÖ)“Ø[“fÖSimŽ‘•HŸ
Ì̸2Ž‘ULØg–ãWÙusing“some“the˜or˜emŽ¡‘"2‡pr›ÿffover–35which“is“c˜orr˜e˜ct“and“c˜omplete“for“rst-or˜der“lo˜gic“with“e˜quality.ŽŽŽŽŽŒ‹�����������������������������������������lÌ ´î; ýW
 Šõ덠ýš
‘ͼç5Ž‘*œŠAn‘Ÿ¼ExampleŽŸ¨†‘ͼÖSuppSŽose–¸Bob“is“a“car“seller“and“Tim“is“a“customer.‘ üTim“tells“Bob“that“he“w•¬ran“tsŽ¤
Æc‘ͼto–.buy“a“nice“car“and“for“some“reason“he“bSŽelievš¬res“that“red“cars“are“v˜ery“nice.‘3BobŽ¡‘ͼhas–Üýtold“Tim“that“he“can“oer“a“magen¬rta“colored“audi.‘ÞOf“course,‘’it“is“commonŽ¡‘ͼbSŽeliev•¬re,‘mOthat›S.magen“ta˜is˜a˜red˜color˜and˜that˜the˜audi˜is˜a˜car.‘rqThis˜situation˜canŽ¡‘ͼbSŽe–ê¨represenš¬rted“b˜y“the“follo˜wing“kno˜wledge“base.Ž¤4¹
Ÿä4€‘5S˜Þ2Ÿ
Ý߸(¹belKievI{e;bob¸)Ž‘.E?Þ2Ÿ
Ý߸(¹belKievI{e;tim¸)ŽŽ’�¯æø×audi‘URcolCorSŽedŽ‘+õmagn9entaŽŽ¤
Æb‘5S˜Þ2Ÿ
Ý߸(¹bel•KievI{e;al“l“¸)ŽŽ’�¯æø×magn9enta–URØ2“×rSŽedŽŽ¡‘5S˜Þ2Ÿ
Ý߸(¹bel•KievI{e;al“l“¸)ŽŽ’�¯æø×audi–URØ2“×carŽŽ¡‘5S˜Þ2Ÿ
Ý߸(¹belKievI{e;bob¸)Ž‘.E?Þ2Ÿ
Ý߸(¹belKievI{e;tim¸)ŽŽ’�µD·×car‘þ6Øu‘ª¨9‘
ÿþ×colCor•SŽed:r“edŽŽ’
׃ØvŽ’
3,Ú×nice‘�´x‰��ff�†fŽ‘:ÞcarŽŽ¡‘5S˜Þ2Ÿ
Ý߸(¹belKievI{e;bob¸)ŽŽ’�¯æøÞ2Ÿ
Ý߸(¹belKievI{e;tim¸)Ž‘2_-×nice‘�´x‰��ff�†fŽ‘:ÞcarŽŽ’
׃ØvŽ’
3,ÚÞ2Ÿ
Ý߸(¹w7ant;tim¸)Ž‘,Ø×buy‘
"±‰��ff�†fŽ‘©carŽŽŽŽŽ¡‘ͼÖF‘ÿVrom–}ºthis“knoš¬rwledge“base“it“follo˜ws“that“Bob“bSŽeliev˜es“that“Tim“w˜an˜ts“to“buy“theŽ¤
Æc‘ͼaudi,‘ê¨i.e.Ž¡’�>´Þ2Ÿ
Ý߸(¹belKievI{e;bob¸)Ž‘.E?Ö(×audi–URØ2“Þ2Ÿ
Ý߸(¹w7ant;tim¸)Ž‘,Ø×buy‘
"±‰��ff�†fŽ‘©carŽ‘_:îÖ)ŽŸA ‘ͼshould–ê¨bSŽe“pro¬rv‘ÿXäable.Ž¡‘m°The–ê¨translation“of“the“knoš¬rwledge“base“results“in“the“follo˜wing“clauses:Ž©º‘@?×colCorSŽedÖ(×V‘�§;–
ÿþaudi;“magn9entaÖ)ŽŽ’�ÏxØ(ŽŽ’�åz<Ÿû™¹bobŽŸëڍbelKievI{eŽŽ›êÛÖ(×;‘
ÿþU‘
@äÖ)–ª¨Ø^“<Ÿû™¹timŽŸëڍbelKievI{eŽŽ˜Ö(×Uò¬;‘
ÿþV‘œpÖ)ŽŽ’
¨”Î(1)ŽŽŽ¤Æc‘p,×rSŽedÖ(×Uò¬;‘
ÿþmagn9entaÖ)ŽŽ’�ÏxØ(ŽŽ’�åz<Ÿû™¹alKlŽŸëڍbelKievI{eŽŽ‘êÛÖ(×;‘
ÿþU‘
@äÖ)ŽŽ’
¨”Î(2)ŽŽŽ¡’�†ç×carSŽÖ(×Uò¬;‘
ÿþaudiÖ)ŽŽ’�ÏxØ(ŽŽ’�åz<Ÿû™¹alKlŽŸëڍbelKievI{eŽŽ‘êÛÖ(×;‘
ÿþU‘
@äÖ)ŽŽ’
¨”Î(3)ŽŽŽ¡‘yØá×nice‘�´x‰��ff�†fŽ‘:ÞcarSŽÖ(×V‘�§;‘
ÿþX‘�ñƒÖ)ŽŽ’�ÏxØ(ŽŽ’�åz<Ÿû™¹bobŽŸëڍbelKievI{eŽŽ›êÛÖ(×;‘
ÿþU‘
@äÖ)–ª¨Ø^“<Ÿû™¹timŽŸëڍbelKievI{eŽŽ˜Ö(×Uò¬;‘
ÿþV‘œpÖ)“Ø^ŽŽŽ¡’�åz×colCoršSŽedÖ(×V‘�§;–
ÿþXJg;“Y‘œpÖ)–ª¨Ø^“×r˜edÖ(×V‘�§;‘
ÿþY‘œpÖ)“Ø^ŽŽŽ¡’�åz×carSŽÖ(×V‘�§;‘
ÿþX‘�ñƒÖ)ŽŽ’
¨”Î(4)ŽŽŽ¡‘}‡{×buy‘
"±‰��ff�†fŽ‘©carSŽÖ(×V‘�§;‘
ÿþX‘�ñƒÖ)ŽŽ’�ÏxØ(ŽŽ’�åz<Ÿû™¹bobŽŸëڍbelKievI{eŽŽ‘êÛÖ(×;›
ÿþU‘
@äÖ)–ª¨Ø^“<Ÿû™¹timŽŸëڍw7antŽŽ‘Ž†Ö(×Uò¬;˜V‘œpÖ)“Ø^ŽŽŽ¡’�åz×nice‘�´x‰��ff�†fŽ‘:ÞcarSŽÖ(×fŸû™‘
Gÿ¹timŽŸëڍbelKievI{eŽŽ‘êÛÖ(×U‘
@äÖ)×;‘
ÿþX‘�ñƒÖ)ŽŽ’
¨”Î(5)ŽŽŽ¦‘ͼW‘ÿVe–©øassume“bšSŽoth“consistency“and“full“in¬rtrosp˜ection“for“the“agen¬rts'“b˜eliefs.‘vÏIn“thisŽ©
Æc‘ͼcase–ê¨wš¬re“are“allo˜w˜ed“to“simplify“the“theory“clauses“for“the“mošSŽdal“op˜erator“toŸû¥2¸11Ž‘	�Ö:Ž¤Æc’�œ Ø<Ÿû™¹XŽŸëڍbelKievI{eŽŽ–êÛÖ(×Uò¬;‘
ÿþYŸû™‘œp¹XŽŸëڍbelKievI{eŽŽ“Ö(×V‘œpÖ))ŽŽ’
RìØ(ŽŽ’
¨”ÎÖ(6)ŽŽŽ¡‘ͼwhere–4×X‘·Öranges“o•¬rv“er–4the“set“of“agenš¬rts“(i.e.“Bob“and“Tim).‘µƒThe“spSŽecial“agen˜t“Ùal‘�™™l‘RÇÖisŽ¦‘ͼtherefore–ê¨a“KD45-opSŽerator“as“wš¬rell,“whic˜h“ranges“o˜v˜er“all“agen˜ts,“th˜us:Ž¡’�œ Ø<Ÿû™¹alKlŽŸëڍbelKievI{eŽŽ–êÛÖ(×Uò¬;‘
ÿþYŸû™‘œp¹XŽŸëڍbelKievI{eŽŽ“Ö(×V‘œpÖ))ŽŽ’
RìØ(ŽŽ’
¨”ÎÖ(7)ŽŽŽ¡‘ͼF‘ÿVor–¬«the“ÙwantÖ-opSŽerator,›Ý,ho•¬rw“ev“er,˜w“e–¬«do“not“assume“an¬rything“in“particular,˜merelyŽ¦‘ͼconsistency–ê¨of“what“is“w•¬ran“ted:Ž¡’�¢Œ“Ø<Ÿû™¹XŽŸëڍw7antŽŽ–Ž†Ö(×Uò¬;‘
ÿþYŸû™‘œp¹XŽŸëڍw7antŽŽ“Ö(×U‘
@äÖ))ŽŽ’
ÙyØ(ŽŽ’
¨”ÎÖ(8)ŽŽŽ¡‘ͼFinally‘ÿV,–ê¨w¬re“get“as“the“negated“theorem:Ž¡’�ñªØ(‘UR×buy‘
"±‰��ff�†fŽ‘©carSŽÖ(×hŸû™¹timŽŸëڍw7antŽŽ‘Ž†Ö(×gŸû™n9¹bobŽŸëڍbelKievI{eŽŽ‘êÛÖ(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
¨”Í(9)ŽŽŽ¡‘ͼBecause–í all“axioms“are“Horn“clauses,‘í¾wš¬re“can“ev˜en“use“PR˜OLOG‘íto“pro˜v˜e“our“theo-Ž¦‘ͼrem.‘8àThe–ê¨linear“deriv‘ÿXäation“of“the“goal“is:ŽŽŽŒ‹���	��������������������������������������z, ´î; ýW
 Šõ덠ýùä
‘ ퟔŒz‰��ff
„23Ÿ	鍍ÌÍŸ!í„�
ô��ffŸûލ‘ÌÍØ(‘UR×buy‘
"±‰��ff�†fŽ‘©carSŽÖ(×hŸû¥2¹timŽŸRAw7antŽŽ‘Ž†Ö(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ‘êÛÖ(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¤
ôÌÍŸ!í„�
ô��ffŸûލ‘ÌÍØ(‘UR<Ÿû¥2¹bobŽŸRAbelKievI{eŽŽ‘êÛÖ(×;›
ÿþU‘
@äÖ)–ª¨Ø^“<Ÿû¥2¹timŽŸRAw7antŽŽ–Ž†Ö(×Uò¬;˜hŸû¥2¹timŽŸRAw7antŽŽ“Ö(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ›êÛÖ(×Ö)))–ª¨Ø^“×nice‘�´x‰��ff�†fŽ‘:ÞcarSŽÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ˜Ö(×U‘
@äÖ)×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ©
ÆbÌÍŸ!í„�
Æb��ffŸûލ‘,÷]using–ê¨axiom“5ŽŽ’
ƒ˜š„�
Æb��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘ÌÍØ(‘UR×nice‘�´x‰��ff�†fŽ‘:ÞcarSŽÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¦ÌÍŸ!í„�
Æb��ffŸûލ‘,÷]using–ê¨axioms“6“and“8ŽŽ’
ƒ˜š„�
Æb��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘ÌÍØ(‘UR<Ÿû¥2¹bobŽŸRAbelKievI{eŽŽ›êÛÖ(×;‘
ÿþU‘
@äÖ)–ª¨Ø^“<Ÿû¥2¹timŽŸRAbelKievI{eŽŽ˜Ö(×Uò¬;‘
ÿþfŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ˜Ö(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ˜Ö(×Ö)))‘URØ^ŽŽ’
ƒ˜š„�
ô��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘"!×colCoršSŽedÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;–
ÿþaudi;“Y‘œpÖ)–ª¨Ø^“×r˜edÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþY‘œpÖ)‘URØ^ŽŽ’
ƒ˜š„�
ô��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘"!×carSŽÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¦ÌÍŸ!í„�
Æb��ffŸûލ‘,÷]using–ê¨axiom“4ŽŽ’
ƒ˜š„�
Æb��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘ÌÍØ(‘UR×colCoršSŽedÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;–
ÿþaudi;“Y‘œpÖ)–ª¨Ø^“×r˜edÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþY‘œpÖ)‘URØ^ŽŽ’
ƒ˜š„�
ô��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘"!×carSŽÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¦ÌÍŸ!í„�
Æb��ffŸûލ‘,÷]using–ê¨axioms“6“t¬rwiceŽŽ’
ƒ˜š„�
Æb��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘ÌÍØ(‘UR<Ÿû¥2¹bobŽŸRAbelKievI{eŽŽ›êÛÖ(×;‘
ÿþU‘
@äÖ)–ª¨Ø^“<Ÿû¥2¹timŽŸRAbelKievI{eŽŽ˜Ö(×Uò¬;‘
ÿþfŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ˜Ö(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ˜Ö(×Ö)))Ø^ŽŽ’
ƒ˜š„�
ô��ffŽŽ¡ÌÍŸ!í„�
ô��ffŸûލ‘"!×ršSŽedÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþmagn9entaÖ)–ª¨Ø^“×car˜Ö(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¦ÌÍŸ!í„�
Æb��ffŸûލ‘,÷]using–ê¨axiom“1ŽŽ’
ƒ˜š„�
Æb��ffŽŽŽŽŽ �¼v-ŸÁLƍ‘溟!í„�
ô��ffŸûލ‘ÌÍØ(‘UR×ršSŽedÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþmagn9entaÖ)–ª¨Ø^“×car˜Ö(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¤
Æb‘溟!í„�
Æb��ffŸûލ‘,÷]using–ê¨axioms“6“t¬rwiceŽŽ’
ƒ˜š„�
Æb��ffŽŽ©
􍍑溟!�
ô��ffŸûލ‘ÌÍØ(‘UR<Ÿû¥2¹alKlŽŸRAbelKievI{eŽŽ–êÛÖ(×;›
ÿþfŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ“Ö(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö)))–ª¨Ø^“×carSŽÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;˜audiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¡‘溟!í„�
Æb��ffŸûލ‘,÷]using–ê¨axiom“2ŽŽ’
ƒ˜š„�
Æb��ffŽŽ¦‘溟!í„�
ô��ffŸûލ‘ÌÍØ(‘UR×carSŽÖ(×fŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ–êÛÖ(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö))×;‘
ÿþaudiÖ)ŽŽ’
ƒ˜š„�
ô��ffŽŽ¡‘溟!í„�
Æb��ffŸûލ‘,÷]using–ê¨axiom“7ŽŽ’
ƒ˜š„�
Æb��ffŽŽ¦‘溟!í„�
ô��ffŸûލ‘ÌÍØ(‘UR<Ÿû¥2¹alKlŽŸRAbelKievI{eŽŽ–êÛÖ(×;‘
ÿþfŸû¥2‘
Gÿ¹timŽŸRAbelKievI{eŽŽ“Ö(×gŸû¥2n9¹bobŽŸRAbelKievI{eŽŽ“Ö(×Ö)))ŽŽ’
ƒ˜š„�
ô��ffŽŽ¡‘溟!í„�
Æb��ffŸûލ‘,÷]using–ê¨axiom“3ŽŽ’
ƒ˜š„�
Æb��ffŽŽ¡‘溟!í„�
Æb��ffŸûލ‘ÌÍsuccessŽŽŽ’
ƒ˜š„�
Æb��ffŽŽ¡‘溟!í„�
Æb��ffŸûލ‘,÷]using–ê¨axiom“7ŽŽ’
ƒ˜š„�
Æb��ffŽŽ‘ ퟈S‰��ff
„23ŽŽŽŸa±—‘ͼç6Ž‘*œŠConclusion–Ÿ¼and“F›þXurther“W˜orkŽŸ¨†‘ͼÖW‘ÿVe–Æpresenš¬rted“an“approac˜h“whic˜h“allo˜ws“to“reason“within“moSŽdal“terminological“logicsŽ¤
Æc‘ͼbš¬ry–òutilizing“an“appropriate“translation“tec˜hnique“in˜to“rst-order“predicate“logic.‘æ
TheŽ¡‘ͼmain–idea“bšSŽehind“this“metho˜d“is“the“Ùfunctional‘Uœsimulation“Öof“accessibilit¬ry“relationsŽ¡‘ͼand–sÇroles“bš¬ry“suitable“sets“of“functions.‘@This“turns“out“to“ha˜v˜e“t˜w˜o“main“adv‘ÿXäan˜tages:Ž¡‘ͼit–µ
decreases“the“size“and“the“n•¬rum“bSŽer–µ
of“clauses“and“it“alloš¬rws“signican˜t“simplicationsŽ¡‘ͼon–ê¨the“set“of“theory“clauses.Ž¡‘m°A‘[ònecessary–\condition“for“the“methošSŽd“prop˜osed“here“to“w¬rork“is“that“the“acces-Ž¡‘ͼsibilitš¬ry–øárelation“propSŽerties“ha˜v˜e“to“bSŽe“rst-order“predicate“logic“denable.‘cŠUnfortu-Ž¡‘ͼnately‘ÿV,–ê¨not“all“mošSŽdal“logics“ha•¬rv“e–ê¨a“rst-order“describable“frame“prop˜ert¬ry‘ÿV.Ž¡‘m°Un•¬rtil›ž{no“w,‘­¸w“e˜ha“v“e˜only˜w“ork“ed˜out˜the˜optimization˜for˜those˜moSŽdalities˜whic“hŽ¡‘ͼha•¬rv“e–Á¯a“simple“pSŽossible“wš¬rorld“seman˜tics.‘+8If“the“in˜teraction“of“m˜ultiple“moSŽdalities“re-Ž¡‘ͼquires–¾÷the“more“complex“neighš¬rb•SŽourho“o“d–¾÷seman˜tics,‘Ç´w˜e“ha˜v˜e“to“rely“on“the“straigh˜t-Ž¡‘ͼforwš¬rard–iþtranslation“whic˜h“will“result“in“a“rather“large“n˜um˜bšSŽer“of“clauses.‘¶ãLo˜okingŽ¡‘ͼfor–,$optimizations“for“this“case“is“part“of“future“w¬rork.‘ýUBesides,‘<„the“extension“of“theŽ¡‘ͼsystem–ê¨b¬ry“Ùnumb–ÿffer‘35r“estrictions‘è…Öis–ê¨one“of“the“ma‘�§jor“future“goals.ŽŽŽŒ‹���
��������������������������������������‰Î ´î; ýW
 Šõ덠ýš
‘ͼçReferencesŽŸ¨†‘ͼÖ1.ŽŽ‘ÛìF.–’ŽBaader“and“B.“Hollunder.‘)ßØK,`RI‘�âÈS‘�æbÖ:‘ˆ¬Knoš¬rwledge“Represen˜tation“and“InferenceŽ¤
Æc‘ͼSystem–xÌ|“System“Description“|.‘	×ýT‘ÿVecš¬rhnical“Memo“DFKI-TM-90-03,‘ÜTDeutsc˜hesŽ¡‘ͼF‘ÿVorsc•¬rh“ungszen“trum–ê¨fšSŽ‘ùÌvur“K˜‘ùÌvunstlicš¬rhe“In˜telligenz,“1990.Ž©Æc‘ͼ2.ŽŽ‘ÛìR.– ƒJ.“Brac¬rhman,›âŠV.“P‘ÿV.“GilbSŽert,˜and“H.“J.“Levš¬resque.‘`An“Essen˜tial“Hybrid“ReasoningŽ¡‘ͼSystem:‘Knoš¬rwledge–”öand“Sym˜bSŽol“Lev˜el“Accoun˜ts“of“ëHkr‘ÿ32yptonÖ.‘©ØIn“ÙPr–ÿffo“c“e“e“dings–äqof“theŽ¡‘ͼNinth–RŠInternational“Joint“Confer–ÿffenc“e–RŠon“A³2rticial“Intel‘�™™ligenc‘ÿffeÖ,–Dpages‘¿532{539,“LosŽ¡‘ͼAngeles,–ê¨California,“1985.Ž¦‘ͼ3.ŽŽ‘ÛìR.–\J.“Bracš¬rhman“and“J.“G.“Sc˜hmolze.‘	‚fAn“Ov˜erview“of“the“ëHklone“ÖKno˜wledgeŽ¡‘ͼRepresen¬rtation›ê¨System.‘5ˆÙCo–ÿffgnitive‘35Scienc“eÖ,˜9(2):171{216,˜1985.Ž¦‘ͼ4.ŽŽ‘ÛìF.–¢#M.“Donini,›Ð
M.“Lenzerini,˜D.“Nardi,˜A.“Sc¬rhaerf,˜and“W.“Nutt.‘XMAdding“Epis-Ž¡‘ͼtemic–¹dOpšSŽerators“to“Concept“Languages.‘šIn“B.“Neb˜el,›íC.“Ric¬rh,˜and“W.“Sw¬rartout,Ž¡‘ͼeditors,‘
7ÙPr–ÿffo“c“e“e“dings–LŸof“the“Thir›ÿffd“International“Confer˜enc˜e“on“Principles“of“Know‘�™™l-Ž¡‘ͼe–ÿffdge›[R“epr“esentation˜and˜R“e“asoningÖ,–!ˆpages›342{353,“San˜Mateo,“CA,˜1992.˜MorganŽ¡‘ͼKaufmann.Ž¦‘ͼ5.ŽŽ‘ÛìB.–I¸Hollunder“and“W.“Nutt.‘	K³Subsumption“Algorithms“for“Concept“Languages.Ž¡‘ͼResearcš¬rh–³ÀRepSŽort“DFKI-RR-90-04,‘¾»Deutsc˜hes“F‘ÿVorsc˜h˜ungszen˜trum“fšSŽ‘ùÌvur“K˜‘ùÌvunstlic¬rhe“In-Ž¡‘ͼtelligenz,‘ê¨1990.Ž¦‘ͼ6.ŽŽ‘ÛìU.–ù^Hustadt,›) A.“Nonnengart,˜R.“Sc¬rhmidt,˜and“J.“Timm.›¬7MOTEL‘ù User“Man¬rual.˜In-Ž¡‘ͼternal–PàrepSŽort“MPI-I-92-236,›o¢Max-Planc¬rk-Institute“for“Computer“Science,˜June“1992.Ž¦‘ͼ7.ŽŽ‘ÛìA.›öLKobsa.‘§6To•¬rw“ards˜Inferences˜in˜BGP-MS:˜Com“bining˜MoSŽdal˜Logic˜and˜PartitionŽ¡‘ͼHierarc¬rhies–ÈRfor“User“MošSŽdeling“(Preliminary“Rep˜ort).‘ýBeric•¬rh“t–ÈRWIS-2,‘Ï0Pro‘�§jekt“BGP-Ž¡‘ͼMS,–ZUUnivš¬rersit‘ú at“Konstanz“Informationswissensc˜haft,‘w2P˜ostfac˜h“5560,‘w27750“Konstanz,Ž¡‘ͼJuni–HP1992.‘	G‚ProšSŽceedings“of“the“Third“In¬rternational“W‘ÿVorkshop“on“User“Mo˜deling,Ž¡‘ͼScš¬rhloss–ê¨Dagstuhl,“German˜y‘ÿV,“Aug.“10{13,“1992.Ž¦‘ͼ8.ŽŽ‘ÛìR.–™‡M.“MacGregor.›>¦Inside“the“LOOM‘™ZDescription“Classier.˜ÙSIGAR‘ÿ™T‘ÓÈBul‘�™™letinÖ,Ž¡‘ͼ2(3):88{92,‘,©1991.‘
—SpSŽecial–¹Issue“on“Implemenš¬rted“Kno˜wledge“Represen˜tation“andŽ¡‘ͼReasoning‘ê¨Systems.Ž¦‘ͼ9.ŽŽ‘ÛìR.–Ž+C.“Mo•SŽore.›ÍAuto“epistemic–Ž+Logic.˜In“Ph.“Smets,›·E.“H.“Mamdani,˜D.“DubSŽois,Ž¡‘ͼand–$ÓH.“Prade,–s^editors,“ÙNon-Standar–ÿffd›SûL“o“gics˜for˜A³2utomate“d˜R“e“asoningÖ.‘$ÓAcademicŽ¡‘ͼPress,–ê¨London,“1988.Ž¦‘ͼ10.ŽŽ‘»èJ.–êêMylopšSŽoulos“and“M.“Bro˜die,‘*ûeditors.‘1/ÙR–ÿffe“adings–Àin“A³2rticial“Intel‘�™™ligenc‘ÿffe“andŽ¡‘ͼDatab‘ÿffasesÖ.‘5ˆMorgan–ê¨Kaufmann,“San“Mateo,“CA,“1989.Ž¦‘ͼ11.ŽŽ‘»èA.–z5Nonnengart.‘~;First-Order“MoSŽdal“Logic“Theorem“Proš¬rving“and“Standard“PR˜O-Ž¡‘ͼLOG.‘YíInš¬rternal–ø–repSŽort“MPI-I-92-228,‘<Max-Planc˜k-Institute“for“Computer“Science,Ž¡‘ͼJuly‘ê¨1992.ŽŽŽŒ‹�����������������������������������������  ´î; ýW
 Šõ덠ýš
‘ͼÖ12.ŽŽ‘»èH.–}J.“Ohlbac¬rh.‘‚òÙA‘ÎhR›ÿffesolution–΁Calculus“for“Mo˜dal“L˜o˜gicsÖ.‘‚òPhD‘|ýthesis,‘“Univ¬rersit‘ú atŽ©
Æc‘ͼKaiserslautern,–ê¨OctobSŽer“1988.Ž¤Æc‘ͼ13.ŽŽ‘»èN.–ê¨Resc¬rher“and“A.“Urquhart.›5ˆÙT‘ÿ™emp–ÿffor“al‘35L“o“gicÖ.˜Springer,–ê¨Berlin,“1971.Ž¡‘ͼ14.ŽŽ‘»èJ.–G.“Scš¬rhmolze.‘—fThe“Language“and“Seman˜tics“of“ëHniklÖ.‘—fT‘ÿVec˜hnical“RepSŽort“89{4,Ž¦‘ͼDepartmenš¬rt–ê¨of“Computer“Science,“T‘ÿVufts“Univ˜ersit˜y‘ÿV,“Medford,“MA,“1989.ŽŽŽŒø��¬Ò
ƒ’À;����è´î;
·˜Q��óHŒ-ø����
���cmcsc10óCú±u�
���
���cmex10ó<ò"V�G®�
���cmbx10ó;!",š�G®�
���cmsy10ó7ò"V�ff�
���cmbx10ó4Kñ`y�ff�
���cmr10ó3TqÔ����
���lasy10ó1߆µT�������cmtt12ó0ÂÖN �������cmbx12ó.›»ˆ@�������cmti12ó-!",š����
���cmsy10ó,·ág£�������cmmi12ó+X«Q�������cmr12ó"Kñ`y�
ó3�
���cmr10óKñ`y�
���
���cmr10ó¾KÈ�������cmsy8ó×
2�������cmmi8ó
|{Y�������cmr8óÙ“ R�������cmr7ó;Î�������cmmi6ù��¯ßßßßßß