? This extended abstract presents work previously published at ESWC 2017 as: Rafael Pen~aloza, Carlos Menc a, Alexey Ignatiev, Joao Marques-Silva: Lean Kernels in Description Logics. In Proc. of ESWC (Part 1) 2017: 518-533.
When trying to understand the axiomatic causes for a consequence to follow from an ontology (e.g. to correct erroneous entailments), it is often convenient to reduce the search space to include only those axioms that play an active role in these entailments. That is, one is interested in nding all the relevant axioms: those axioms that appear in at least one MinA (or justi cation) for a given entailment. Unfortunately, deciding whether an axiom is relevant is a computationally hard problem, even for very weak logics with linear-time entailment relations.
Lean kernels (LKs) were rst introduced in the area of propositional logic as a means to approximate the set of all relevant axioms. In a nutshell, the lean kernel is the set of all clauses that appear in a resolution proof for unsatis ability of a given formula. As such, it is an overapproximation of the set of all relevant clauses for explaining unsatis ability. Recent work has shown that LKs provide an e ective optimization for enumerating the set of all MinAs (or MUSes, as they are called in the propositional satis ability community). Indeed, LKs are comparatively fast to compute, and typically do not contain many super uous clauses.
Interestingly, an analogous notion of LKs has never been considered within the DL community. One di culty when introducing such a notion is that it depends on a speci c decision procedure (like resolution). In this work, we consider an abstract notion of decision procedures, called consequence-based methods, which include resolution, the completion algorithm for EL, and many other procedures for expressive description logics. We de ne LKs based on these methods, and show that they can be modi ed to compute LKs for all consequences with only a linear time overhead w.r.t. standard reasoning. As for propositional formulas, LKs in DLs preserve all relevant axioms. In other words, these sets are small MinA-preserving modules.
We then compare LKs with other known approximations of the set of relevant axioms. Speci cally, we show that in ALC and EL+, LKs are always strictly contained in locality-based modules. Moreover, an empirical analysis over wellknown large EL+ ontologies shows that the di erences are signi cant: the size of the LK is in many cases one-tenth or less than the locality-based modules. Thus, LKs provide an e ective approximation of the set of relevant axioms.