=Paper= {{Paper |id=Vol-1879/paper10 |storemode=property |title=None |pdfUrl=https://ceur-ws.org/Vol-1879/paper10.pdf |volume=Vol-1879 }} ==None== https://ceur-ws.org/Vol-1879/paper10.pdf 
      Lean Kernels in DLs (Extended Abstract)?

Rafael Peñaloza1 , Carlos Mencı́a2 , Alexey Ignatiev3 , and Joao Marques-Silva3
         1
          Free University of Bozen-Bolzano, Italy (penaloza@inf.unibz.it)
                 2
                   University of Oviedo, Spain (cmencia@gmail.com)
     3
       University of Lisbon, Portugal ({aignatiev,jpms}@ciencias.ulisboa.pt)

    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 finding all the relevant axioms:
those axioms that appear in at least one MinA (or justification) for a given
entailment. Unfortunately, deciding whether an axiom is relevant is a compu-
tationally hard problem, even for very weak logics with linear-time entailment
relations.
    Lean kernels (LKs) were first 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 unsatisfiability
of a given formula. As such, it is an overapproximation of the set of all relevant
clauses for explaining unsatisfiability. Recent work has shown that LKs provide
an effective optimization for enumerating the set of all MinAs (or MUSes, as
they are called in the propositional satisfiability community). Indeed, LKs are
comparatively fast to compute, and typically do not contain many superfluous
clauses.
    Interestingly, an analogous notion of LKs has never been considered within
the DL community. One difficulty when introducing such a notion is that it
depends on a specific decision procedure (like resolution). In this work, we con-
sider an abstract notion of decision procedures, called consequence-based meth-
ods, which include resolution, the completion algorithm for EL, and many other
procedures for expressive description logics. We define LKs based on these meth-
ods, and show that they can be modified 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. Specifically, we show that in ALC and EL+ , LKs are always strictly
contained in locality-based modules. Moreover, an empirical analysis over well-
known large EL+ ontologies shows that the differences are significant: the size
of the LK is in many cases one-tenth or less than the locality-based modules.
Thus, LKs provide an effective approximation of the set of relevant axioms.

?
    This extended abstract presents work previously published at ESWC 2017 as:
    Rafael Peñaloza, Carlos Mencı́a, Alexey Ignatiev, Joao Marques-Silva: Lean Ker-
    nels in Description Logics. In Proc. of ESWC (Part 1) 2017: 518-533.