数据与知识工程 DL

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,教师：常亮,办公室电话,:2291071,手机,办公室：,7212,数据与知识工程,欢迎参加,描述逻辑的推理问题,(1),概念的可满足性,描述逻辑的推理问题,(2),知识库的可满足性,/,知识库的一致性,/ABox,相对于,TBox,的一致性,描述逻辑的推理问题,(3),公式的可满足性,描述逻辑,ALC,的,判定算法,预处理：,转化为,negation normal form(NNF),判断概念可满足性的步骤：,(,令,D,为待判定的概念,),(1),构造初始树,T,0,，仅由单结点,x,0,组成，并且,L(x,0,)=D,；,(2),应用,Tableau,扩展规则对,T,0,进行扩展；,描述逻辑,ALC,的,判定算法,ALC,的,Tableau,扩展规则：,描述逻辑,ALC,的,判定算法,判断概念可满足性的步骤：,(,令,D,为待判定的概念,),(1),构造初始树,T,0,，仅由单结点,x,0,组成，并且,L(x,0,)=D,；,(2),应用,Tableau,扩展规则对,T,0,进行扩展；,如果存在某种扩展方式得到一棵饱和的并且无冲突的树，则返回“概念,D,相对于,TBox T,是可满足的”，,否则返回“概念,D,相对于,TBox T,不可满足”。,冲突：,饱和,/,完全的树：,不能再应用,tableau,扩展规则进行扩展。,描述逻辑,ALC,的,判定算法,Parent,x,Parent,Father,Mother,Man,Parent,Father,Mother,Parent,Father,Mother,Man,Woman,Parent,Father,Mother,Man,Woman,Person,Woman,y,Person,hasChild,z,Person,hasChild,描述逻辑,ALC,的,判定算法,Parent,x,Parent,Father,Man,Parent,Father,Parent,Father,Man,Person,Woman,Parent,Father,Man,Person,Woman,Person,y,Person,hasChild,Parent,Father,Man,Person,Woman,Female,练习,Use tableau algorithm to decide whether the following concept is satisfiable or not.,(,R,.,A,)(,R,.,B,),R,.(,A,B,).,练,习,习,GiventhefollowingTBox,usetableaualgorithmtodecidewhethertheconcept,Grandmother,issatisfiableornot.,对,知,知,识,识,库,库,一,一,致,致,性,性,的,的,判,判,定,定,GivenaTBoxTandanABoxA,usetableaualgorithmtodecidewhetherAisconsistentw.r.t.T.,判,断,断,知,知,识,识,库,库,一,一,致,致,性,性,的,的,步,步,骤,骤,：,：,(1),根,据,据,ABoxA,构,造,造,初,初,始,始,图,图,T,0,。,A,中,出,出,现,现,的,的,每,每,个,个,个,个,体,体,名,名,对,对,应,应,于,于,图,图,中,中,一,一,个,个,结,结,点,点,；,；,每,个,个,结,结,点,点,上,上,标,标,记,记,其,其,对,对,应,应,的,的,个,个,体,体,名,名,所,所,需,需,要,要,满,满,足,足,的,的,概,概,念,念,；,；,结,点,点,之,之,间,间,的,的,边,边,对,对,应,应,于,于,个,个,体,体,名,名,之,之,间,间,所,所,需,需,要,要,满,满,足,足,的,的,角,角,色,色,。,。,(2),应,用,用,Tableau,扩,展,展,规,规,则,则,对,对,T,0,进,行,行,扩,扩,展,展,；,；,如,果,果,存,存,在,在,某,某,种,种,扩,扩,展,展,方,方,式,式,得,得,到,到,一,一,棵,棵,饱,饱,和,和,的,的,并,并,且,且,无,无,冲,冲,突,突,的,的,树,树,，,，,则,则,返,返,回,回,“,“,知,知,识,识,库,库,是,是,一,一,致,致,的,的,”,”,，,，,否则返回“,知,知识库是不,一,一致的”。,例子,Use tableau algorithm todecide whetherthe following knowledge base is satisfiable or not.,练习,Use tableau algorithm todecide whetherthe following knowledge base is satisfiable or not.,对公式可满,足,足性的判定,Givena TBox,use tableaualgorithmto decidewhether aformula is satisfiable or not.,判断公式可,满,满足性的步,骤,骤：,(,令,为待判定的,公,公式,),(1),将公式,转化为析取,范,范式,1,n,；,(2),将每个析取,项,项,i,看作一个,ABox,，应用,Tableau,方法判断其,相,相对于,TBox,是否为一致,的,的；,如果其中至,少,少存在一个,ABoxA,i,是相对于,TBoxT,一,致,致,的,的,，,，,则,则,返,返,回,回,“,“,公,公,式,式,相,对,对,于,于,TBoxT,是,一,一,致,致,的,的,”,”,，,，,否,则,则,返,返,回,回,“,“,公,公,式,式,相,对,对,于,于,TBoxT,不,一,一,致,致,”,”,。,。,练,习,习,GiventhefollowingTBox,usetableaualgorithmtodecidewhethertheformulaissatisfiableornot.,描,述,述,逻,逻,辑,辑,ALC,(,判,定,定,算,算,法,法,的,的,性,性,质,质,),可,终,终,止,止,性,性,：,：,可,靠,靠,性,性,：,：,完,备,备,性,性,：,：,复,杂,杂,度,度,：,：,PSPACE-,完,全,全,算,法,法,复,复,杂,杂,度,度,理,理,论,论,几,类,类,多,多,项,项,式,式,时,时,间,间,复,复,杂,杂,度,度,之,之,间,间,的,的,关,关,系,系,O(1)O(log,n,)O(,n,)O(,n,log,n,)O(,n,2,)O(,n,3,),几,类,类,指,指,数,数,时,时,间,间,复,复,杂,杂,度,度,之,之,间,间,的,的,关,关,系,系,O(2,n,)O(3,n,),O(,n,!)O(,n,n,),P,NP,PSPACE,EXPTIME,NEXPTIME,EXPSPACE,2EXPTIME,N2EXPTIME,P,EXPTIMENP,NEXPTIME,PSPACE,EXPSPACEEXPTIME,2EXPTIME,NEXPTIME,N2EXPTIME,描,述,述,逻,逻,辑,辑,的,的,推,推,理,理,问,问,题,题,(4),判,断,断,概,概,念,念,之,之,间,间,的,的,包,包,含,含,关,关,系,系,判,断,断,概,概,念,念,之,之,间,间,的,的,不,不,相,相,交,交,关,关,系,系,判,断,断,概,概,念,念,之,之,间,间,的,的,等,等,价,价,关,关,系,系,都可以,转,转化为,概,概念的,可,可满足,性,性问题,进而可,以,以转化,为,为公式,的,的可满,足,足性问,题,题,描述逻,辑,辑的推,理,理问题,(5),AxiomEntailment,Whether aknowledge baseKBentailsa DL axiom,.,Whether KB,?,KB,iffConj(KB),is,unsatisfiable,练习,Giventhefollowing knowledgebase,usetableaualgorithmtodecide whetherKB,Mother(Alice).,描述逻,辑,辑的推,理,理问题,(6),InstanceRetrieval,Givena knowledgebase KB anda conceptC,findallindividualnames,a,N,I,forwhich,a,I,C,I,foreverymodelIofKB.,Itisobvious thatanindividualname,a,will be deliveredaspart of theanswerofaninstanceretrieval withrespecttoa conceptCpreciselyifKB|=C(,a,).,Therefore,instance retrievalcanbeperformed by successivelycheckingwhether theconsidered knowledgebase entailsC(,a,)foreveryindividual name,a,.,描述逻,辑,辑的推,理,理问题,(7),Classification,Givena knowledgebase KB,theconceptnamesoccurringthereincanbeput intoahierarchyaccording to their sub-sumptionrelationships.,描述逻,辑,辑的推,理,理问题,(8),其它推,理,理问题,：,：,ConjunctiveQueryAnswering,GivenaknowledgebaseKBandasetofassertionsC,1,(,x,1,),C,n,(,x,n,),R,1,(,x,1,1,x,1,2,),R,m,(,x,m,1,x,m,2,),findalltuples(,p,1,p,2,p,2,)such that,.,Abduction,Explanation,Module Extraction,ConservativeExtensions,教材,BrachmanR,LevesqueH.,Knowledge RepresentationandReasoning,.,Morgan KaufmannPress,2004.,AntoniouG,HarmelenF.,ASemanticWebPrimer.,SecondEdition.,Cambridge,Mass.:MITPress,2008.,参,考,考,书,书,1.BaaderF,CalvaneseD,McGuinnessD,NardiD,andPatel-SchneiderP.F.,TheDescriptionLogicHandbook:Theory,ImplementationandApplications.,CambridgeUniversityPress,2003.,2.Antoniou G,Harmelen F.,著,陈小平等译,.,语义网基础,教,教程,(,第,1,版,),.,机械工业出,版,版社,2008.,3.Bell J.L.,Machover M.,A Course in MathematicalLogic,.,North-Holland PublishingCompany,1977.,教材及参考,书,书,Thanks,！,Question!,演讲完毕，,谢,谢谢观看！,