Finding Justifications by Approximating Core for Large-scale Ontologies

Finding Justifications by Approximating Core for Large-scale Ontologies

Mengyu Gao, Yuxin Ye, Dantong Ouyang, Bin Wang

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Doctoral Consortium. Pages 6432-6433. https://doi.org/10.24963/ijcai.2019/905

Finding justifications for an entailment is one of the major missions in the field of ontology research. Recent advances on finding justifications w.r.t. the light-weight description logics focused on encoding this problem into a propositional formula, and using SAT-based techniques to enumerate all MUSes (minimally unsatisfiable subformulas). It's necessary to import more optimized techniques into finding justifications as emergence of large-scale real-world ontologies. In this paper, we propose a new strategy which introduce local search(in short, LS) technique to compute the approximating core before extracting an exact MUS. Although it is based on a heuristic and LS, such technique is complete in the sense that it always delivers a MUS for any unsatisfiable SAT instance. Our method will find the justifications for large-scale ontologies more effectively.
Keywords:
Knowledge Representation and Reasoning: Description Logics and Ontologies
Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving
Constraints and SAT: SAT: Applications