| Axiom Pinpointing(AP)is an important research topic in the ontology field,with the goal of finding hidden reasons for given logical entailments,helping users understand requirements,or debugging and fixing inconsistent ontologies.As ontologies are being applied more widely,the research on describing logical ontologies with strong expressivity has become a trend,while balancing the ability to describe logical expressions and the efficiency of reasoning engines has always been a focus of AP research.In recent years,a consequence-based reasoning algorithm has shown good performance in basic reasoning problems,attracting the attention of researchers.There are two main approaches to AP based on existing ontology reasoning engines: glass-box and black-box methods.Glass-box methods can directly obtain the localization of reasoning results and are closely intertwined with the reasoning algorithm,but their portability is poor.Black-box methods do not care about the internal structure of the reasoning engine,nor do they care about the ontology language and axiom types.Additionally,they can obtain localization results without modifying the reasoning algorithm,but their efficiency is often low due to repeated calls to the reasoning engine.Based on this,this paper uses the consequence-based reasoning algorithm from both glass-box and black-box perspectives to address the axiom pinpointing problem in ontologies with strong descriptive logic.The specific work is as follows:(1)Using a multi-typed clause equal logic that preserves the implication relationship and satisfiability,the ontology axiom is converted into DL clauses for further reasoning.Using the modified consequence-based rule(i.e.,localization rule)to trace the specific process of reasoning and introducing the concept of localization formula to establish the correspondence between the Boolean formula tag of the clause and the set of all minimal axioms for logical entailment.By tracking the reasoning process under the consequence-based decision algorithm,the localization task of axioms is achieved by solving the localization formula of clauses.(2)Referring to the enumeration algorithm of the smallest unsatisfiable subset in the SAT solving research field,a seed-shrink enumeration framework based black-box localization algorithm is proposed for strong expressive descriptive logical ontologies.The algorithm enumerates all subsets(also known as seeds)of the axiom set and selects and retrieves the seeds from the power set to be explored based on the seed-shrink framework.Based on the judgment results,pruning is performed,and Min A is obtained under the condition of satisfaction.The algorithm can accurately calculate all Min A for a given logical entailment,avoiding missing or duplicate results.(3)Analyzing the basic process of the seed-shrink framework and improving the seed-shrink algorithm by adopting a parallelization strategy.Unlike the seed-shrink algorithm for propositional logic,the efficiency of each judgment process for seeds in the algorithm is extremely high,so parallelization strategy is not meaningful.In the seedshrink localization algorithm for strong descriptive logic ontologies,each judgment process after obtaining a seed needs to call the reasoning engine to reason over axiom sets with high complexity,resulting in a high time cost.Therefore,a parallelization strategy is used in the recursive process of obtaining seeds to reduce the time cost generated by repeated calls to the external reasoning engine and improve the localization efficiency.Experiments show that both the consequence-based glass-box and black-box localization methods proposed in this paper can calculate all reasons for a given logical entailment,with no missing or duplicate results.Compared with existing localization algorithms,they have some competitiveness and development potential. |
