Research On Constructive Justification Extraction For ?L~+ Ontology

?L~+ is a lightweight descriptive logic language which describes the prevailing large-scale medical ontology.Its widespread use has aroused researchers'interest in the research of reasoning under this language.This paper is devoted to solving the extraction of justification in description logic?L~+,realizing the fast pinpointing of axioms to find the minimum axiom set which implies the objective axiom.Black box is the main method for extracting justification,which usually requires multiple implication tests.Since its core idea is to reduce ontology to justification containing object axiom,it can be considered as a destructive extraction process.In this case,this paper proposes a construction method to detect key axioms in ontology,instead of the traditional destructive method of deleting irrelevant axioms from ontology.The specific research contents are as follows:(1)This paper analyzes the justification extraction algorithm proposed by Ye,and points out that this method is actually a constructive extraction method.In addition,we analyze the complexity of the algorithm,make m denote the axiom number in the ontology,and k denote the axiom number in the justification.We suppose that adding an axiom to an empty ontology set requires m times to confirm the implication of the target axiom,and then add the obtained Critical Axioms to justification at most k times,so it requires O(m~*k)calls to the ontology reasoner.(2)we developed a constructive reason extraction algorithm under lightweight large-scale ontology.The algorithm based on the justification extraction problem transformed into the extraction problem of the minimal unsatisfied sub-formula(MUS)of the propositional formula,we proposed the following optimization strategy:(i)Firstly is the clause set refinement and redundancy removal techniques.The clause set refinement is equivalent to the preprocessing technique of MUS extraction for large proposition formulas,in order to reduce the call to the SAT solver.The redundancy removal technique can be used with clause set refinement but not immediately,it requires a simple test to decide when to use an unsatisfactory superset as a valid CNF formula in the next loop.(ii)Secondly is the model rotation technology.Model rotation can be used to iteratively invert the variables in the model assignment and continuously detect the key clauses in the proposition formula to construct MUS.This technology reduces the number of calls to the SAT solver and speeds up the extraction of MUS.The experimental results prove that the constructive justification extraction method can avoid the detection of irrelevant axioms by detecting the key axioms,and it is superior to the traditional black box method in efficiency and performance aspects.And under the lightweight large-scale ontology,the constructive reason extraction method further reduces the number of detections through the strategy of model rotation.