Abstract
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 introduces 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