| Description Logics(DLs) are a well-known family of knowledge representation formalisms.they are based on the notion of concepts(unary predicates, classes) and roles(binary relations),and are mainly characterised by constructors that allow complex concepts and roles to be builtfrom atomic ones. they represent the knownledge of an application domain by first definingthe relevant concepts of the domain(its terminology), and then using these concepts to specifyproperties of objects and individuals occurring in the domain(the world description). Sound andcomplete algorithms for the interesting inference problems such as subsumption and satisfiabilityof concepts are known for a wide variety of DLs.Recently, a substantial amount of work has been carried out in the context of DescriptionLogics and they have had a more complete theory system. In order to make description logics to handle more general fuzzy information, Straccia has discovered a fuzzy description logic(?)-ALCbased on a certainty lattice. Stoilos and his partners have presented a fuzzy descriptionlogic f-SI for providing the ability of expressing multimedia knowledge. Transitive roles and inverse roles play an important role not only in the adequate representation of complex, aggregatedobjects, but also for reasoning with conceptual data models. Based on these methods, this paperproposes a new description logic (?)-SI, and defines its syntax, semantics. we also present aconstraint propagation calculus for reasoning in it and the proof of soundness and completeness.In contrast to (?)-ALC and f-SI, the system (?)-SI we will present is more expressive and canprove that the (?)-SI reasoning tasks are P space.The main content of this paper will proceed as follows:In introduction part, introduces the historical background and present situation which arerelative with the content of this paper;In chapter 1, reviews the basic theoretical knownledge of description logic SI.In chapter 2, introduces the syntax, semantics of description logic (?)-SI whose value takesfrom a certainty lattice and presents a constraint propagation calculus for reasoning in it.In chapter 3, gives the proof of termination, soundness and completeness in detail. Finally,it discusses the complexity of reasoning algorithm. In chapter 4, it surnrnarizes some focal point of this paper and gives the research directionwe can do in the future.To get the theoretical results, we assume:(A1) For a certainty values set T, we assume that there is a function from T to T, callednegation function(denoted (?))that is anti-monotone w.r.t (?) and satisfies (?)α=α, (?)α∈T.(A2) Assume that T is finite if the certainty lattice (?)= is not a total order set.(A3) Assume that certainty lattice (?) is safe. We call a certainty lattice (?) safe. iff (ⅰ) forany c∈T, |D?(c)| is finite; (ⅱ) the decision problem whether a set of assertions is inconsistentis decidable.(A4) In order to ensure the computational complexity of algorithm on combined complexityis pspace we have to assume that(ⅰ)(?) is safe; (ⅱ)for any set of (?)-assertions S and certaintyvalue c, |D?(c)|is polynomially bounded w. r. t, combined complexity; and (ⅲ)deciding whethera set of (?)-assertions S contains a clash can be done in polynomially space w. r. t, combinedcomplexity.These assumptions are reasonable becuase it is adequate to realistic application in our dailylife and the procedure of this paper will be implemented easily in experiments.We have following conclusions in this paper:proposition 1 let∑be a KB in which no <(a, b): R (?) c> occurs and consider <α(?) c>. IfLemma 1 An (?)-SIAboxA is consistent if and only if there exists a fuzzy tableau for A.The reasoning algorithm of description logic (?)-SI, it is main content of this paper and isa keypart for every formal language.Lemma 2 Let T be a completion forest obtained by applying the expansion rules to anAboxA, then, for every node x in T, B(x)(?)(x).Lemma 3 For each AboxA, the tableaux algorithm terminates.theorem 1 If the expansion rules can be applied to an AboxA such that they yield acomplete and clash-free completion forest, then A has a tableau.theorem 2 If A has a tableau, then the expansion rules can be applied in such a way thatthe tableaux algorithm yields a complete and clash-free completion forest for A.theorem 3 The tableaux algorithm is a decision procedure for the consistency.
|
PDF Full Text Request