IS-εL系统循环定义术语集的可满足性推理
发布时间：2018-03-08 19:17
本文选题：描述逻辑 切入点：IS-εL 出处：《广西师范大学》2015年硕士论文 论文类型：学位论文
【摘要】：描述逻辑(DLS)是一类知识表示的形式系统,其以结构化、形式化的方法定义应用领域的概念及刻画领域内的信息.描述逻辑具有强大的表达能力、有效推理等优点,它的核心是推理服务.一直以来描述逻辑受到人们的关注,描述逻辑在信息系统软件工程以及自然语言处理等领域得到了广泛的应用.特别是在第三代Web—语义网中扮演者关键角色,并成为W3C推荐Web本体语言OWL的逻辑基础.Nebel率先深入研究描述逻辑循环定义,提出循环定义的3种语义.接着F.Baader建立语法描述图GT和语义描述图GJ,使用描述图及图之间的模拟关系给出描述逻辑系统εL在循环定义下3中语义的被定义概念的可满足性推理和包含关系推理算法,并证明推理算法是多项式时间复杂的.随着研究工作的深入,人们不满足于只带交算子和全称算子的描述逻辑系统FL0。和只带交算子和存在算子的描述逻辑系统εL的表达力,许多人们在已有研究基础上通过增加构造子等方式继续研究.在此基础上,本文初步探讨增加角色的逆算子,角色的合成算子的描述逻辑系统TS-εL循环定义术语集的可满足性推理.本文并不针对F.Baader中循环定义的3种语义的某一种语义讨论,即不设定特定语义环境讨论可满足性.因为不管是在哪种语义下的可满足性,只要被定义概念是是有解的,那么其可满足.以Baader的结论1为起点,在最大不动点语义下,一个待定义的概念A∈Ndef是否可满足(在给定的基解释(△,力中)要求的条件：存在一个语法描述图GT到语义描述图GJ的一个模拟:GT(?)GJ.该结论较一般化,具有概括性,也可以理解为要求的条件苛刻.本文认为该结论是一个抽象的一般化的结论,所以尝试从细节方面探讨,针对5个具体的循环定义依据其语法图和语义图采用路径匹配的方法判断其可满足性,继而抽象得出一般化的结论.也就是该5个循环定义有解的必要条件是：语义路径存在循环.5个循环定义有解的充要条件是：存在尾部循环的语义路径图使得语法路径图与之匹配,并且尾部循环的语义路径图上的结点就是被定义概念的解.使用路径图之间的匹配关系给出该5种被定义概念在TS-εL循环术语集的可满足性推理算法,并证明了推理算法是多项式时间复杂的.这样如果存在特定的语义路径图,则可以快速判断该路径上的结点是否是被定义概念的解.这样的结论是具有意义的.前人判断某元素是否是解的方法一般有：把某元素放到被定义式中验证看其是否满足左右的定义式或者根据在最大不动点语义下,根据Baader的结论1的方法寻找是否存在一个GT到GJ的一个模拟.不管怎样,这两种方法的共同特点在于：每个可能是解的元素都要一一验证.这对于计算机判断中是不够快速有效的.关于本文中判断是解结论中是根据特定的语义路径图的形状来判定的,并且得到的往往是一群相关元素是否是解的问题.如果把特定形状的语义路径图存储在计算机中再匹配,毫无疑问这样的匹配是快速有效率的,不需一一验证,可以节省更多时间和空间.本文主要工作如下：第二章,介绍了描述逻辑系统TS-εL的语法及语义等预备知识.第三章,介绍描述图.第四章,引入路径匹配的方法判断循环定义的可满足性.本文的主要研究成果总结如下：命题10N≡(?)r. N.其中α1∈GT,α2∈GJ.若α2是一个由某x开始的复合路径,它的每一条边都是r.而且,每一单路径都以循环为尾部.令S={x|x是α2的结点元素},N=S(?)ΔJ,则以下3个结论成立：1.α1与α2匹配；2.S={x|x是α2的结点元素}.则N=S(?)ΔJ是N≡(?)r.N的解；3.结论1与结论2等价.命题14N≡(?)r1. N(?)r2. N.α2∈GJ,若α2是由某x开始的复合路径,该路径上的每个结点分别存在r1,r2的边.而且,每一单路径都以循环为尾部.令S={x|x是α2的结点元素},N=S(?)ΔJ,则以下3个结论成立：1.α1与α2匹配；2.S={x|x是α2的结点元素}.则N=S(?)ΔJ是N≡(?)r1. N(?)r2. N的解；3.结论1与结论3等价.命题16N≡(?)r1. N1,N1≡(?)r2.N.α2∈GJ,α2是一个由某元素x开始的复合路径,它是以r1,r2(以r1或者r2开始)交替为边的多个起点的路径,而且,每一单路径都以循环为尾部.令S1={x|(?)y,(?)z(x,y)∈r1∧(y,z)∈r2,x是α2的结点元素},S2={x|(?)y,(?)z(x,y)∈r2∧(y,z)∈r2,x是α2的结点元素},S=S1US2={x|x是α2的结点元素},N=S1(?)△J,N1=S2(?)△J,则以下3个结论成立：1.α1与α2匹配；2.N=S1(?)△J,N1=S2(?)△J分别是N≡(?)r1. N1,N1≡(?)r1.N的解；3.结论1与结论2等价.命题19 给定描述逻辑TS-εL的TBox丁是N=(?)r.N,J1=(△J1,·J1),J2=(△J2,·J2)是两个不同的基解释.语法图GT=(Ndef,ET,LT),语义图为G1J=(△J1,E1,L1),G2J=(△J2,E2,L2).对于α∈GT,单路径β1∈G1J,单路径β2∈G2J,如果α与β1匹配,β1与β2匹配,那么α与β2匹配.
[Abstract]:Description Logic (DLS) is a family of knowledge representation formalisms, the concept of structured, formal methods to define the characterization and application in the field of information. The description logic has a powerful expressive ability, effective reasoning etc., which is the core of the reasoning service. To describe the logic of attention. The description logic is widely used in the information system of software engineering and other fields. Especially, Natural Language Processing plays a key role in the third generation of Web in semantic web, and become a logical foundation.Nebel W3C recommended Web OWL ontology language to study the description logic cycle definition, puts forward 3 kinds of semantic definition. Then establish F.Baader circulation grammar figure GT description and semantic description in figure GJ, used to describe the relationship between the simulated graph and graph description logic system in the epsilon L cycle definition 3 semantic concept can be defined The reasoning and inference algorithm contains, and prove that the inference algorithm is polynomial time complexity. With in-depth research, expression of people are not satisfied with only the FL0. description logic system and universal operator and cross operator and operator has a description logic system L, a lot of people based on existing study on the structure by increasing the sub way to continue the study. On this basis, this paper makes a preliminary discussion on the role of the increase of the inverse operator, composition operator role description logic system TS- epsilon L cycle definition of terminological satisfiability reasoning. This is not a semantic 3 semantic cyclic definitions in F.Baader are discussed, i.e. don't set a specific semantic environment to discuss satisfiability. Because no matter what semantics could be satisfied, as long as the defined concept is the solution, so it can meet with the conclusion of Baader 1. Starting point, in the greatest fixpoint semantics, a definition of the concept of A and whether Ndef can meet (explained in a given base (delta force,) requirements: there is a syntax description of figure GT to a semantic description: GT simulation figure GJ (?) GJ. the more general conclusion out, general, can also be understood as the requirements of harsh conditions. This paper argues that this conclusion is an abstract generalization of the conclusion, so try to explore from the details, for 5 concrete circular definition according to the method of its syntax and semantic graph map using path matching judgment which can meet, and then get the abstract the general conclusion. It is to define the 5 cycle of the necessary conditions for the solutions are: semantic path exists in cycle.5 cycle defined the necessary and sufficient conditions are: the existence of semantic path graph tail cycle makes grammatical path graph matching, semantic path and cycle tail Node diameter on the graph is defined by the concept of solution. Using the path graph matching relationship between the 5 kinds of concepts defined in TS- e L terminological cycles satisfiability reasoning algorithm, and prove that the inference algorithm is polynomial time complexity. So if the semantic path specific, can quickly judge the path is defined by the concept of solution. This conclusion is of significance. To determine whether the element is a previous solution methods are: a defined type element into the verification to see if they meet the definition about or according to the maximum fixed point semantics, according to the conclusion of Baader 1 the method to find out whether there is a GT to a simulated GJ. Anyway, is a common feature of these two methods: every possible solution is verified. The elements have 11 for computer judgment is not fast enough Speed effectively. This paper is about the judgment is determined based on semantic path specific solution for the shape of the conclusion, and often is whether a group of related elements is the solution of the problem. If the semantic path graph specific shape, then stored in the computer, there is no doubt that the match is fast and efficiency that does not need to be verified one by one, can save more time and space. The main work of this paper is as follows: the second chapter introduces the description logic TS- epsilon L syntax and semantic and other preliminaries. The third chapter, introduces the description graph. The fourth chapter introduced the path matching cycle definition of Satisfiability judgement. Main research results in this paper are summarized as follows: proposition 10N = (?) r. N. alpha 1 in GT, and if GJ. alpha 2 alpha 2 is a start from a x composite path, each of its edges are R. and every single path to circulation as the tail of the S={x|. x鏄，
本文编号：1585202
本文链接：https://www.wllwen.com/kejilunwen/yysx/1585202.html
