描述逻辑概念可满足性推理的研究

《描述逻辑概念可满足性推理的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、浙江大学博士学位论文摘要在WEB上提供机器可理解的知识并实现WEB信息的自动处理逐渐成为人们重要的生活、工作需求之一。这其中，如何恰当地表示知识并在其上实现快速有效的推理以找出其它的相关知识是这个浩大工程中的关键点。随着研究的深入，关于知识表示与推理的研究已经转移到集中了其它诸多表示方法的优点而克服了它们缺点的描述逻辑当中。本文所关注的是在描述逻辑当中如何实现高效的概念可满足性的推理。因为概念可满足性是描述逻辑推理的基本问题之一，对该类问题进行高效处理具有相当重要的意义。经过一段时期的研究，本文取得了如下研究成果：1)提出了

2、基于概念描述本身进行推理的新思路。概念可满足性算法Tableau是基于断言库ABoX可满足性的，由此也带来了许多不必要的操作以及空间浪费。本文所提出的CDNF(CompleteDisjunctiveNormalForm)算法则是直接在初始概念描述上构建可满足性已知的完全析取范式，实现了“计算”概念可满足性，并可取得更好的空间性能。2)提出了面向皿例的基础型CDNF算法。在描述逻辑基础语言灿何中，Tableau算法就已存在描述重复情况。而CDNF算法在不改变描述的语义的前提下，移去V算子并合并部分描述，最后形成一个可满足性直接

3、可知的描述，几乎消除了描述重复的现象，且移去V算子可进一步降低了空间的使用。3)提出了面向灿弧的子句重用的CDNF判定算法。在描述逻辑语言舢舭中，逆角色使得描述的重组织存在反复的可能，而传递性角色则可能导致描述无限扩展。必须采取一定的策略及时检测并阻止这种不必要的扩展。CDNF算法的子旬重用与Tableau算法的精化阻塞技术相比，效果相同但只需更少的空间。4)提出了面向SHOI矾／(D)的CDNF算法。在与本体描述语言OWLDL相对应的描述逻辑SHOI：gV(D)中，CDNF算法在此要处理命名个体、数据类型，以及角i浙江大学

4、博士学位论文摘要色分层。此时，一个j算子的出现代表的涵义往往是两种事物之间的多重关系。此外，在前述基础上再考虑数量限制约束后，必须对子句重用的判断施加更强的条件。此时，CDNF算法相对于Tableau算法的优越性主要体现在减少n、u算子导致的描述重复。关键词：描述逻辑，推理，可满足性，析取范式浙江大学博士学位论文AbstractToprovidemachineunderstandableknowledgeoninternetSOthatWEBinformationcanbeprocessedautomaticallyhasg

5、raduallybecomeallimportantneedinpeople’Slifeandwork．Onthewaytothisgoal，howtorepresentknowledgeandinferuponitefficientlyisthecrucialissueamidthislmgeprojeet．Withresearchdeepening，thishasalreadytransferredtotheresearchofdescriptionlogicsforitsadvantagesoverothermetho

6、lds．ThisthesisfocusesOllhowtorealizeefficientreasoningonconceptsatisfiabilityindescriptionligics，forconceptsatisfiabilityisoneofthebasicissuesindescriptionlogicreasoning．Afteracertainperiodofresearch,wehaveachieved：1)Anewideaofreasoningondescriptionsdirectly．Concep

7、tsatisfiabilityalgorithmTableauisbasedonthesatisfiabilityofABox，whichbringslotsofdescriptionoverlaps．，nleCDNFalgorithmsinthispaperaretogainthesatisfiabilityjudgementofaconceptbyfindingasatisfiabilityself-tellingcompletedisjunctivenormalformdirectlybasedonitsdescrip

8、tion，thus‘'workingout'’thesatisfiability．Therefore，ithasbetterspatialperformance．2)AbasicCDNFalgorithmfor灿例Eveninthebasicdescriptionlogiclanguage