Research On The Reasoning Of Concept Satisfiability In Description Logics

To provide machine understandable knowledge on internet so that WEB information can be processed automatically has gradually become an important need in people's life and work.On the way to this goal,how to represent knowledge and infer upon it efficiently is the crucial issue amid this huge project.With research deepening,this has already transferred to the research of description logics for its advantages over other metholds.This thesis focuses on how to realize efficient reasoning on concept satisfiability in description ligics,for concept satisfiability is one of the basic issues in description logic reasoning.Aider a certain period of research,we have achieved:1) A new idea of reasoning on descriptions directly.Concept satisfiability algorithm Tableau is based on the satisfiability of ABox,which brings lots of description overlaps.The CDNF algorithms in this paper are to gain the satisfiability judgement of a concept by finding a satisfiability self-telling complete disjunctive normal form directly based on its description,thus "working out" the satisfiability.Therefore,it has better spatial performance.2) A basic CDNF algorithm for ALCN.Even in the basic description logic language ALCN,there is already the phenomenon of description overlaps.CDNF algorithm removes the(?) operators and merges parts of descriptions under the premise of not changing their semantics,and obtains a satisfiability-known description,which eliminates almost all the description overlaps and further reduces the spatial cost by deleting(?) operators.3) A clause-reusing CDNF algorithm for ALCNI_R+.In the basic description logic language ALCNI_R+,while inverse roles make repetitiveness in reorganization possible,transitive roles may lead to endless expansion of a description.Certain measures should be taken to detect and stop such unnecessary unfolding. Compared with the refined blocking in Tableau,the reusing of clauses in CDNF can gain same effect with less space. 4) An advanced CDNF algorithm for SHOIN(D).In SHOIN(D) which corresponds to Ontology language OWL DL,CDNF algorithm here has to process named individuals,datatypes,and role hierarchy.At this moment,one occurrence of(?) operator may imply multiple relations between two kinds of objects.Besides, considering number restrictions atop these conditions,the judgement of reusable clauses needs stronger requirements.Here,the advantages of CDNF over Tableau are embodied by reducing the description overlaps caused by operator∩and∪.