Unfounded Sets for Disjunctive Hybrid MKNF Knowledge Bases

TL;DR

This paper introduces a formal notion of unfounded sets for disjunctive hybrid MKNF knowledge bases, aiming to enhance solver efficiency by enabling better constraint propagation in combined answer set programming and ontologies.

Contribution

It formalizes unfounded sets for hybrid MKNF knowledge bases, analyzes their complexity, and discusses integration into solvers, addressing challenges posed by ontologies.

Findings

Formal definition of unfounded sets for hybrid MKNF

Identification of lower complexity bounds

Discussion on integration challenges and solver improvements

Abstract

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.