Approximation fixpoint theory (AFT) is a robust and popular mathematical framework that characterizes many nonmonotonic semantics, where the construction of stable fixpoints, called stable revision, play a central role. Nondeterministic AFT is a recent development that redefines AFT for a nondeterministic setting to capture disjunctive semantics. This theory departs from traditional AFT by introducing distinct definitions, thus raising the question of whether deterministic AFT can be adopted directly to define nondeterministic stable revision. This work proposes such an alternate theory and creates a new way to study disjunctive semantics in terms of normal (non-disjunctive) knowledge bases. To demonstrate the viability of our framework, we show how to capture stable and partial stable models for disjunctive logic programs. We then study the relationships between this alternative theory and the state-of-the-art nondeterministic AFT.

Abstract Hybrid MKNF Knowledge Bases (HMKNF-KBs) constitute a formalism for tightly integrated reasoning over closed-world rules and open-world ontologies. This approach allows for accurate modeling of real-world systems, which often rely on both categorical and normative reasoning. Conflict-driven solving is the leading approach for computationally hard problems, such as satisfiability (SAT) and answer set programming (ASP), in which MKNF is rooted. This paper investigates the theoretical underpinnings required for a conflict-driven solver of HMKNF-KBs. The approach defines a set of completion and loop formulas, whose satisfaction characterizes MKNF models. This forms the basis for a set of nogoods, which in turn can be used as the backbone for a conflict-driven solver.

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 DPLL-based 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.