Unfounded Sets for Disjunctive Hybrid MKNF Knowledge Bases
  Combining the closed-world reasoning of answer set programming (ASP) with the
open-world reasoning of ontologies broadens the space of applications of
reasoners. Disjunctive hybrid MKNF knowledge bases succinctly extend ASP and in
some cases without increasing the complexity of reasoning tasks. However, in
many cases, solver development is lagging behind. As the result, the only known
method of solving disjunctive hybrid MKNF knowledge bases is based on
guess-and-verify, as formulated by Motik and Rosati in their original work. A
main obstacle is understanding how constraint propagation may be performed by a
solver, which, in the context of ASP, centers around the computation of
\textit{unfounded atoms}, the atoms that are false given a partial
interpretation. In this work, we build towards improving solvers for hybrid
MKNF knowledge bases with disjunctive rules: We formalize a notion of unfounded
sets for these knowledge bases, identify lower complexity bounds, and
demonstrate how we might integrate these developments into a solver. We discuss
challenges introduced by ontologies that are not present in the development of
solvers for disjunctive logic programs, which warrant some deviations from
traditional definitions of unfounded sets. We compare our work with prior
definitions of unfounded sets.
