The Satisfiability Reasoning Of Terminological Cycles In Description Logic IS-εL

Description Logics (VLS) is a formalism for representing knowledge which definition the c-oncept of application and describe the information in the field through the structured and formal way. Description logics has the advantegges such as strong and effective expression an and the re-asoning is the core of it. Description Logics has been widely used in software engineerineering and information system of natural language procssing and other fields, especially in the third gen-eration of Web, the semantic web, plays a key r-ole and become the logical basis of W3C reco-mmended Web OWL ontology language.Nebel pioneered the study of description logic cycle definition, then he put forward 3 kinds of semantics to circular definition. Subsequent to this realization, the syntax description graph and semantics description gragh are set up by Baader. The satisfiability and subsumption reasoni-ng algorithms of terminological cycles in description logic εL w.r.t fixpoint semantics and descr-ription semantics are presented w-ith simulation between description graphs. It is proved that th-e satisfiability and subsumption reasoning algorithms of terminological cycles in EL are polyno-mial.With the deeper researchs go on, people have realized that the expression ability of descripti-on logic systems FL0 with the constructors intersection, value restrivton and EL with the constru-ctors intersection, existential quantification are not atrong enough. So people on the basis of the existing research by increasing the constructor method to study. On this basis, this paper makes a preliminary discussion about the satisfiability reasoning ofterminological cycles in LS-εL which is presented by adding inverse constructor, synthesis constructor of role to description logic εL. In this paper, we don’t research the satisfiability about concepts under the fixpoint semantics, bec-ause no matter what kind of semantics could be satisfied, as long as the defined concept has a so-lution, so it is satisfying. Conclusion as a starting point to Baader 1, any A∈Ndef is satisfiable when there is a simulation:GT(?)GJ from description graph GT to semantics description gragh GJ. This conclusion is general, recapitulative but harsh in other words. We try to discuss from th-e details, for 5 different cycles definition according to the method of the graph grammarand sem -antic map by path, determine the satisfiability, then abstract the general conclusions. The necess-ary conditions for the solution about these 4 cycles definitions is semantic path is the tail cycl-e. A necessary and sufficient condition is there is a semantic-tail cycle path matching descriptio-n graph, and then the nodes of the tail cycle path are solutions of the defined concept. So if the s-pecific semantic path exist, we can quickly determine whether the nodes of path issolution of de-fined concept, and the method is very meaningful. The former general way to judge whether an element is a solution are:whether the element satisfies an equality of defined concept or whether there is a simulation:GT(?)GJ from GT to GJ. Anyway the common features of the two methods is each may be the solution should be tested one by one, and it is not fast and effective enough to computing machinery. This article about solution judgment is determined based on the specific s-emantic path, and the result is often a group of related elements whether the solution. If the spec-ific shape of the semantic path is stored in computer to match which is no doubt that the match i-s more faster and efficient, without the one one verification and can save more time and space.The main work of this paper will be proceed as follows:In chapter 2, we introduce the syntax and semantic knowledge etc of TS-εL.In chapter 3, the normalization of a terminological set, description graph and simulation rela-tionship of description logic system TS-εL are defined.In chapter 4, introduce the method of path matching to determine satsfiability of the cycle d-efinition.The main results in this paper are listed below:Proposition 10 N≡3r. N, and α1∈GT, α2∈GJ.α2 is a composite path starting from x, where each edges are r. Moreover, every single path in circulation as the tail. Order S={x|x is a node of α2}, N=S(?)△J, then the following 3 conclusio-ns establishment:1. α, match α2;2. S={x| x is a node of α2}, N=S(?)△J is the solution of N≡(?)r. N;3. conclusion 1 is equivalent to conclusion 2.Proposition 14 N≡(?)r1. N(?)r2. N, and α1∈GT, α2∈GJ.α2 is a composite path starting from x, where each edges are r1 and r2. Moreover, every singl-e path in circulation as the tail. Order S={x|x is a node of α2}, N=S(?)△J, then the following 3 co-nclusions establishment:1. α, match α2;2.S={x|x is a node of α2}, N=S(?)△J is the solution of N=(?)r1. N(?)r2. N;3. conclusion 1 is equivalent to conclusion 2.Proposition 16 N≡(?)r1. N1,N1=(?)r2. N. N, and α1∈GT, α2∈GJ.α2 is a composite path starting from x, where each edges are r1 and r2 appearing alternately. Moreover, every single path in circulation as the tail. Order S={x|(?)y,(?)z, (x, y) ∈r1,∧ (y, z) ∈r2, x i-s a node of α2}, S2={x (?)y,(?)z, (x, y) ∈r2∧ (y, z) ∈r2, x is a node of α2}, N=S1(?)△J, N1=S2(?)△J, then the following 3 conclusions establishment:1. α1 match α2;2. N=S1(?)△J and N1=S2(?)△J are the solutions of N≡(?)r1, N1 and N1=(?)r2. N;3. conclusion 1 is equivalent to conclusion 2.Proposition 19 J1= (A△J1, ·J1), J2= (△J2, ·J2) are two different primitive interpretations of T, a TBox of TS-εL, which is N≡(?)r. N. description graph GT=(Ndef, ET, LT), and semantics des-cription gragh G1J=(△J1, E1, L1), G2J= (△J2, E2,L2). To α∈GT, single path β1∈G1J, β∈G2J, if β1 m-atch β2. then α match β2.