On the Foundations of Conflict-Driven Solving for Hybrid MKNF Knowledge Bases
Riley Kinahan, Spencer Killen, Kevin Wan, Jia-Huai You
TL;DR
This paper addresses the challenge of computing MKNF models for Hybrid MKNF Knowledge Bases by constructing a conflict-driven solving framework. It introduces a formal dependency graph, and adapts completion and loop formulas to HMKNF-KBs, culminating in nogoods that encode the semantic constraints for a CDNL-style solver. The core contributions include a detailed formulation of completion and loop formulas, a complete nogood taxonomy (completion and loop nogoods), and a high-level architecture for a conflict-driven solver tailored to HMKNF-KBs. The work lays the theoretical groundwork for native, scalable reasoning over tightly integrated rules and ontologies, with practical implementation paths and future work on ontology reasoning integration and solver integration.
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.