Fixpoint Characterizations of Disjunctive Hybrid
MKNF Knowledge Bases
Spencer Killen1 , Jia-Huai You1
1
    University of Alberta, Edmonton, Alberta, Canada


                                         Abstract
                                         Combining answer set programming with ontologies is of great theoretical and practical interest. Hybrid
                                         MKNF is a semantics that combines ASP with ontologies without increasing the solving complexity.
                                         While there are efficient solvers for ASP and ontologies, efficient solvers for hybrid MKNF have yet to be
                                         constructed. In this work, we address some issues that must be solved before a CDNL-based (conflict-
                                         driven nogood learning) solver for hybrid MKNF knowledge bases can be developed. We formulate a
                                         framework to characterize disjunctive hybrid MKNF semantics through a family of fixpoint operators,
                                         then contextualize this framework by demonstrating that it could be possible to integrate it into a solver.
                                         Crucially, our approach can be performed without relying on a dependency graph. Finally, we recognize
                                         a property of our characterization that is analogous to head-cycle free disjunctive logic programs and
                                         demonstrate how to exploit this property to improve solver efficiency.

                                         Keywords
                                         Hybrid MKNF Knowledge Bases, Disjunctive ASP, Fixpoint Computation




1. Introduction
Efficient answer set programming (ASP) solvers are highly desired. Proven solver techniques,
such as constraint-driven nogood learning (CDNL) [1], are essential to constructing highly
efficient ASP solvers. Solvers that incorporate extensions to ASP allow for a wider range of
problems to be tackled with solvers. One powerful extension is to extend ASP programs with
ontologies, combining closed- and open-world reasoning. While researchers have proposed a
variety of hybrid semantics and have developed efficient CDNL solvers for them [2, 3], these
semantics trend towards ASP modulo theories, a class of semantics where stable models are
validated by an external theory. The external theories supported by these hybrid semantics
are in general nonmonotonic, and thus are ill-suited to capture the monotonic reasoning of
ontologies.
   Hybrid MKNF (Minimal Knowledge Negation as Failure) knowledge bases are one exception
to this trend; Introduced by Motik and Rosati [4], this semantics equips an ASP program with a
monotonic fragment of first-order logic obtained from an ontology. Hybrid MKNF is suitable for
incorporating into a solver because it is faithful to the underlying semantics of the description

The proofs for this work are available at the following URL:
https:// github.com/ sjkillen/ FixpointCharacterizations/ raw/ master/ proofs.pdf
14th Workshop on Answer Set Programming and Other Computing Paradigms
" sjkillen@ualberta.ca (S. Killen); jyou@ualberta.ca (J. You)
 0000-0003-3930-5525 (S. Killen); 0000-0001-9372-4371 (J. You)
                                       Copyright © 2021 Spencer Killen and Jia-Huai You. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)
logic and ASP without increasing complexity [4]. The state-of-the-art of hybrid MKNF solving
is only marginally more efficient than guess-and-verify, but a CDNL-based solver would be
much more efficient. One major obstacle to developing an efficient CDNL-based solver for
disjunctive hybrid MKNF is the unavailability of syntactic dependency; In general, a dependency
graph can not be generated for a hybrid knowledge base without knowing the internal structure
of the ontology. A framework that treats the ontology as a black box has a broader range of
applications than a solver that must be tuned for a particular ontology. Atom dependency
analysis is crucial for both model verification and conflict generation.
   In this work, we present a framework for disjunctive hybrid MKNF knowledge bases that
utilizes fixpoint operators. This framework does not rely on dependency graphs and the only
restriction it imposes on the description logic is that the entailment relation can be checked in
polynomial time.


2. Related Work
Numerous accounts on the complexity of disjunctive ASP [5, 6, 7, 8] agree that the complexity of
computing answer sets of disjunctive logic programs resides in the class Σ𝑃2 . Leone et al. show
that answer sets can be computed by generating unfounded-free interpretations [5], while Lee
and Lifschitz show that loop formulas in conjunction with a program’s Clark completion can be
used for model-checking [7]. Both unfounded sets and loop formulas rely heavily on syntactic
dependencies between atoms: One cannot generate a set of loop formulas for a program without
knowing its structure and an atom is not deemed unfounded unless it is known to be underivable.
The semantics of the well-known ASP solver, Clingo [9], is defined in terms of loop formulas
and in terms of unfounded sets. Due to the complexity of model checking, there is an intractable
number of loop formulas; Because static dependencies between atoms are easy to establish,
this complexity can be handled lazily [10]. Unlike ASP, its ontology-free counterpart, hybrid
MKNF knowledge bases do not lend themselves well to dependency graph generation. If a
knowledge base’s ontology is left unrestricted, generating a static dependency graph for a hybrid
MKNF knowledge base would require testing the ontology’s entailment relation for all subsets
of atoms. In the remainder of this paper, we describe a framework that establishes dependencies
between atoms through fixpoint operators and thus does not require static dependency analysis.


3. Preliminaries
Minimal knowledge and negation as failure (MKNF)[11] is an extension of first-order logic
that adds two modal operators, K and not , for minimal knowledge and negation as failure
respectively. An MKNF structure is a triple (𝐼, 𝑀, 𝑁 ) where 𝐼 is a first-order interpretation
and 𝑀 and 𝑁 are sets of first-order interpretations. The satisfiability relation under an MKNF
structure is defined as:

    • (𝐼, 𝑀, 𝑁 ) |= 𝐴 if 𝐴 is true in 𝐼 where 𝐴 is a first-order atom
    • (𝐼, 𝑀, 𝑁 ) |= ¬𝐹 if (𝐼, 𝑀, 𝑁 ) ̸|= 𝐹
    • (𝐼, 𝑀, 𝑁 ) |= 𝐹 ∧ 𝐺 if (𝐼, 𝑀, 𝑁 ) |= 𝐹 and (𝐼, 𝑀, 𝑁 ) |= 𝐺
    • (𝐼, 𝑀, 𝑁 ) |= K 𝐹 if (𝐽, 𝑀, 𝑁 ) |= 𝐹 for each 𝐽 ∈ 𝑀
    • (𝐼, 𝑀, 𝑁 ) |= not 𝐹 if (𝐽, 𝑀, 𝑁 ) ̸|= 𝐹 for some 𝐽 ∈ 𝑁

Other symbols such as ∨, and ⊃ are interpreted in MKNF as they are in first-order logic.
   An MKNF interpretation 𝑀 is a set of first-order interpretations (“possible worlds”) and we
say that 𝑀 satisfies a formula 𝐹 , written 𝑀 |=𝑀 𝐾𝑁 𝐹 𝐹 , if (𝐼, 𝑀, 𝑀 ) |= 𝐹 for each 𝐼 ∈ 𝑀 .
An MKNF model 𝑀 of a formula 𝐹 is an MKNF interpretation such that 𝑀 |=𝑀 𝐾𝑁 𝐹 𝐹 and
there does not exist an MKNF interpretation 𝑀 ′ ⊃ 𝑀 such that (𝐼, 𝑀 ′ , 𝑀 ) |= 𝐹 for each
𝐼 ∈ 𝑀 ′ . Following Motik and Rosati [4], a hybrid MKNF knowledge base 𝒦 = (𝒪, 𝒫) consists
of a decidable description logic knowledge base 𝒪 (typically called an ontology) which is
translatable to first-order logic and a set of MKNF rules 𝒫. We denote this translation as 𝜋(𝒪)
and rules in 𝒫 are of the form:

                  K 𝑎1 , . . . , K 𝑎𝑘 ← K 𝑎𝑘+1 , . . . , K 𝑎𝑚 , not 𝑎𝑚+1 , . . . , not 𝑎𝑛        (1)

In the above, 𝑎1 , . . . , 𝑎𝑛 are function-free first-order atoms. Given a rule 𝑟 ∈ 𝒫, we define the
following abbreviations:

                                head(𝑟) = {K 𝑎1 , . . . , K 𝑎𝑘 },
                             𝑏𝑜𝑑𝑦 + (𝑟) = {K 𝑎𝑘+1 , . . . , K 𝑎𝑚 },
                             𝑏𝑜𝑑𝑦 − (𝑟) = {not 𝑎𝑚+1 , . . . , not 𝑎𝑛 },
                        K (𝑏𝑜𝑑𝑦 − (𝑟)) = {K 𝑎 | not 𝑎 ∈ 𝑏𝑜𝑑𝑦 − (𝑟)}, and
                               body(𝑟) = (𝑏𝑜𝑑𝑦 + (𝑟), K (𝑏𝑜𝑑𝑦 − (𝑟)))

  Let 𝜋(𝒫) denote rule set 𝒫’s corresponding MKNF formula:
                                ⋀︁
                       𝜋(𝒫) =       𝜋(𝑟), where
                                    𝑟∈𝒫
                                      𝑘
                                     ⋁︁             𝑚
                                                    ⋀︁                𝑛
                                                                     ⋀︁
                           𝜋(𝑟) =         K 𝑎𝑖 ⊂           K 𝑎𝑖 ∧           not 𝑎𝑖
                                    𝑖=1            𝑖=𝑘+1            𝑖=𝑚+1

   The semantics of a hybrid MKNF knowledge base 𝒦 is obtained by applying both transfor-
mations to 𝒪 and 𝒫 and placing 𝒪 within a K operator, i.e. 𝜋(𝒦) = 𝜋(𝒫) ∧ K 𝜋(𝒪). We use
𝒫, 𝒪, and 𝒦 in place of 𝜋(𝒫), 𝜋(𝒪), and 𝜋(𝒦) respectively when it is clear from context that
the respective translated variant is intended. We refer to formulas of the form K 𝑎 and not 𝑎 as
K-atoms and Not-atoms respectively. When it is clear from context, we may write a bare atom
𝑎 in place of a K-atom K 𝑎. Throughout this work, we assume that MKNF formulas are ground,
i.e., they contain no variables.
   We now outline some definitions and conventions. For a hybrid MKNF knowledge base
𝒦 = (𝒪, 𝒫), we denote the set of all modal atoms found within 𝒫 as KA(𝒦) where KA(𝒦) is
defined as follows.

        KA(𝒦) = {K 𝑎 | either K 𝑎 or not 𝑎 occurs in the head or body of a rule in 𝒫}
The objective knowledge of a hybrid MKNF knowledge base 𝒦 w.r.t. a set of K-atoms 𝑆 ⊆ KA(𝒦)
is the set of first-order formulas {𝜋(𝒪)} ∪ {𝑎 | K 𝑎 ∈ 𝑆}. We denote this set as OB𝒪,S .
   A (partial) partition of KA(𝒦) is a disjoint pair of subsets of KA(𝒦). We usually denote a
partition as (𝑇, 𝐹 ). K-atoms in 𝑇 are said to be true and K-atoms in 𝐹 are said to be false.
A partition is total if 𝑇 ∪ 𝐹 = KA(𝒦). We frequently treat (𝑇, 𝐹 ) as an interpretation that
contains only K-atoms. A dependable partition is a partial partition (𝑇, 𝐹 ) with the additional
restriction that OB𝒪,T ∪ {¬𝑏} is consistent for each K 𝑏 ∈ 𝐹 or OB𝒪,T is consistent if 𝐹 is
empty. A partial partition that is not dependable may not be extended to an MKNF model. A
rule body is applicable w.r.t. a partition (𝑇, 𝐹 ) if body(𝑟) ⊑ (𝑇, 𝐹 ), i.e., if 𝑏𝑜𝑑𝑦 + (𝑟) ⊆ 𝑇 and
K (𝑏𝑜𝑑𝑦 − (𝑟)) ⊆ 𝐹 . We say that an MKNF interpretation 𝑀 of 𝒦 induces a partition (𝑇, 𝐹 ) if
                           ⋀︁                        ⋀︁
                              𝑀 |=𝑀 𝐾𝑁 𝐹 K 𝑎 ∧           𝑀 |=𝑀 𝐾𝑁 𝐹 ¬K 𝑎                          (2)
                         K 𝑎∈𝑇                        K 𝑎∈𝐹

Note that the partition (𝑇 * , 𝐹 * ) induced by an MKNF model 𝑀 is unique and dependable. For
a partition (𝑇, 𝐹 ) that is a subset of this (𝑇 * , 𝐹 * ), i.e., (𝑇, 𝐹 ) ⊑ (𝑇 * , 𝐹 * ), we say that (𝑇, 𝐹 )
can be extended to an MKNF model; such a partition is also dependable.


4. Headcut Semantics
In this section, we formulate a framework that relies on fixpoint operators to represent
MKNF models. First consider the MKNF knowledge base 𝒦 = (𝒪, 𝒫) where 𝜋(𝒪) = {(𝑎∨𝑏) ⊃
𝑐} and 𝒫 only contains the rule K 𝑎, K 𝑏 ← not 𝑐. This knowledge base has no MKNF models.
Intuitively, we can verify that 𝒦 does not have an MKNF model by recognizing that there is no
rule to derive K 𝑐 and thus some K-atom in the head of this rule must be true in an MKNF model
of 𝒦. With either K 𝑎 or K 𝑏 true, an inconsistency is created if K 𝑐 is false.
   We generalize and formally express these intuitive semantics by considering head-cuts of 𝒫.
We define a head-cut 𝑅 of 𝒦 to be a set 𝑅 ⊆ 𝒫 × KA(𝒦) where each rule 𝑟 ∈ 𝒫 occurs in no
more than one pair (𝑟, ℎ) ∈ 𝑅 and K ℎ ∈ head(𝑟). For example, the program 𝒫 = {K 𝑎, K 𝑏 ←},
𝒫 has exactly two head-cuts, {(𝑟, 𝑎)} and {(𝑟, 𝑏)} where 𝑟 refers to the only rule in 𝒫 (Note
that we omit “K ” when describing head-cuts). Given a head-cut 𝑅, we use head(𝑅) and rule(𝑅)
to denote the sets {ℎ | (𝑟, ℎ) ∈ 𝑅} and {𝑟 | (𝑟, ℎ) ∈ 𝑅} respectively.
                                                                   (𝑇,𝐹 )
Definition 4.1. For a total partition (𝑇, 𝐹 ), we define 𝐻𝒦 to be the set containing every
head-cut 𝑅 of 𝒦 such that head(𝑅) ⊆ 𝑇 and for each rule 𝑟 ∈ 𝒫, 𝑟 ∈ rule(𝑅) if and only if
body(𝑟) ⊑ (𝑇, 𝐹 ).
                                            (𝑇,𝐹 )
  Intuitively, there is a head-cut in 𝐻𝒦      for each way of selecting a single head-atom for
                                         (𝑇,𝐹 )
every satisfied rule in 𝒫. In essence, 𝐻𝒦 , gives us a way to avoid dealing with negation
or disjunction. We use this set to show atoms are justified by defining a family of operators
induced by a head-cut 𝑅:

            𝑄𝑅 (𝑋) ={K ℎ | where (𝑟, ℎ) ∈ 𝑅 and 𝑏𝑜𝑑𝑦 + (𝑟) ⊆ 𝑋 for each 𝑟 ∈ 𝒫 }
                      ∪{K 𝑎 ∈ KA(𝒦) | OB𝒪,X |= 𝑎}
We denote the least fixpoint of an operator 𝑄𝑅 as lfp 𝑄𝑅 and use 𝑄𝑅        𝑖 to denote applying the
𝑄 operator 𝑖 times on the empty set (e.g., 𝑄2 = 𝑄 (𝑄 (∅))). This operator simply takes a
  𝑅                                             𝑅       𝑅     𝑅

set of K-atoms 𝑋 and extends it with immediate consequences under 𝑅.
   Revisiting the initial example where 𝒦 = (𝒪, 𝒫), 𝜋(𝒪) = {(𝑎 ∨ 𝑏) ⊃ 𝑐}, and 𝒫 =
{K 𝑎, K 𝑏 ← not 𝑐}, consider any total dependable partition (𝑇, 𝐹 ) where K 𝑐 ∈ 𝐹 . Ob-
                                       (𝑇,𝐹 )
serve that for each head-cut 𝑅 ∈ 𝐻𝒦 , we have 𝑐 ∈ lfp 𝑄𝑅 . For example, let (𝑇, 𝐹 ) =
                                              (𝑇,𝐹 )
({K 𝑎}, {K 𝑐, K 𝑏}). Every head-cut 𝑅 in 𝐻𝒦          contains the rule from 𝒫, thus the 𝑄𝑅 op-
erator will compute either 𝑎 or 𝑏 on the first iteration and then 𝑐 on the second iteration.
Conversely, if we consider a dependable partition (𝑇, 𝐹 ) such that K 𝑐 ∈ 𝑇 , then for each
                  (𝑇,𝐹 )
head-cut 𝑅 ∈ 𝐻𝒦 , we have 𝑐 ̸∈ lfp 𝑄𝑅 . For example, let (𝑇, 𝐹 ) = ({K 𝑎, K 𝑐}, {K 𝑏}).
                                                  (𝑇,𝐹 )
No rule in 𝒫 is applicable w.r.t. (𝑇, 𝐹 ), thus 𝐻𝒦       contains a single head-cut, ∅. We have
𝑄0 = 𝑄1 = ∅, thus 𝑐 ̸∈ lfp 𝑄 .
  ∅     ∅                     𝑅
                                                  (𝑇,𝐹 )
   We now formally show that sets of the form 𝐻𝒦         coincide with an MKNF models of hybrid
                                                      (𝑇,𝐹 )
knowledge bases. First, we connect family of sets 𝐻𝒦         to total partitions that satisfy all rules
in 𝒫 but are not necessarily induced by an MKNF model.
                                                         (𝑇,𝐹 )
Lemma 4.1. For a total partition (𝑇, 𝐹 ), the set 𝐻𝒦 is empty if and only if there exists a rule
𝑟 ∈ 𝒫 where body(𝑟) ⊑ (𝑇, 𝐹 ) and head(𝑟) ∩ 𝑇 = ∅.

Definition 4.2. A set of head-cuts 𝐻 is a supporting set for a total dependable partition (𝑇, 𝐹 )
if: An MKNF model 𝑀 of 𝒦 that induces (𝑇, 𝐹 ) exists if and only if 𝐻 is nonempty and for each
𝑅 ∈ 𝐻 the set computed by lfp 𝑄𝑅 is precisely 𝑇 .

                               (𝑇,𝐹 )
Proposition 4.1. The set 𝐻𝒦             is a supporting set of the dependable partition (𝑇, 𝐹 ).
                                                                     (𝑇,𝐹 )
  In the following example, we demonstrate how the set 𝐻𝒦                     can be used to verify that a
partition can be extended to a model.

Example 1. Let 𝒦 = (∅, 𝒫) where 𝒫 is defined as

                       1 : K 𝑎, K 𝑏 ← K 𝑐                          2 : K 𝑏, K 𝑐 ←

                                                                  (𝑇,𝐹 )
Let (𝑇, 𝐹 ) = ({K 𝑏, K 𝑐}, {K 𝑎}). By definition, the set 𝐻𝒦    contains two head-cuts: 𝑅0 =
{(1, 𝑏), (2, 𝑏)} and 𝑅1 = {(1, 𝑏), (2, 𝑐)}. When we repeatedly apply the 𝑄 operator on each of
these head-cuts we obtain the following sets.

           𝑄𝑅
            0 =∅
             0
                               𝑄𝑅
                                1 = {𝑏}
                                  0
                                                        𝑄𝑅0   𝑅0
                                                         2 = 𝑄1                    𝑄𝑅0   𝑅0
                                                                                    3 = 𝑄1
           𝑄𝑅
            0 =∅
             1
                               𝑄𝑅
                                1 = {𝑐}
                                  1
                                                        𝑄𝑅
                                                         2 = {𝑏, 𝑐}
                                                          1
                                                                                   𝑄𝑅 1  𝑅1
                                                                                    3 = 𝑄2

   Using Proposition 4.1, it is easy to confirm that (𝑇, 𝐹 ) = ({K 𝑎, K 𝑏, K 𝑐}, ∅) can not be extended
to a model of 𝒦 by observing that neither lfp 𝑄𝑅0 nor 𝑄𝑅1 computes 𝑇 . If we instead use (𝑇, 𝐹 ) =
                                        (𝑇,𝐹 )
({K 𝑎, K 𝑐}, {K 𝑏}), then the set 𝐻𝒦           contains the just a single head-cut, 𝑅0 = {(1, 𝑎), (2, 𝑐)}.
We have lfp 𝑄𝑅0 = 𝑇 , thus (𝑇, 𝐹 ) can be extended to an MKNF model.
    Now that we have established a semantics in terms of a family of fixpoint operators, we
                                                          (𝑇,𝐹 )
discuss some optimizations that, when applied to 𝐻𝒦 , greatly reduce the number of head-
cuts in the set. This is a crucial step that enables the set to be used in a solver. For a dependable
                                                                                              (𝑇,𝐹 )
partition (𝑇, 𝐹 ), that cannot be extended to a model, there are many head-cuts in 𝐻𝒦                that
contain rules whose bodies are never satisfied by iterative construction or do not derive anything
new. Our first optimization step is to remove such rules from head-cuts by defining a new
          (𝑇,𝐹 )             (𝑇,𝐹 )                           (𝑇,𝐹 )
set 𝐻𝑀𝒦           based on 𝐻𝒦 . A head-cut 𝑅 is in 𝐻𝑀𝒦               if and only if there is a head-cut
         (𝑇,𝐹 )
  ′
𝑅 ∈ 𝐻𝒦           such that 𝑅 = 𝑅 ∖ 𝑅𝑀 , where
                                   ′


                    𝑅𝑀 = {(𝑟, ℎ) ∈ 𝑅 | ∀𝑖, body(𝑟) ⊆ 𝑄𝑅               𝑅
                                                      𝑖 =⇒ head(𝑟) ⊆ 𝑄𝑖 }

                                                                   (𝑇,𝐹 )                          (𝑇,𝐹 )
 This set removes some pairs in each head-cut from 𝐻𝒦 . For each head-cut 𝑅 ∈ 𝐻𝑀𝒦
                                 (𝑇,𝐹 )
there is some head-cut 𝑅′ ∈ 𝐻𝒦          for which 𝑅 ⊆ 𝑅′ . However, 𝑅′ is not unique in general.
             (𝑇,𝐹 )
The set 𝐻𝑀𝒦         also has the convenient property of only including pairs that contribute to
the computation of 𝑄𝑅 , thus head(𝑅) ⊆ lfp 𝑄𝑅 .
                                                               (𝑇,𝐹 )
   In the example following example, we demonstrate that 𝐻𝑀𝒦          can be used as a supporting
set.

Example 2. Let 𝒦 = (∅, 𝒫) where 𝒫 contains the following rules

                                0:                                K 𝑎, K 𝑏 ←
                                1:                                       K𝑐 ← K𝑎
                                2:                                       K𝑐 ← K𝑏
                                3:                                K 𝑎, K 𝑑 ← K 𝑐

Let (𝑇, 𝐹 ) = (KA(𝒦), ∅) and 𝑅 = {(0, 𝑎), (1, 𝑐), (3, 𝑑)}. 𝑄𝑅    1 computes “𝑎” via rule 0, then 𝑄2
                                                                                                    𝑅
                                                     𝑅
computes “𝑐” via rule 2. On the third iteration, 𝑄3 computes “𝑑” via rule 3, however, we already
                                            (𝑇,𝐹 )
have head(3) ⊆ 𝑄𝑅 2 , thus 𝑅 is not in 𝐻𝑀𝒦         . Instead, the head-cut 𝑅 = {(0, 𝑎), (1, 𝑐)} is in
     (𝑇,𝐹 )
𝐻𝑀𝒦 .
          (𝑇,𝐹 )                   (𝑇,𝐹 )
  Like 𝐻𝒦          , the set 𝐻𝑀𝒦            is a supporting set of (𝑇, 𝐹 ).
                              (𝑇,𝐹 )
Proposition 4.2. 𝐻𝑀𝒦                   is a supporting set of (𝑇, 𝐹 ).

   We define more optimizations that further reduce the number of head-cuts that need to be
tested to verify a model. A head-cut 𝑅 is branch-minimal w.r.t. a set of head-cuts 𝑆 if for each
𝑅′ ∈ 𝑆 such that head(𝑅) ⊆ head(𝑅′ ) or head(𝑅′ ) ⊆ head(𝑅), we have head(𝑅) ⊆ head(𝑅′ ).
It can be easily shown that this relation is a partial order between head-cuts.
                                                  (𝑇,𝐹 )
   We formulate a further optimization of 𝐻𝑀𝒦            based on this notion of minimality.
                     (𝑇,𝐹 )                    (𝑇,𝐹 )                                 (𝑇,𝐹 )
              𝐻𝑃𝒦             = {𝑅 ∈ 𝐻𝑀𝒦                | 𝑅 is branch-minimal w.r.t. 𝐻𝑀𝒦       }
                         (𝑇,𝐹 )
Proposition 4.3. 𝐻𝑃𝒦              is a supporting set of (𝑇, 𝐹 ).
                (𝑇,𝐹 )
  The set 𝐻𝑃𝒦       is not practical for use in solver: Because of the complexity of determining
whether a head-cut is branch-minimal, the set cannot be efficiently enumerated. We develop a
                                              (𝑇,𝐹 )
supporting set that is a compromise of 𝐻𝑃𝒦           .
  Given a head-cut 𝑅, we define 𝑅[𝑖] to be the subset of 𝑅 that contains only the rules in
rule(𝑅) whose bodies are satisfied after 𝑖 iterations of the 𝑄𝑅 operator, that is,

                         𝑅[𝑖] = {(𝑟, ℎ) ∈ 𝑅 | ℎ ̸∈ 𝑄𝑅       +       𝑅
                                                    𝑖 , 𝑏𝑜𝑑𝑦 (𝑟) ⊆ 𝑄𝑖 }

Intuitively, 𝑅[𝑖] contains the atoms newly derived on iteration 𝑖. Likewise, we define a range
𝑅[0..𝑗] where 0 ≤ 𝑗
                                                 𝑗
                                                ⋃︁
                                      𝑅[0..𝑗] =    𝑅[𝑘]
                                                        𝑘=0

  A head-cut 𝑅 is semi-branch-minimal w.r.t. a head-cut 𝑅′ if for the largest 𝑖 such that

                                      𝑅[0..(𝑖 − 1)] = 𝑅′ [0..(𝑖 − 1)]

we have head(𝑅[𝑖]) ⊆ head(𝑅′ [𝑖]).
               (𝑇,𝐹 )
  We define 𝐻𝐺𝒦       to be the set
    (𝑇,𝐹 )               (𝑇,𝐹 )                                                                          (𝑇,𝐹 )
𝐻𝐺𝒦          = {𝑅 ∈ 𝐻𝑀𝒦           | 𝑅 is semi-branch-minimal w.r.t. every other head-cut 𝑅′ ∈ 𝐻𝑀𝒦                 }

                                                        (𝑇,𝐹 )                    (𝑇,𝐹 )
  We give an example of a head-cut from 𝐻𝑀𝒦                      that is also in 𝐻𝐺𝒦

Example 3. Let 𝒦 = (𝒪, 𝒫) where 𝒪 = ∅ and

                                             1 :K 𝑎, K 𝑏 ← K 𝑐
                                             2 :K 𝑎, K 𝑏 ← K 𝑐
                                             3 :K 𝑐 ←

Let (𝑇, 𝐹 ) = (KA(𝒦), ∅). Define the following head-cuts:

                                       𝑅0 = {(1, 𝑎), (2, 𝑎), (3, 𝑐)},
                                       𝑅1 = {(1, 𝑎), (2, 𝑏), (3, 𝑐)},
                                       𝑅2 = {(1, 𝑏), (2, 𝑎), (3, 𝑐)},
                                       𝑅3 = {(1, 𝑏), (2, 𝑏), (3, 𝑐)}

               (𝑇,𝐹 )
We have 𝐻𝑀𝒦         = {𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 }. For each pair of head-cuts 𝑅𝑖 and 𝑅𝑗 , we have 𝑅𝑖 [0..1] =
𝑅𝑗 [0..1]. However, we have head(𝑅0 [2]) ⊂ head(𝑅1 [2]) and head(𝑅0 [2]) ⊂ head(𝑅2 [2]), thus
                                                                  (𝑇,𝐹 )
neither 𝑅1 nor 𝑅2 is semi-branch-minimal. This gives us 𝐻𝐺𝒦              = {𝑅0 , 𝑅2 }.
                     (𝑇,𝐹 )         (𝑇,𝐹 )                          (𝑇,𝐹 )
   Both the sets 𝐻𝑃𝒦       and 𝐻𝐺𝒦       are subsets of 𝐻𝑀𝒦 , however, in general, neither
                                            (𝑇,𝐹 )                               (𝑇,𝐹 )
set is a subset of the other. The set 𝐻𝐺𝒦          is easier to enumerate than 𝐻𝑃𝒦        because
                                                                                (𝑇,𝐹 )
head-cuts can be constructed iteratively whereas to enumerate head-cuts in 𝐻𝑃𝒦         , one must
                                     (𝑇,𝐹 )                                                  (𝑇,𝐹 )
test whether each head-cut in 𝐻𝑀𝒦            is branch-minimal. We demonstrate how 𝐻𝐺𝒦
may be iterated later on when we construct an abstract solver.

Example 4. Let 𝒦 = (𝒪, 𝒫) such that 𝒪 = ∅ and

               𝒫 = {1 : K 𝑎, K 𝑏, K 𝑐, K 𝑑 ←; 2 : K 𝑎, K 𝑏, K 𝑑 ←;
                      K 𝑐 ← 𝑎; K 𝑐 ← 𝑏; K 𝑎 ← 𝑏; K 𝑏 ← 𝑎; K 𝑎 ← 𝑑; K 𝑏 ← 𝑑; }
                                                                                              (𝑇,𝐹 )
We use the total partition (𝑇, 𝐹 ) = (KA(𝒦), ∅) to consider various head-cuts in the sets 𝐻𝐺𝒦
        (𝑇,𝐹 )
and 𝐻𝑃𝒦        . For brevity, we omit pairs in head-cuts that contain normal rules. First, we give a
                           (𝑇,𝐹 )             (𝑇,𝐹 )
head-cut 𝑅 found in 𝐻𝐺𝒦           but not 𝐻𝑃𝒦        .

                                             𝑅 = {(1, 𝑑), (2, 𝑑)}
                                        𝑄𝑅
                                         1 = {𝑑}
                                    lfp 𝑄𝑅 = {𝑎, 𝑏, 𝑐, 𝑑}
                                                                     (𝑇,𝐹 )
   𝑅 is semi-branch-minimal w.r.t. every head-cut from 𝐻𝑀𝒦             because head(𝑅) contains a
                                      ′        (𝑇,𝐹 )                 ′
single atom and there is no head-cut 𝑅 in 𝐻𝑀𝒦         such that head(𝑅 ) = ∅. However, the selection
of 𝑑 in 𝑅 results in the atoms 𝑎, 𝑏, and 𝑐, also being derived; For the head 𝑅′ = {(1, 𝑎), (2, 𝑎)},
        ′                                                                                (𝑇,𝐹 )
lfp 𝑄𝑅 = {𝑎, 𝑏, 𝑐}, thus 𝑅 is not branch-minimal. We give a head-cut 𝑅 that is in 𝐻𝑃𝒦           and
          (𝑇,𝐹 )
not 𝐻𝐺𝒦 :

                                             𝑅 = {(1, 𝑐), (2, 𝑏)}
                                        𝑄𝑅
                                         1 = {𝑏, 𝑐}
                                    lfp 𝑄𝑅 = {𝑎, 𝑏, 𝑐}
                                                         (𝑇,𝐹 )
𝑅 is branch-minimal because every head-cut in 𝐻𝑀𝒦           computes at least 𝑎, 𝑏, and 𝑐, however,
                                                                            (𝑇,𝐹 )
𝑅 is not semi-branch-minimal because 𝑐 ∈ head(𝑅); A head-cut 𝑅 in 𝐻𝐺𝒦              cannot contain a
pair with 𝑐 in it because there is always a head-cut 𝑅′ that is semi-branch-minimal w.r.t. 𝑅.
                                                                        (𝑇,𝐹 )         (𝑇,𝐹 )
  We give an exhaustive account of the head-cuts that are in both 𝐻𝐺𝒦          and 𝐻𝑃𝒦        :


                                        𝑅0 = {(1, 𝑎), (2, 𝑎)}
                                        𝑅1 = {(1, 𝑏), (2, 𝑏)}
                                  lfp 𝑄𝑅0 = lfp 𝑄𝑅1 = {𝑎, 𝑏}
                                                (𝑇,𝐹 )
As mentioned above, no head-cut 𝑅 in 𝐻𝑃𝒦      can have 𝑑 ∈ head(𝑅) and no head-cut 𝑅 in
   (𝑇,𝐹 )                                              (𝑇,𝐹 )     (𝑇,𝐹 )
𝐻𝐺𝒦       can have 𝑐 ∈ head(𝑅), thus no head-cut in 𝐻𝐺𝒦       ∩ 𝐻𝑃𝒦      can contain either
                                                                                (𝑇,𝐹 )                            (𝑇,𝐹 )
atom. Finally, we give an example of a head-cut in 𝐻𝑀𝒦                                   that is neither in 𝐻𝑀𝒦            nor
    (𝑇,𝐹 )
𝐻𝐺𝒦 :
                                                      𝑅 = {(1, 𝑎), (2, 𝑑)}
                                                  𝑄𝑅
                                                   1 = {𝑎, 𝑑}
                                              lfp 𝑄𝑅 = {𝑎, 𝑏, 𝑐, 𝑑}
The head-cut demonstrated above is neither branch-minimal nor semi-branch-minimal.
                      (𝑇,𝐹 )                 (𝑇,𝐹 )
   Even though 𝐻𝑃𝒦           and 𝐻𝐺𝒦        are disjoint, they are related in a crucial way that allows
                       (𝑇,𝐹 )                                                                (𝑇,𝐹 )
us to show that 𝐻𝐺𝒦           is a supporting set. Intuitively, a head-cut 𝑅 from 𝐻𝑃𝒦               can be
thought of as having a minimal set head(𝑅) that is globally minimal w.r.t. iterations of 𝑄𝑅               𝑖
                                     (𝑇,𝐹 )
whereas a head-cut 𝑅 from 𝐻𝑀𝒦 ’s set head(𝑅) is only locally minimal w.r.t. an iteration of
                           (𝑇,𝐹 )                                                      (𝑇,𝐹 )
𝑄𝑅𝑖 . As it turns out, 𝐻𝑃𝒦        is more precise and if there is a head-cut in 𝐻𝑃𝒦           that fails to
                                                                        (𝑇,𝐹 )
compute 𝑇 , we can guarantee that such a head-cut exists in 𝐻𝐺𝒦                as well. We demonstrate
this property formally.
                                                                       (𝑇,𝐹 )
Lemma 4.2. If there exists a head-cut in 𝑅 ∈ 𝐻𝑃𝒦       such that lfp 𝑄𝑅 ⊂ 𝑇 , then there is a
                (𝑇,𝐹 )        (𝑇,𝐹 )                 ′
head-cut 𝑅′ ∈ 𝐻𝑃𝒦      ∩ 𝐻𝐺𝒦         such that lfp 𝑄𝑅 ⊂ 𝑇
                                                                                                   (𝑇,𝐹 )
   Finally, we can use the property demonstrated above to show that 𝐻𝐺𝒦                                     is a supporting
set of (𝑇, 𝐹 ).
                         (𝑇,𝐹 )
Proposition 4.4. 𝐻𝐺𝒦              is a supporting set of (𝑇, 𝐹 ).


5. An Abstract Solver
Up until now, we have dealt exclusively with total partitions. We now discuss how the techniques
described in the previous section can be applied to partial partitions and in turn be used to
develop an abstract solver.
  We define the set 𝐷𝒦𝑅 under a head-cut 𝑅.

                               (𝑇 * ,𝐹 * )
                𝑅
               𝐷𝒦 = {𝐻𝐺𝒦                     | where 𝑅 = 𝑅* [0..𝑖]
                                                         (𝑇 * ,𝐹 * )
                    for some 𝑖 and 𝑅* ∈ 𝐻𝐺𝒦                            and total partition (𝑇 * , 𝐹 * )}
  Given a head-cut 𝑅, we can extract an appropriate partition from 𝑅:
                                         ⋃︁
                      𝒮(𝑅) = (lfp 𝑄𝑅 , {𝑏𝑜𝑑𝑦 − (𝑟) | (𝑟, ℎ) ∈ 𝑅})
                          (𝑇 * ,𝐹 * )
Note that for each 𝐻𝐺𝒦            ∈ 𝐷𝒦 𝑅 , we have 𝒮(𝑅) ⊑ (𝑇 * , 𝐹 * ). Intuitively, the set 𝐷 𝑅 holds
                                                                                              𝒦
                            *  *
                          (𝑇 ,𝐹 )
every possible set 𝐻𝐺𝒦            if 𝒮(𝑅) were extended to a total partition (𝑇 * , 𝐹 * ). Note that
(𝑇 * , 𝐹 * ) may not be dependable. We also define a total variant of 𝒮(𝑅):
                                  𝒮 * (𝑅) = (lfp 𝑄𝑅 , KA(𝒦) ∖ lfp 𝑄𝑅 )
We recursively define a subclass of head-cuts to limit the use of 𝐷𝒦
                                                                   𝑅.
Definition 5.1. Given, a head-cut 𝑅 where 𝒮(𝑅) is a dependable partition, we call 𝑅 a head-
                                                             ′                      ′
     ⋃︀ if𝑅′either 𝑅 = ∅ or there is another head-cut state 𝑅 such that either 𝑅 = 𝑅 [0..𝑖] or
cut state
𝑅 ∈ 𝐷𝒦 .

   Intuitively, a head-cut state is a head-cut that can be extended to some a head-cut in 𝑅 ∈ 𝐻
for every 𝐻 ∈ 𝐷𝒦   𝑅 . Note that 𝒮(𝑅) ⊑ 𝒮 * (𝑅) for a head-cut state 𝑅.

   We now define an abstract solver that operates on head-cut states. Supporting can assist a
solver in several key ways: Conflict propagation and immediate propagation that adds positive
direct consequences to a head-cut state 𝑅 (See 𝑇 (𝑅) in Algorithm 1), Guiding solver decisions
at points where the current head-cut state cannot be extended through means of well-founded
propagation (See 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) in Algorithm 2) and as already shown, supporting sets can
be used for model verification. We join these roles together in an abstract solver outlined in
Algorithm 3. Finally, we show how supporting sets can be used to reason about head-cut states
that can be verified in polynomial time (similar to head-cycle free). We leave certain details
unspecified such as how to enumerate the set 𝐷𝒦     𝑅 in an efficient way in the context of each of

the algorithms and the overall complexity of the algorithms we provide.
 Algorithm 1: 𝑇 (𝑅)
1 (𝑇, 𝐹 ) ← 𝒮(𝑅);
2 𝐵 ← {𝑅′ [𝑖 + 1] | 𝑅′ ∈
                         ⋃︀ 𝑅 ′
                           𝐷𝒦 , 𝑅 [0..𝑖] = 𝑅};
                 ⋂︀
3 if ∃(𝑟, ℎ) ∈        𝐵, |head(𝑟) ∖ 𝐹 | =
                                        ̸ 1 or body(𝑟) ̸⊑ (𝑇, 𝐹 ) then
4     return 𝑅;
5 assert |𝐵| ≤ 1;
                 ⋂︀
6 return 𝑅 ∪          𝐵;
  Intuitively, Algorithm 1 adds information to 𝑅 only if there are only rules whose bodies are
satisfied w.r.t. 𝒮(𝑅) and the head of the rule contains no true atoms and only a single atom
that is not false. We demonstrate that a solver cannot miss any models by applying 𝑇 (𝑅) to a
head-cut state.

Lemma 5.1. For a head-cut state 𝑅 and any head-cut 𝑅* ∈ 𝐷𝒦        where 𝑅 = 𝑅* [0..𝑖], we either
                                                           ⋃︀ 𝑅
have 𝑅* [0..(𝑖 + 1)] = 𝑇 (𝑅) or 𝑅 = 𝑇 (𝑅).

   With 𝑇 (𝑅), we only propagate information if it holds in all models that 𝒮(𝑅) can be extended
to. At some point in the solving process, we must add information for which this does not hold.
We describe a process for extending head-cut states with decision atoms.
 Algorithm 2: 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅)
1 𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠 ← ∅;
         ⋃︀ 𝑅
2 if 𝑅 ∈   𝐷𝒦 then
3     return ∅;
4 for 𝑅′ ∈     𝐷𝒦 where ∃𝑖, 𝑅′ [0..𝑖] = 𝑅 do
           ⋃︀ 𝑅
5     if 𝒮(𝑅′ [0..(𝑖 + 1)]) is dependable then
6         𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠 ← 𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠 ∪ {𝑅′ [0..(𝑖 + 1)]};

7 return 𝐷𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠;

  We guarantee very little about the atoms added by 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) and in general, the solver
will be forced to backtrack because of the atoms that were added by this procedure. However,
extensions made by 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛(𝑅) will maintain the property that 𝑅 is a head-cut state. Further-
more, if 𝒮(𝑅) can be extended to an MKNF model of 𝒦, then a head-cut in 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) also
has this property. This ensures that a solver that uses 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) will not miss any models.

Lemma 5.2. Given a head-cut state 𝑅 and an MKNF model 𝑀 that induces 𝒮(𝑅), there is either
a head-cut state 𝑅′ ∈ 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) such that 𝑀 induces 𝒮(𝑅′ ) or 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) is empty.
                                                                                             𝒮 * (𝑅)
   We define check-model(𝑅) to be a procedure that simply enumerates all head-cuts in 𝐻𝐺𝒦
to verify that 𝒮 * (𝑅) can be extended to a model by applying the 𝑄𝑅 until a fixed point is reached.
The correctness of such an algorithm follows directly from Proposition 4.4.
   We now integrate all preceding algorithms into an abstract solver.
 Algorithm 3: 𝑠𝑜𝑙𝑣𝑒𝑟(𝑅)
1 𝑅 ← lfp 𝑇 (𝑅);
2 for 𝑅′ ∈ 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) do
3     if 𝑠𝑜𝑙𝑣𝑒𝑟(𝑅′ ) then
4         return 𝑠𝑜𝑙𝑣𝑒𝑟(𝑅′ );

5 if 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) = ∅ and check-model(𝑅) then
6     return 𝒮 * (𝑅)
7 return 𝑓 𝑎𝑙𝑠𝑒;

  While we do not specify which head-cut from 𝑑𝑒𝑐𝑖𝑠𝑖𝑜𝑛𝑠(𝑅) should be selected to minimize
backtracking, our algorithm can locate a model if one exists.

Lemma 5.3. Given a head-cut state 𝑅, if there exists a model that induces 𝒮(𝑅), then 𝑠𝑜𝑙𝑣𝑒𝑟(𝑅)
will return a total partition induced by a model.

   While more efficient than a guess-and-verify solver, Algorithm 3 does not efficiently verify
total partitions. It is well known that head-cycle free disjunctive logic programs can be solved
in NP [12]. We demonstrate an analogous subclass of disjunctive MKNF knowledge bases that
can be verified in polynomial time.
  First, we identify a property of head-cut states that enables polynomial verification. We show
that this property holds if and only if a head-cut state coincides with an MKNF model.
Definition 5.2. A head-cut state 𝑅 is P-verifiable if the following holds. For every head-cut 𝑅* ∈
                                                                               *
  𝐷𝒦 , where 𝑅* [0..𝑖] = 𝑅[0..𝑖] and 𝑅* [𝑖 + 1] ̸= 𝑅[𝑖 + 1], we have lfp 𝑄𝑅 ⊇ head(𝑅[𝑖 + 1]).
⋃︀ 𝑅


Proposition 5.1. If a head-cut state 𝑅 is P-verifiable and 𝒮 * (𝑅) is dependable, then lfp 𝑄𝑅 = 𝑇
                     ′                         𝒮 * (𝑅)
if and only if lfp 𝑄𝑅 = 𝑇 for each 𝑅′ ∈ 𝐻𝐺𝒦            .
Corollary 5.1. A head-cut state 𝑅 is P-verifiable if and only if 𝒮 * (𝑅) can be extended to an
MKNF model of 𝒦.
  Using the above property, we construct a verification algorithm that is more efficient than
check-model(𝑅).
 Algorithm 4: check-model2 (𝑅)
       𝒮 * (𝑅)
1 if 𝐻𝐺𝒦       = ∅ then
2     return 𝑓 𝑎𝑙𝑠𝑒;
3 for 𝑖 ← 0; 𝑄𝑅          𝑅
                𝑖 ̸= 𝑄𝑖−1 ; 𝑖 ← 𝑖 + 1 do
                     𝒮 * (𝑅)
4     for 𝑅′ ∈ 𝐻𝐺𝒦           where 𝑅[0..𝑖] = 𝑅′ [0..𝑖] and 𝑅[𝑖 + 1] ̸= 𝑅′ [𝑖 + 1] do
                                        ′
5         if head(𝑅[𝑖 + 1]) ̸⊆ lfp 𝑄𝑅 then
6             return 𝑓 𝑎𝑙𝑠𝑒;

7 return 𝑡𝑟𝑢𝑒;

   When check-model(𝑅) is replaced with Algorithm 4 in the solver (Algorithm 3), P-verifiable
head-cut states can be quickly verified. We feel strongly that with further complexity analysis we
will be able conclude that our abstract solver algorithm, when used with an empty ontology and
head-cycle free disjunctive logic program, can verify any enumerated partition in polynomial
time.


6. Conclusion
We have provided a new way of characterizing disjunctive MKNF models through supporting
                                     (𝑇,𝐹 )
sets. The largest set we defined, 𝐻𝒦 , contains many redundant head-cuts and is not practical
                                                       (𝑇,𝐹 )                              (𝑇,𝐹 )
for use in a solver. We defined a smaller set, 𝐻𝑀𝒦 , where each head-cut in 𝐻𝑀𝒦                   is
                                                                                    (𝑇,𝐹 )
limited to rules that contribute to the fixpoint computation. Next we refined 𝐻𝑀𝒦          further
              (𝑇,𝐹 )                                               (𝑇,𝐹 )
to obtain 𝐻𝑃𝒦        and the less precise but more tractable set 𝐻𝐺𝒦 . We provided an abstract
solver that utilizes supporting sets to enumerate partitions and to verify models. Finally, we
characterized P-verifiable head-cut states, a property of head-cut states that is comparable to
head-cycle-free disjunctive logic programs, and we give a more efficient model verification
procedure that leverages this property.
   We speculate that the complexity of our abstract solver algorithm is no worse than a guess-
and-verify solver if the entailment relation of the accompanying ontology can be computed
in polynomial time. We also speculate that if the ontology is empty and 𝒫 is a head-cycle
free disjunctive logic program that the complexity of finding a model lies in 𝑁 𝑃 . However,
we leave a full analysis of the complexity of our algorithm and the complexity of recognizing
P-verifiable head-cut states to future work. In this work, we introduce many new structures
to characterize our semantics; It would be interesting to recast this work using more familiar
fixpoint structures such as approximators in approximation fixpoint theory [13]. In the future,
we would also like to leverage this framework to generate conflicts so that a CDNL-based solver
may be constructed.


References
 [1] M. Gebser, B. Kaufmann, T. Schaub, Advanced conflict-driven disjunctive answer set
     solving, in: Proceedings of the Twenty-Third International Joint Conference on Artificial
     Intelligence, IJCAI ’13, AAAI Press, 2013, p. 912–918.
 [2] T. Eiter, G. Ianni, R. Schindlauer, H. Tompits, A uniform integration of higher-order
     reasoning and external evaluations in answer-set programming., 2005, pp. 90–96.
 [3] M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, P. Wanko, Theory solving
     made easy with clingo 5, in: M. Carro, A. King, N. Saeedloei, M. D. Vos (Eds.), Technical
     Communications of the 32nd International Conference on Logic Programming, ICLP 2016
     TCs, October 16-21, 2016, New York City, USA, volume 52 of OASICS, Schloss Dagstuhl -
     Leibniz-Zentrum für Informatik, 2016, pp. 2:1–2:15.
 [4] B. Motik, R. Rosati, Reconciling description logics and rules, J. ACM 57 (2010) 30:1–30:62.
 [5] N. Leone, P. Rullo, F. Scarcello, Disjunctive stable models: Unfounded sets, fixpoint
     semantics, and computation, Inf. Comput. 135 (1997) 69–112.
 [6] V. Lifschitz, A. A. Razborov, Why are there so many loop formulas?, ACM Trans. Comput.
     Log. 7 (2006) 261–268.
 [7] J. Lee, V. Lifschitz, Loop formulas for disjunctive logic programs, in: C. Palamidessi (Ed.),
     Logic Programming, 19th International Conference, ICLP 2003, Mumbai, India, December
     9-13, 2003, Proceedings, volume 2916 of Lecture Notes in Computer Science, Springer, 2003,
     pp. 451–465.
 [8] T. Eiter, G. Gottlob, On the computational cost of disjunctive logic programming: Proposi-
     tional case, Ann. Math. Artif. Intell. 15 (1995) 289–323.
 [9] M. Gebser, B. Kaufmann, T. Schaub, Conflict-driven answer set solving: From theory to
     practice, Artif. Intell. 187 (2012) 52–89.
[10] C. Drescher, T. Walsh, Answer set solving with lazy nogood generation, in: A. Dovier, V. S.
     Costa (Eds.), Technical Communications of the 28th International Conference on Logic
     Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary, volume 17 of LIPIcs,
     Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 188–200.
[11] V. Lifschitz, Nonmonotonic databases and epistemic queries, in: J. Mylopoulos, R. Reiter
     (Eds.), Proceedings of the 12th International Joint Conference on Artificial Intelligence.
     Sydney, Australia, August 24-30, 1991, Morgan Kaufmann, 1991, pp. 381–386. URL: http:
     //ijcai.org/Proceedings/91-1/Papers/059.pdf.
[12] R. Ben-Eliyahu, R. Dechter, Propositional semantics for disjunctive logic programs, Ann.
     Math. Artif. Intell. 12 (1994) 53–87.
[13] F. Liu, J. You, Alternating fixpoint operator for hybrid MKNF knowledge bases as an
     approximator of AFT, in: P. Fodor, M. Montali, D. Calvanese, D. Roman (Eds.), Rules
     and Reasoning - Third International Joint Conference, RuleML+RR 2019, Bolzano, Italy,
     September 16-19, 2019, Proceedings, volume 11784 of Lecture Notes in Computer Science,
     Springer, 2019, pp. 113–127.