Axiom Pinpointing For Lightweight Description Logic Ontology

In recent years,lightweight description logic languages have gradually attracted the attention of experts and scholars.This kind of language with weak expressive ability but low complexity is more suitable for building large-scale ontologies.With the continuous increase of the ontology scale,various logical conflicts will inevitably occur in the process of ontology construction.If these conflicts are not corrected in time,they will affect a series of downstream applications of ontology engineering or knowledge engineering.In order to efficiently debug and generate semantically correct large-scale ontologies,axiom pinpointing methods are usually used to explore defects in the ontology and compute the hidden reasons for logical conclusions.Axiom pinpointing(AP)is an important reasoning task in description logical ontology.Its purpose is to find the justification for a given logical conclusion in the ontology,which is named the minimal axiom set(Min A).Compared with the traditional axiom pinpointing methods,the methods based on the Horn encoding proposed in recent years are more efficient.It encodes the classification process of the ontology into the propositional logic Horn formula,which is called the Horn pinpointing formula,and calculates the minimal unsatisfiable subset(MUS)of the Horn pinpointing formula.Thanks to the development of SAT solving technology,the axiom pinpointing algorithm and implementation tools for solving a single justification have tended to be perfect and efficient,but the research on enumerating all justifications for logical conclusions needs to be further developed.Faced to the problem of justifications enumeration of lightweight description logic ontology,the specific work of this dissertation is as follows:1)The enumeration framework of the minimal unsatisfiable subset,the seed-shrink enumeration framework,is applied to the axiom pinpointing of description logic.In this dissertation,we propose a seed-shrink justifications enumeration system.The system constructs the Horn pinpointing formula for the ontology,and enumerates the sub-formulas(seeds)of the Horn pinpointing formula.Then the algorithm determines the satisfiability of the seeds,finally we obtain all Min As by shrinking the unsatisfiable seeds.2)Under the framework of seed-shrink enumeration,the justification enumeration algorithm is improved.Typically,the seed-shrink process will preferentially enumerate larger seeds,but it is computationally expensive.To solve this problem,this dissertation proposes two optimization strategies: recursive method and replication method.The recursive method gradually narrows the search space at each iteration,from which smaller seeds can be obtained.When there is no new seed in the current recursive level,go back to the previous level and continue searching.The replication method uses the known Min As to gradually expand the scope of the search space,and uses the resolution principle to construct new unsatisfiable seeds from the known results,which replacing part of the satisfiability judgment operations.The above two improved algorithms limit the size of the seeds and reduce the cost of shrinkage.After experimental comparison,both the recursive method and the replication method speed up the enumeration process.In addition,the replication method reduces the frequency of seed consistency determination,making the optimization effect more obvious.3)In addition to using recursion and replication strategies to optimize the justifications enumeration,this dissertation also performs parameter tuning of the SAT solver for the Horn pinpointing formula to further improve the overall efficiency of the enumeration process.Specifically,we modified the restart strategy,learning clause management method and VSIDS branch heuristic decay parameter in the satisfiability decision according to the structure and characteristics of Horn pinpointing formula,which makes the new solver more suitable for the satisfiability judgment of seeds in Horn pinpointing formula.The experimental results show that the satisfiability solver customized in this dissertation generally improves the efficiency of seed satisfiability determination,and further accelerates the seed-shrink justification enumeration algorithm.In this dissertation,experiments were carried out using the bio-medical ontologies Gene,Galen,NCI and the large ontology Snomed-CT.The experimental results show that the Min As enumeration algorithm based on seed-shrink system can effectively calculate all justifications for a given inference,and the time complexity is better than the exist algorithms EL2 MUS and SATPin.The replication method,which uses a customized satisfiability solver,has the best performance among all algorithms.