2008.5 international conference

FederatedALCI:PreliminaryReport

GeorgeVoutsadakis,GioraSlutzki,VasantHonavar

DepartmentofComputerScience

IowaStateUniversityAmes,IA50011

JieBao

DepartmentofComputerScienceRensselaerPolytechnicInstitute

Troy,NY12180

Abstract—WeintroduceF-ALCI,afederatedversionofthedescriptionlogicALCI.AnF-ALCIontology,likeitspackage-basedcounterpartALCIP−,consistsofmultipleALCIontolo-giesthatcanimportconceptsorrolesdefinedinothermodules.UnlikeALCIP−,whichsupportsonlycontextualizednegation,F-ALCI,supportscontextualizationofeachofthelogicalconnec-tives,afeaturethatallowsmoreflexiblereuseofknowledgefromindependentlydevelopedontologies.WeprovideanewsemanticsforF-ALCIbasedonimagedomainrelationsandestablishtheconditionsthatneedtobeimposedondomainrelationstoensureproperties,suchaspreservationofunsatisfiabilityandmonotonicityofinference,thataredesirableindistributedwebapplications.WealsoestablishthedecidabilityofF-ALCI.

I.INTRODUCTION

Thesemanticweb,muchliketheworld-wideweb,reliesonthenetworkeffect,thatisonleveragingtheworkofindepen-dentactorswhocontributeresources,includingontologies,thatareinterlinkedtoformawebofresources.Inshort,ontologies:semanticweb::webpages:web.Inevitably,theaxiomsthatmakeupsuchontologiesareapplicablewithinthespecificcontextsthatareimplicitlyassumedbytheirauthors.Hence,semanticwebapplicationsthathavetorelyonknowledgefromanetworkofinterlinkedontologiesneedtocarefullyreconcilethedisparatecontextsassumedbydifferentontologies[4],[3].Modularontologyformalisms,suchasdistributeddescrip-tionlogics(DDL)E-Connections,semanticimporting,se-manticbindingandpackage-baseddescriptionlogics(P-DL)(see[2]andthereferencescitedtherein),providesupport,tovaryingdegrees,forexploitinganetworkofinterlinkedontologies.WiththeexceptionofP-DL[1],[2]whichprovideslimitedsupportforexplicittreatmentofcontextthroughcon-textualizednegation,noneoftheformalismsprovidessupportforexplicitreferencetocontext.

Againstthisbackground,thispaperexploresafamilyofcontextualizedfederateddescriptionlogics(CFDLs)toexploretheincorporationofcontextinasimplified,yetpracticallyusefulsetting.

•IntroductionofCFDLF-ALCI,inwhicheachofthein-dividualontologymodulesisexpressedintheDLALCI(themostfundamentaldescriptionlogicALCaugmentedwithinverseroles),which,tothebestofourknowledge,representsthefirstmodularontologylanguagetosupportcontextualizedinterpretationofalllogicalconnectivesusedwithintheDLmodules.IntheCFDLF-ALCI,inferencesarealwaysdrawnfromthepointofviewofawitnessmodule.Theresultsofinferenceareguranteed

978-0-7695-3496-1/08 $25.00 © 2008 IEEEDOI 10.1109/WIIAT.2008.296

tobethesameasthoseobtainedbyastandardreasoneroveranontologythatintegrates(fromthepointofviewofthewitnessmodule)theknowledgethatit(selectively)importsfromtheothermodules.Differentmodulesmightinferdifferentconsequences,basedontheknowledgethattheyimportfromtheothermodules.

•Characterizationofthetradeoffsbetweentherestrictionsondomainrelations(andhencethesemanticsoftheCFDLF-ALCI)andthedesirablefeaturesofthere-sultingmodularontologies(e.g.,monotonicityofinfer-enceandtransitivepropagationofconceptsubsumptionsacrossmoduleslinkedbyimportingrelations).Specifi-cally,weshowthat,inthegeneralcase,wheninterpreta-tionswitharbitrarydomainrelationsareallowedinthesemanticsofF-ALCI,severalofthedesirableproperties,e.g.,monotonicityofinferenceandpreservationofun-satisfiability,arelost;andthatregainingthesepropertiesrequiresstrengtheningtheconditionsonthesemanticsofF-ALCI.Furthermore,weshowthatitispossibletopreservemanyofthedesirablepropertiesofP-DLs,whileatthesametimeimposingmilderrestrictionsthanthoseusedinP-DLs.

Forthesakeofsimplicity,wehavenotconsideredcyclicimportingormoreexpressivelanguagesthanALCI(e.g.,SHOIQ).NorhavewedealtwithA-BoxesorR-Boxes.OurexperiencewithP-DLssuggeststhatincorporationofA-BoxesandR-Boxesareunlikelytopresentmajorchallenges.How-ever,theinterplaybetweenincreasedexpressivityoflanguageusedbyindividualontologymodules,unrestrictedimportingrelations(e.g.,cyclicimporting)andthesemanticsbasedonimagedomainrelationsrequiresfurtherstudy.

II.THEFEDERATEDDESCRIPTIONLOGICF-ALCIIn[2],givenanordinarydescriptionlogicL,thenotationLPisintroducedtodenoteitspackage-basedcounterpart,i.e.,thepackage-baseddescriptionlogicwhichusesLasthelogicallanguageineachofitspackages.Furthermore,thenotationLP−signifiesthattheimportingofconceptnamesandrolenamesacrosspackagesisacyclic.Inthepresentwork,weusetheprefix“F-”,standingforFederated,todenoteacontextualizedfederatedlanguageand,sinceourdiscussionislimitedtoacyclicimporting,omittheuseofasuperscript“−”fromthenotation.

Inthissection,thesyntaxandthesemanticsofthelanguageF-ALCIwillbedescribedinsomedetail.

571575

Authorized licensed use limited to: Iowa State University. Downloaded on June 21, 2009 at 23:08 from IEEE Xplore. Restrictions apply.

A.TheSyntax

SupposeadirectedacyclicgraphG=󰀘V,E󰀙,withV={1,2,...,n},isgiven.Theintuitionisthatitsnnodescorrespondtolocalmodulesofamodularontologyanditsedgescorrespondtotheimportingrelationsbetweenthesemodules.Fortechnicalreasons,weaddalooponeachvertexofG.

Foreverynodei∈V,thesignatureofthei-languagealwaysincludesasetCiofi-conceptnamesandasetRiofi-rolenames.Weassumethatallsetsofnamesarepairwisedisjoint.

󰀁iandasetofOutofthese,asetofi-conceptexpressionsC

󰀁iarebuilt.i-roleexpressionsR

RecallthatthedescriptionlogicALCIallowsconceptexpressionsthatareconstructedrecursivelyfromitssignaturesymbols,i.e.,itsroleandconceptnames,usingnegation,conjunction,disjunction,valueandexistentialrestrictionandinversesofrolenames.Itsformulasaresubsumptionsbetweenconceptexpressions.

ThesyntaxofthedescriptionlogicF-ALCIisdefinedasfollows:

Definition1(RolesandConcepts):Thesetofi-rolesor

󰀁iconsistsofexpressionsoftheformi-roleexpressionsR

R,R−,withR∈Rj,(j,i)∈E.

󰀁i,ontheThesetofi-conceptsori-conceptexpressionsC

otherhand,isdefinedrecursivelyasfollows:

A∈Cj,󰀇j,⊥j,¬jC,C󰀜jD,C󰀛jD,∃jR.C,∀jR.C,(1)󰀁i∩C󰀁jandR∈R󰀁i∩R󰀁j.where(j,i)∈E,C,D∈C

UsingtheconceptsandrolesofF-ALCI,wedefineitsformulas,asfollows:

Definition2(Formulas):Thei-formulasareexpressionsof

󰀁i,foralli∈V.theformC󰀝D,withC,D∈C

AnF-ALCI-TBoxorTBoxisacollectionT={Ti}i∈V,whereTiisafinitesetofi-formulas,calledthei-TBox.Since,inthispaper,wedonotconsiderRBoxesorABoxes,thetermsTBox,ontologyandknowledgebasewillbeusedinterchangeably.

Foralli∈V,RiandCidenotethesetofi-rolesandofi-concepts,respectively,thatoccurinTi.Ciisafinitesubset󰀁i.ArolenameinRj∩RioraconceptnameinCj∩CiisofC

saidtobeimportedfrommodulejtomodulei.Furthermore,

󰀁i,itisobviousthatamoduleiisallowedtousesinceCi⊆C

logicalconnectivessubscriptedbytheindexofamodulej,whenever(j,i)∈E.

B.TheSemantics

Inthissubsection,wepresentthesemanticsforthelanguageF-ALCI.

Definition3:AninterpretationI=󰀘{Ii}i∈V,

ii

{rij}(i,j)∈E󰀙consistsofafamilyIi=󰀘Δ,·󰀙,i∈V,oflocalinterpretations,togetherwithafamilyofimagedomainrelationsrij⊆Δi×Δj,(i,j)∈E,suchthatrii=idΔi,foralli∈V.

Notation:Forabinaryrelationr⊆Δi×Δj,X⊆ΔiandS⊆Δi×Δi,weset

r(X):={y∈Δj:(∃x∈X)((x,y)∈r)},

r(S):={(z,w)∈Δj×Δj:(∃(x,y)∈S)((x,z),(y,w)∈r)}.Alocalinterpretationfunction·iinterpretsi-rolenamesandi-conceptnames,aswellas⊥iand󰀇i,asfollows:

ii

•C⊆Δ,forallC∈Ci,

iii

•R⊆Δ×Δ,forallR∈Ri,

iii

•󰀇i=Δ,⊥i=∅.

Theinterpretationsofimportedrolenamesandimportedconceptnamesarecomputedbythefollowingrules:

ij󰀁i,•C=rji(C),forallC∈Cj∩Cij󰀁i,•R=rji(R),forallR∈Rj∩Riji

•󰀇j=rji(Δ),⊥j=∅.

Therecursivefeaturesofthelocalinterpretationfunction·iareasfollows:

−−i

•R=Ri,forallR∈Ri,

ijj

•(¬jC)=rji(Δ−C)

ijj

•(C󰀜jD)=rji(C∩D)

ijj

•(C󰀛jD)=rji(C∪D)

ijj

•(∃jR.C)=rji({x∈Δ:(∃y)((x,y)∈Randy∈Cj)})

ijj

•(∀jR.C)=rji({x∈Δ:(∀y)((x,y)∈Rimpliesy∈Cj)})

Foralli∈V,i-satisfiability,denotedby|=i,isdefinedbyI|=iC󰀝DiffCi⊆Di.GivenaTBoxT={Ti}i∈V,theinterpretationIisamodelofTi,writtenI|=iTi,iffI|=iτ,foreveryτ∈Ti.Moreover,IisamodelofT,writtenI|=T,iffI|=iTi,foreveryi∈V.

Letw∈V.DefineGw=󰀘Vw,Ew󰀙tobethesubgraphofGinducedbythoseverticesinGfromwhichwisreachable

∗

andTw:={Ti}i∈Vw.WesaythatanF-ALCI-ontologyT=

∗

{Ti}i∈VisconsistentaswitnessedbyamoduleTwifTwhas

w

amodelI=󰀘{Ii}i∈Vw,{rij}(i,j)∈Ew󰀙,suchthatΔ=∅.AconceptCissatisfiableaswitnessedbyTwifthereisa

∗

modelIofTw,suchthatCw=∅.AconceptsubsumptionC󰀝DisvalidaswitnessedbyTw,denotedbyC󰀝wD,if,

∗

foreverymodelIofTw,Cw⊆Dw.Analternativenotation

∗

forC󰀝wDisTw|=wC󰀝D.Example1.(SeeFigure1).Thisexampleillustratescontex-tualizedintersectionandcontextualizednegationinF-ALCI.ConsideramodulePi,containingconcepts“ComputerModel”and“PhoneModel”.ModulePj,ontheotherhand,hasaconcept“Brand”.SupposemodulePjimportsconcepts“Computermodel”and”PhoneModel”frommodulePi.AninterpretationoftheontologyisgiveninFigure1.Theimagedomainrelationrijmapsbothacomputermodel“MacBookAir”andaphonemodel“iPhone”tothebrand“Apple”,aninstanceoftheconcept“Brand”inPj.Onemayverifythat,whereas(ComputerModel󰀜iPhoneModel)j=∅,wehavethat(ComputerModel󰀜jPhoneModel)j=∅.Intu-itively,(ComputerModel󰀜jPhoneModel)jcontainsbrandsindomainΔjthatareassociatedwithbothindividualsof“ComputerModel”andindividualsof“PhoneModel”inmodulePi.Thebrand“Apple”fulfillsthisrequirement.Onemayalsoverifythat,inthiscase,

jj

(¬iComputerModel)=Brand(individualsindomain

576572

Authorized licensed use limited to: Iowa State University. Downloaded on June 21, 2009 at 23:08 from IEEE Xplore. Restrictions apply.

Fig.1.InterpretationofContextualizedNegation.

ΔjthatareassociatedwithindividualsthatarenotcomputermodelsindomainΔi),whereas(¬jComputerModel)j=∅(individualsindomainΔjthatarenotassociatedwithindividualsthatarecomputermodelsindomainΔi).ThisexampleshowsthatnegationinF-ALCIhascontextualizedmeaningindifferentmodules.

III.EXACTNESSOFF-ALCI

Exactnessisapropertyofsomeinterpretationsoffederateddescriptionlogics,whichensuresseamlesspropagationofknowledgeacrossimportingchains.Moreprecisely,ifacon-ceptCinmodulekisimportedbybothmoduleiandmodulej,andmodulejimportsmodulei,thenexactnessisequivalenttorkj(Ck)=rij(rki(Ck)).Thishastheconsequencethat,ifI|=iC󰀝D,thenI|=jC󰀝D,providedthattheinterpretationisexactforbothconceptsCandD.Thisisapropertythatmaybeverydesirableinsomecontextsbutnotabsolutelynecessaryinothers.Becauseitimposesratherstrongrestrictionsonthemodels,weapplyitonourinterpretationsselectivelyratherthanrequirethatitholdsuniversally,asisdonein[2].

Definition4(Exactness):Given(i,j)∈E,anF-ALCI-interpretationI=󰀘{Ii}i∈V,{rij}(i,j)∈E󰀙issaidtobe(i,j)-󰀁i∩C󰀁j,rij(Ci)=Cj.Iisexactifexactif,foreveryC∈C

itis(i,j)-exact,forall(i,j)∈E.

Notethat,ingeneral,thenotionofexactnessinDefinition4requiresthattheconditionrij(Ci)=Cjholdsforaninfinitecollectionofconceptexpressions.Forourapplicationsthefollowingweakerconceptofexactness,thatdependsonthecontentsofaspecificknowledgebaseunderconsideration,

󰀁iofi-conceptexpressionssuffices.FirstletuscallasetEi⊆C

closedifitisclosedunderconceptsub-expressions,i.e.,foreveryC∈Ei,allsub-conceptsofCarealsoinEi.

Definition5(ExactnessforT):LetE={Ei}i∈V,with

󰀁i,i∈V,beaV-indexedcollectionofclosedsetsEi⊆C

ofconceptexpressionsandI=󰀘{Ii}i∈V,{rij}(i,j)∈E󰀙beanF-ALCI-interpretation.Given(i,j)∈E,Iissaidtobe(i,j)-exactforEif,foreveryC∈Ei∩Ej,rij(Ci)=Cj.IisexactforEifitis(i,j)-exactforE,forall(i,j)∈E.

LetT={Ti}i∈VbeanF-ALCI-ontologyandI=󰀘{Ii}i∈V,{rij}(i,j)∈E󰀙anF-ALCI-interpretation.Iissaidtobe(i,j)-exactforTifitis(i,j)-exactforC:={Ci}i∈VanditissaidtobeexactforTifitis(i,j)-exactforT,forall(i,j)∈E.

AnalternativeconditioncharacterizingtheexactnessofanF-ALCI-interpretationisprovidedinthefollowinglemma(see[6]forproof).

Lemma6:AnF-ALCI-interpretationI=󰀘{Ii}i∈V,{rij}(i,j)∈E󰀙isexactifandonlyif,forallk,i,j∈V,suchthat(k,i),(k,j),(i,j)∈E,rij(rki(Ck))=rkj(Ck),for

󰀁j∩C󰀁k.Theimportingrelationsaredepicted󰀁i∩CeveryC∈C

inFigure2.

k

rki drkj

 d© d󰀆

Ejirij

Fig.2.

ImportingDiagram

Anecessaryandsufficientconditionfortheexactnessofan

F-ALCI-interpretationforagivenV-indexedcollectionEofclosedsetsofconceptexpressions(see[6]forproof).

󰀁i,i∈V,beLemma7:LetE={Ei}i∈V,withEi⊆C

aV-indexedcollectionofclosedsetsofconceptexpressionsandI=󰀘{Ii}i∈V,{rij}(i,j)∈E󰀙anF-ALCI-interpretation.IisexactforEifandonlyif,forallk,i,j∈V,suchthat(k,i),(k,j),(i,j)∈E,rij(rki(Ck))=rkj(Ck),foreveryC∈Ei∩Ej∩Ek.TheimportingrelationsaredepictedinFigure2.

Basedonthedefinitionofanexactinterpretation,wedefineexactmodelsofanF-ALCI-ontology.

Definition8(ExactModel):LetT={Ti}i∈VbeanF-ALCI-ontology.AninterpretationI=󰀘{Ii}i∈V,{rij}(i,j)∈E󰀙isanexactmodelofTifitisexactforTandI|=T.Tissaidtobeexactlyconsistentaswitnessedbya

∗

moduleTwifthereexistsanexactmodelIofTw,suchthatw

Δ=∅.AconceptCisexactlysatisfiableaswitnessedby

∗

TwifthereexistsanexactmodelIofTw,suchthatCw=∅.Finally,aconceptsubsumptionC󰀝DisexactlyvalidaswitnessedbyTw,denotedC󰀝ewDif,foreveryexactmodel

∗ww∗

IofTw,C⊆D.InthiscasewealsowriteTw|=ewC󰀝D.

IV.DECIDABILITYOFF-ALCI

WeestablishthedecidabilityofF-ALCI,byprovidingareductionRfromanF-ALCIKBΣd={Ti}toanALCIKBΣ:=R(Σd):ThesignatureofΣistheunionofthelocalsignaturesofthemodulestogetherwithaglobaltop󰀇,aglobalbottom⊥,localtopconcepts󰀇i,foralli∈V,and,finally,acollectionofnewrolenames{Rij}(i,j)∈E,i.e.,

󰀂

Sig(Σ)=i(Ci∪Ri)∪{󰀇,⊥}∪

{󰀇i:1≤i≤n}∪{Rij:(i,j)∈E}.Moreover,variousaxiomsderivedfromthestructureofΣdareaddedtoΣ.

•ForeachC∈Ci,C󰀝󰀇iisaddedtoΣ.

577573

Authorized licensed use limited to: Iowa State University. Downloaded on June 21, 2009 at 23:08 from IEEE Xplore. Restrictions apply.

•

•

•

ForeachR∈Ri,󰀇iisstipulatedtobethedomainandrangeofR,i.e.,󰀇󰀝∀R−.󰀇iand󰀇󰀝∀R.󰀇iareaddedtoΣ.

ForeachnewrolenameRij,󰀇iisstipulatedtobeits

−

domainand󰀇jtobeitsrange,i.e.,󰀇󰀝∀Rij.󰀇iand󰀇󰀝∀Rij.󰀇jareaddedtoΣ.

ForeachC󰀝D∈Ti,#i(C)󰀝#i(D)isaddedto

󰀁itothesetofALCI-Σ,where#iisafunctionfromC

concepts.Theprecisedefinitionofthemapping#i(C),whichservestomaintainthecompatibilityoftheconceptdomains,isobtainedbyinductiononthestructureofC∈󰀁ie.g.,#i(C)=C,ifC∈Cietc.(See[6]).C

conditionsimposedinF-ALCIareconsiderablymilderthan

theonesimposedontheP-DLsemantics.

ThepreservationofunsatisfiabilityinF-ALCIfollowsfrommonotonicity:AconceptsubsumptionC󰀝D,thatisunsatisfiableaswitnessedbyamoduleTi,isnecessarilyunsatisfiableaswitnessedbyanyothermoduleTjthatimportstheconceptsC,DfromTi.

VI.SUMMARYANDDISCUSSION

Wehaveintroducedamodularontologylanguage,theCFDLF-ALCI,which,tothebestofourknowledge,repre-sentsthefirstmodularontologylanguagetosupportcontextu-alizedinterpretationofalllogicalconnectivesusedwithintheDLmodules.WehaveestablishedthedecidabilityofF-ALCI,whichisaprerequisiteforautomatinginferencewithF-ALCI.IntheCFDLF-ALCI,inferencesarealwaysdrawnfromthepointofviewofawitnessmoduleallowingdifferentmodulestoinferdifferentconsequences,basedontheknowledgethattheyimportfromothermodules.Wehavecharacterizedthetradeoffsbetweentherestrictionsondomainrelations(andhencethesemanticsoftheCFDLF-ALCI)andthedesirablefeaturesoftheresultingmodularontologies(e.g.,monotonicityofinferenceandtransitivepropagationofconceptsubsump-tionsacrossmoduleslinkedbyimportingrelations).WorkinprogressisaimedatexploringmoreexpressiveCFDLsaswellasdevelopingfederatedreasoningalgorithmsfortheresultingCFDLsusingmessagepassingtechniquessimilartothoseintroducedforP-DL.

ACKNOWLEDGMENT

ThisworkwassupportedinpartbyagrantfromtheNationalScienceFoundation(IIS0639230)toVasantHonavarandGioraSlutzkiandinpartbyanexploratoryresearchgrantfromtheIowaStateUniversityNSF-Industry-UniversityCooperativeResearchCenterforInformationProtection.

REFERENCES

[1]JieBao,GioraSlutzki,andVasantHonavar.Asemanticimporting

approachtoknowledgereusefrommultipleontologies.InAAAI,pages1304–1309,2007.

[2]JieBao,GeorgeVoutsadakis,GioraSlutzki,andVasantHonavar.Package

baseddescriptionlogics.InC.Parent,S.Spaccapietra,andH.Stucken-schmidt,editors,OntologyModularization.Springer-Verlag,InPress.[3]ChiaraGhidiniandFaustoGiunchiglia.Localmodelssemantics,

orcontextualreasoning=locality+compatibility.ArtificialIntelligence,127(2):221–259,2001.

[4]JohnL.McCarthy.Generalityinartificialintelligence.Commun.ACM,

30(12):1029–1035,1987.

[5]StephanTobies.Complexityresultsandpracticalalgorithmsforlogics

inknowledgerepresentation.Ph.d.dissertation,TechnischenHochschuleAachen,Aachen,Germany,2001.

[6]GeorgeVoutsadakis,JieBao,GioraSlutzki,andVasantHonavar.F-ALCI:Afullycontextualized,federatedlogicforthesemanticweb.Technicalreport,IowaStateUniversity,Ames,IA,2008.

If,inadditiontothepreviousconditions,foreachsetofimportingrelationsoftheformshowninFigure2andall

−−−

C∈Ci∩Cj∩Ck,∃Rij.(∃Rki.#k(C))=∃Rkj.#k(C)isaddedtoΣ,thenthereductionissaidtobeanexactreductionandisdenotedbyRe(Σd).

WehaveshownthatthereductionRanditsexactcounterpartRearesoundandcomplete[6]:

Theorem9(SoundnessandCompleteness):SupposethatΣd={Ti}i∈VisanF-ALCIontology.ΣdisconsistentaswitnessedbyamoduleTwifandonlyif󰀇wissatisfiable

∗

withrespecttoR(Tw).Moreover,ΣdisexactlyconsistentaswitnessedbyTwifandonlyif󰀇wissatisfiablewithrespect

∗

toRe(Tw).

ThelanguageALCIisanextensionofALCandafragmentofALCIQb.Itiswell-knownthatconceptsatisfiability,con-ceptsubsumptionandconsistencyproblemsforthelanguageALCarePSPACE-complete.ThesameproblemsforthelanguageALCIQbareinPSPACE[5].Hencewehave:

Theorem10:Theconceptsatisfiability,conceptsubsump-tionandconsistencyproblemsforF-ALCIarePSPACE-complete.

V.PROPERTIESOFF-ALCI

AconsequenceofTheorem9isthatRanditsexactcounterpartRearesubsumption-preservingreductions:Thatis,agivensubsumptionisvalidaswitnessedbyamoduleTiofanF-ALCIontologyTifandonlyifitstranslationunder#iisvalidwithrespecttothereductionR(Ti∗)(oritsexactcounterpartRe(Ti∗)asthecasemaybe,see[6]foraproof).AnotherimportantconsequenceofTheorem9isthemono-tonicityoffederatedreasoningwithrespecttoexactmodels.Moreprecisely,wehaveshownthat,givenanF-ALCIontologyΣd={Ti}i∈VandanexactmodelIdofΣd,asubsumptionC󰀝D,withC,D∈Ci∩Cj,(i,j)∈E,isvalidaswitnessedbymoduleTjprovidedthatitisvalidaswitnessedbymoduleTi(see[6]foraproof).

Itisimportanttoemphasizethatthistheoremassertsmono-tonicityofsubsumptionsinF-ALCIonlyforsubsumptionsbetweenconceptsthatactuallyappearinmodulesoftheontologyunderconsideration,and(unlikeinthecaseofP-DLs[1],[2])notforarbitraryconceptsubsumptions(e.g.,subsumptionsthatmightbeaddedtotheontologyatalatertime).Thisshouldnotbesurprisingbecausetheexactness

578574

Authorized licensed use limited to: Iowa State University. Downloaded on June 21, 2009 at 23:08 from IEEE Xplore. Restrictions apply.