本文選題：描述邏輯　切入點：IS-εL　出處：《廣西師范大學》2015年碩士論文　論文類型：學位論文

【摘要】：描述邏輯(DLS)是一類知識表示的形式系統(tǒng),其以結構化、形式化的方法定義應用領域的概念及刻畫領域內(nèi)的信息.描述邏輯具有強大的表達能力、有效推理等優(yōu)點,它的核心是推理服務.一直以來描述邏輯受到人們的關注,描述邏輯在信息系統(tǒng)軟件工程以及自然語言處理等領域得到了廣泛的應用.特別是在第三代Web—語義網(wǎng)中扮演者關鍵角色,并成為W3C推薦Web本體語言OWL的邏輯基礎.Nebel率先深入研究描述邏輯循環(huán)定義,提出循環(huán)定義的3種語義.接著F.Baader建立語法描述圖GT和語義描述圖GJ,使用描述圖及圖之間的模擬關系給出描述邏輯系統(tǒng)εL在循環(huán)定義下3中語義的被定義概念的可滿足性推理和包含關系推理算法,并證明推理算法是多項式時間復雜的.隨著研究工作的深入,人們不滿足于只帶交算子和全稱算子的描述邏輯系統(tǒng)FL0。和只帶交算子和存在算子的描述邏輯系統(tǒng)εL的表達力,許多人們在已有研究基礎上通過增加構造子等方式繼續(xù)研究.在此基礎上,本文初步探討增加角色的逆算子,角色的合成算子的描述邏輯系統(tǒng)TS-εL循環(huán)定義術語集的可滿足性推理.本文并不針對F.Baader中循環(huán)定義的3種語義的某一種語義討論,即不設定特定語義環(huán)境討論可滿足性.因為不管是在哪種語義下的可滿足性,只要被定義概念是是有解的,那么其可滿足.以Baader的結論1為起點,在最大不動點語義下,一個待定義的概念A∈Ndef是否可滿足(在給定的基解釋(△,力中)要求的條件：存在一個語法描述圖GT到語義描述圖GJ的一個模擬:GT(?)GJ.該結論較一般化,具有概括性,也可以理解為要求的條件苛刻.本文認為該結論是一個抽象的一般化的結論,所以嘗試從細節(jié)方面探討,針對5個具體的循環(huán)定義依據(jù)其語法圖和語義圖采用路徑匹配的方法判斷其可滿足性,繼而抽象得出一般化的結論.也就是該5個循環(huán)定義有解的必要條件是：語義路徑存在循環(huán).5個循環(huán)定義有解的充要條件是：存在尾部循環(huán)的語義路徑圖使得語法路徑圖與之匹配,并且尾部循環(huán)的語義路徑圖上的結點就是被定義概念的解.使用路徑圖之間的匹配關系給出該5種被定義概念在TS-εL循環(huán)術語集的可滿足性推理算法,并證明了推理算法是多項式時間復雜的.這樣如果存在特定的語義路徑圖,則可以快速判斷該路徑上的結點是否是被定義概念的解.這樣的結論是具有意義的.前人判斷某元素是否是解的方法一般有：把某元素放到被定義式中驗證看其是否滿足左右的定義式或者根據(jù)在最大不動點語義下,根據(jù)Baader的結論1的方法尋找是否存在一個GT到GJ的一個模擬.不管怎樣,這兩種方法的共同特點在于：每個可能是解的元素都要一一驗證.這對于計算機判斷中是不夠快速有效的.關于本文中判斷是解結論中是根據(jù)特定的語義路徑圖的形狀來判定的,并且得到的往往是一群相關元素是否是解的問題.如果把特定形狀的語義路徑圖存儲在計算機中再匹配,毫無疑問這樣的匹配是快速有效率的,不需一一驗證,可以節(jié)省更多時間和空間.本文主要工作如下：第二章,介紹了描述邏輯系統(tǒng)TS-εL的語法及語義等預備知識.第三章,介紹描述圖.第四章,引入路徑匹配的方法判斷循環(huán)定義的可滿足性.本文的主要研究成果總結如下：命題10N≡(?)r. N.其中α1∈GT,α2∈GJ.若α2是一個由某x開始的復合路徑,它的每一條邊都是r.而且,每一單路徑都以循環(huán)為尾部.令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的邊.而且,每一單路徑都以循環(huán)為尾部.令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開始)交替為邊的多個起點的路徑,而且,每一單路徑都以循環(huán)為尾部.令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