An Approximate Core Method To Find A Justification For Large-scale Lightweight Ontologies

Finding justifications for ontology is one of the important reasoning tasks in the field of ontology research.For the large-scale lightweight ontologies that are commonly used in practical applications,researchers believe that the encoding of the ontology classification process into Horn clauses under propositional logic can be used to transform finding justifications for ontology into computing the minimal unsatisfiable set(MUS)under the propositional logic formula.Based on the above analysis,this paper proposes an improved strategy of finding one justification for ontology based on approximate core method,which is suitable for finding the justification for large-scale lightweight ontology and specific entailment.Relevant research shows that the local search(LS)algorithm can better extract approximate MUS from unsatisfiable formula when the propositional logic formula is large-scale,that is to say,it can make local search algorithm show better performance.The specific work of this paper is as follows:(1)Reduce the size of Horn clause set using the modularization approach.The cardinality of the lightweight ontology are large,and the scale of clause set generated by encoding is larger,so it is not practical and feasible to use LS directly on clause set.The selection function is to select clauses based on the correlation of literals between the specific entailment and the SAT instance.The semantic-based selection function can be used to filter out clauses that are irrelevant to specific entailment and delete them,and to retain clauses that are semantically related to implication relations.The modularization method can effectively reduce the scale of the set of clauses generated by encoding.(2)It proposed an approximate core method to find a justification for ontology based on LS.It will cause a waste of time and resources if using the black-box or glass-box directly to find the justification for large-scale lightweight ontology.The idea of approximate methodcan be used to pre-select a subset of unsatisfiable clauses based on ontology and specific entailment,and then extract the justification using the method of finding the exact justification for ontology.Because LS has no special requirements on the size and type of the clauses,the approximate core method based on LS breaks the limitations of existing approximate methods that are only applicable to certain specific types of clauses and are only suitable for small-scale SAT instances.Experiments show that compared with (?)SAT,the approximate core method takes about 69% less time to find a justification on the GO and NCI ontology.(3)It construct an exact solution of finding the exact justification for ontology on the basis of approximate core using the three approaches of destructive approach,constructive approach and SAT-based divide-and-conquer approach.The destructive approach is to iteratively delete clauses from the approximate core;the constructive approach is to iteratively insert clauses into MUS;the SAT-based divide-and-conquer approach can delete multiple clauses at once.In the solution of the above three methods,the satisfiability of the SAT instance is determined based on LS.Compare the structure of algorithm and computational complexity,it is concluded that the SAT-based divide-and-conquer method is more suitable for finding the justification for ontology.The experimental results show that the modularization method can reduce the size of clause set by about 85%.The approximate core method is suitable for large-scale lightweight ontology instances,and the experimental results show that the approximate core method is better than(?)SAT,and the calculation time is improved in an approximately linear relationship based on the size of the ontology.The justification of large-scale lightweight ontology could be calculated by using SAT-based divide and conquer method.