=Paper=
{{Paper
|id=Vol-3799/paper3ASPOCP
|storemode=property
|title=Adapting Approximation Fixpoint Theory to Nondeterministic Hybrid Reasoning
|pdfUrl=https://ceur-ws.org/Vol-3799/paper3ASPOCP.pdf
|volume=Vol-3799
|authors=Spencer Killen,Jia-Huai You
|dblpUrl=https://dblp.org/rec/conf/iclp/KillenY24
}}
==Adapting Approximation Fixpoint Theory to Nondeterministic Hybrid Reasoning==
<pdf width="1500px">https://ceur-ws.org/Vol-3799/paper3ASPOCP.pdf</pdf>
<pre>
                         Adapting Approximation Fixpoint Theory to
                         Nondeterministic Hybrid Reasoning
                         Spencer Killen1 , Jia-Huai You1
                         1
                             University of Alberta, Edmonton, Canada


                                        Abstract
                                        Approximation fixpoint theory (AFT) is an abstract, algebraic framework for the study of operators and their
                                        fixpoints on bilattices. It is based on approximating operators (approximators for short) and has seen application
                                        in expressing semantics for a variety of nonmonotonic languages. The original AFT only treats consistent,
                                        symmetric, and exact approximators. Consequently, it lacks the means to deal with inconsistencies which may
                                        arise naturally in systems of hybrid reasoning. This problem was addressed by a generalization of AFT by Liu
                                        and You [1], which alters the exactness condition so that inconsistencies can be supported. However, neither the
                                        original AFT nor this generalized AFT is capable of expressing nondeterministic semantics, which is essential
                                        for characterizing disjunctive knowledge. The recent proposal of nondeterministic AFT by Heyninck et al. [2]
                                        only deals with consistent and exact approximations, and its definitions of orderings, fixpoints, and monotonicity
                                        deviate from that of the original AFT. Due to differences in these core definitions, it is highly challenging, if
                                        not impossible, to generalize nondeterministic AFT to handle inconsistencies. In this paper, we present a new
                                        framework which relies on a family of approximators in Liu and You’s formulation to express nondeterministic
                                        semantics abstractly and algebraically. As an application, we show how to capture the partial stable semantics of
                                        (disjunctive) hybrid MKNF knowledge bases.

                                        Keywords
                                        approximation fixpoint theory, hybrid MKNF, disjunctive ASP




                         1. Introduction
                         Approximation Fixpoint Theory (AFT) [3] is a powerful framework that leverages pairs of elements
                         (approximations) to construct operators (approximators) that can capture the fixpoints of nonmonotonic
                         operators defined on bilattices and provide characterizations of semantics for nonmonotonic systems.
                         A bilattice is a partially ordered set consisting of a set of pairs (𝑥, 𝑦), where 𝑥 and 𝑦 are elements of
                         a complete lattice and an ordering. In the ideal situation where the value of 𝑥 is less or equal to 𝑦 in
                         the underlying ordering, (𝑥, 𝑦) represents an interval where 𝑥 is a lower bound and 𝑦 an upper bound.
                         In the context of logic, 𝑥 is often used to represent the set of true atoms and 𝑦 the set of possibly true
                         atoms (so that any atom not in 𝑦 is false and atoms that are neither true nor false are undefined). An
                         exact pair (𝑥, 𝑥) can be viewed as a two-valued interpretation.
                            In AFT, we are given the tools of algebra, in terms of operators and the fixpoints built around them,
                         to express stable semantics as well as partial stable semantics, and the main focus while characterizing
                         a semantics is to define an appropriate approximator. Note that in the context of logic programming,
                         partial semantics is often closely related to the simplification of a program during grounding and to
                         constraint propagation in search; namely, in these processes, we are interested in which atoms we can
                         infer to be true or false towards the goal of constructing two-valued stable solutions. AFT’s generality
                         and ease of use has made it a popular approach for a variety of applications (e.g. [4, 5, 6, 7, 8, 9]).
                            However, AFT requires operators to be deterministic and exact. It is incapable of expressing nonde-
                         terministic semantics and dealing with inconsistencies in general, which are required for capturing
                         disjunctive knowledge and dealing with classical hybrid reasoning, respectively. An exact approximator
                         must map an exact pair to an exact pair. In the context of logic programming, this is to say that, given a
                         two-valued interpretation, a logic program must map it to a two-valued interpretation. This requirement
                         is too strict for hybrid reasoning, where different reasoning components together may lead to a conflict,


                          ASPOCP 2024: 17𝑡ℎ Workshop on Answer Set Programming and Other Computing Paradigms, October, 2024, Dallas, USA.
                                       © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).


CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
which shall be represented by a pair (𝑥, 𝑦) where 𝑥 is not a “lower value" than that of 𝑦. In general, a
hybrid knowledge base may even map a partial interpretation to an inconsistent one.
   This paper shows how to adapt AFT to capture nondeterministic semantics. This results in an
extension of the current development of AFT. That is, we propose a new abstract, algebraic framework
to represent and characterize nondeterministic semantics relying only on the notations and definitions
of the current AFT. To accommodate inconsistencies, we lift the notion of conditional stable fixpoints
from Liu and You [1]’s generalized AFT to a nondeterministic setting. As a demonstration, we instantiate
our extension to apply it to hybrid MKNF (Minimal Knowledge and Negation as Failure) [10].
   The unique challenges of capturing disjunctive hybrid MKNF are twofold: inconsistencies may
arise from the ontology and disjunctive rules and require nondeterministic treatment. While AFT has
recently been extended to nondeterministic operators [2], this framework is ill-suited for inconsistencies:
Heyninck et al.’s Definition 15 and Proposition 5 [2] demonstrate how inconsistent pairs are excluded
in their framework. Bi et al. [11] construct a generalized variant of AFT that relaxes AFT to deal with
inconsistent approximations and in prior work [12], we applied this theory to lift this framework to
disjunctive hybrid MKNF. However, this application is separate from AFT and thus could not easily be
applied elsewhere. Here, we recharacterize the semantics of disjunctive hybrid MKNF knowledge bases
using a set of approximators. We provide a method of incorporating nondeterminism and inconsistencies
into AFT.
   This paper is outlined as follows. Section 2 introduces prelimaries for lattice theory (Section 2.1),
and approximation fixpoint theory (Section 2.2). Next, we lift AFT to the nondeterministic setting
(Section 3). In Section 4, we apply our theory to hybrid MKNF knowledge bases after we introduce
prelimaries for disjunctive logic programs (Section 4.1) and hybrid MKNF knowledge bases (Section 4.2).
Finally, we conclude and discuss future work in Section 5.


2. Preliminaries
2.1. Lattice Theory
We review common lattice theory [13] to establish the notation and terminology used throughout this
work. A preorder ⟨𝑆, ⪯⟩ is a relation ⪯ over a non-empty set of elements 𝑆 that satisfies: reflexivity
(∀𝑥 ∈ 𝑆, 𝑥 ⪯ 𝑥) and transitivity (∀𝑥, 𝑦, 𝑧 ∈ 𝑆 if 𝑥 ⪯ 𝑦 and 𝑦 ⪯ 𝑧 then 𝑥 ⪯ 𝑧). If the order ⪯ also
satisfies antisymmetry, (∀𝑥, 𝑦 ∈ 𝑆, if 𝑥 ⪯ 𝑦 and 𝑦 ⪯ 𝑥 then 𝑥 = 𝑦), then we call it a partial order (or
poset for short). Without confusion, we sometimes refer to a poset ⟨𝑆, ⪯⟩ simply by 𝑆 or ⪯. Given a
preorder ⟨⪯, 𝑆⟩, we call an element 𝑥 ∈ 𝑆 an upper bound (resp. a lower bound) of a subset 𝑄 ⊆ 𝑆 if
∀𝑦 ∈ 𝑄, 𝑦 ⪯   ⋁︀ 𝑥 (resp. ∀𝑦 ∈ 𝑄, 𝑥 ⪯ 𝑦). An upper bound of ⋀︀𝑄 w.r.t. a poset ⟨𝑆, ⪯⟩ is a least upper bound,
denoted as ⪯ (𝑄) (resp. greatest lower bound , denoted as ⪯ (𝑄)) if it is a lower bound of the set of all
upper bounds of 𝑄 (resp. an upper bound of the set of all lower bounds of 𝑄). A complete lattice ⟨ℒ, ⪯⟩
is a partial order s.t. a least upper bound
                                        ⋀︀ and greatest lower
                                                           ⋁︀ bound exists for every subset 𝑆 ⊆ ℒ. For a
complete lattice ⟨ℒ, ⪯⟩, we denote ⪯ (ℒ) as ⊥⪯ and ⪯ (ℒ) as ⊤⪯ when ℒ is clear from context or
simply as ⊥ and ⊤ when the lattice’s relation is unambiguous. Given a complete lattice ⟨ℒ, ⪯⟩, we say
a function 𝑓 : ℒ → ℒ is monotone if for each 𝑥, 𝑦 ∈ ℒ, having 𝑥 ⪯ 𝑦 implies 𝑓 (𝑥) ⪯ 𝑓 (𝑦).
   Every preorder ⟨ℒ𝑎 , ⪯⟩ has a dual ordering ⟨ℒ𝑎 , ⪯ ⟩ where the ordering has been “flipped”. That is,
(𝑎 ⪯ 𝑏) ⇐⇒ (𝑏 ⪯ 𝑎). We also define a strict variant ≺ to mean two elements are comparable and not
equal, i.e., (𝑎 ≺ 𝑏) ⇐⇒ ((𝑎 ⪯ 𝑏) ∧ 𝑎 ̸= 𝑏). We use ℒ1 × ℒ2 to denote the cartesian product between
two sets and ℒ2 to mean ℒ × ℒ. We use ℘(𝑆) to indicate the set of all subsets of 𝑆 and use ℘𝑜 (𝑆) to
denote the set of all non-empty subsets of 𝑆.
     We use subscript notation to denote the projection of components of a tuple 𝑠 ∈ ℒ2 , that is,
(𝑠1 , 𝑠2 ) = 𝑠.
    Given a complete lattice ⟨ℒ, ⪯⟩ and a ⪯-monotone function 𝑜 : ℒ → ℒ, an element 𝑥 ∈ ℒ is a
fixpoint of 𝑜 if 𝑥 = 𝑜(𝑥). The set of all fixpoints of 𝑜 has a lower bound that is also a fixpoint of 𝑜 [14].
We call this element the least fixpoint of 𝑜 and denote it as lfp⪯𝛼 𝑜.
  We denote partially applied functions using a “·” in place of arguments to be filled in, that is,
for a function 𝑜(𝑇, 𝑃 ) : ℒ2 → ℒ2 , we write 𝑜(·, 𝑃 ) (resp. 𝑜(𝑇, ·)) to mean 𝜆𝑥 ⇒ 𝑜(𝑥, 𝑃 ) (resp.
𝜆𝑥 ⇒ 𝑜(𝑇, 𝑥)). If a “·” is used within a tuple projection, the body of the lambda abstraction includes
the projections, for example,

                                                              (where 𝑓 (𝑥, 𝑦) : ℒ2 → ℒ2 )
                           (︀                )︀
               𝑓 (𝑥, ·)1 = 𝜆𝑦 ⇒ (𝑓 (𝑥, 𝑦)1 )

This makes it possible to write lfp⪯ 𝑜(𝑇, ·)1 to express the ⪯-least fixpoint of 𝑜 as partially applied
with 𝑇 . We use 𝑚𝑖𝑛⪯ (𝑆) to denote the set 𝑚𝑖𝑛⪯ (𝑆) := {𝑏 ∈ 𝑆 | ¬∃𝑏′ ∈ 𝑆, 𝑏′ ≺ 𝑏}.

2.2. Generalized AFT
Introduced by Denecker et al. [2000], AFT (Approximation Fixpoint Theory) is a framework for defining
operators over a bilattice. The framework captures a variety of nonmonotonic semantics through
fixpoints of a stable revision operator. Bi et al. [11] propose a generalization of AFT (Approximation
Fixpoint Theory) that relaxes the exact condition on approximators. That is, in traditional AFT, an
operator must map exact pairs to exact pairs. In generalized AFT, an operator can also map exact pairs
to inconsistent pairs. This enhancement enables the creation of more precise approximators for systems
that blend classical and nonmonotonic reasoning.
   First, we define the bilattice on which both original [3] and generalized [11] AFT rely. Given a
complete lattice ⟨ℒ, ⪯⟩, for any two pairs (𝑥′ , 𝑦 ′ ), (𝑥, 𝑦) ∈ ℒ2 ,

                             (𝑥′ , 𝑦 ′ ) ⪯2𝑡 (𝑥, 𝑦) ⇐⇒ ((𝑥′ ⪯ 𝑥) ∧ (𝑦 ′ ⪯ 𝑦))
                             (𝑥′ , 𝑦 ′ ) ⪯2𝑝 (𝑥, 𝑦) ⇐⇒ ((𝑥′ ⪯ 𝑥) ∧ (𝑦 ′ ⪯ 𝑦))

  We introduce the generalization of AFT from Bi et al. [11] and Liu and You [1].

Definition 2.1. A (generalized) approximator 𝑜 : ℒ2 → ℒ2 over a complete lattice ⟨ℒ, ⪯⟩ is a ⪯2𝑝 -
monotone function such that for any element 𝑥 ∈ ℒ if

                         𝑜(𝑥, 𝑥)1 ⪯ 𝑜(𝑥, 𝑥)2 then 𝑜(𝑥, 𝑥) = (𝑜(𝑥, 𝑥)1 , 𝑜(𝑥, 𝑥)1 )

   Traditional AFT [3] requires approximators to map exact pairs (a pair (𝑥, 𝑥)) to exact pairs. Here, we
only require that exact pairs are not mapped to inexact, consistent pairs (a pair (𝑥, 𝑦) is consistent if
𝑥 ⪯ 𝑦). For example, the following approximator is possible in this generalized AFT [11], but not in
traditional AFT [3].

Example 1. Given a complete lattice {⊥, ⊤}, define 𝑜 : ℒ2 → ℒ2 as follows.
                                          {︃
                                            (⊤, ⊥) if 𝑥 = 𝑦 = ⊥
                               𝑜(𝑥, 𝑦) :=
                                            (𝑥, 𝑦) otherwise

The above operator is ⪯2𝑝 -monotone as 𝑜(⊥, ⊥) = 𝑜(⊤, ⊥). Here, the exact pairs (⊥, ⊥) and (⊤, ⊤) map
to an inconsistent and exact pair respectively. Thus, 𝑜 is an approximator.

   We can reuse the original AFT [3] definition of stable fixpoints for approximators [1], which are
shown to be well-defined; however, these fixpoints might not be consistent. As a result, some stable
fixpoints of approximators do not correspond to intended models.

Definition 2.2. Given an approximator 𝑜, the stable revision operator 𝑆(𝑜) : ℒ2 → ℒ2 is defined as
follows: 𝑆(𝑜)(𝑥, 𝑦) := (lfp⪯𝛼 (𝑜(·, 𝑦)1 ), lfp⪯𝛼 (𝑜(𝑥, ·)2 )).

  For an approximator 𝑜, we refer to the fixpoints of S(o) as stable fixpoints. The smallest fixpoint
w.r.t. ⪯2𝑝 is called the least stable fixpoint. Critically, this modified variant of AFT maintains the truth
minimality property of traditional AFT.
Proposition 2.1. Let (𝑥, 𝑦) be a stable fixpoint of a approximator 𝑜 over ⟨ℒ, ⪯2𝑝 ⟩.

    • (𝑥, 𝑦) is a fixpoint of 𝑜, and
    • there does not exist a fixpoint (𝑥′ , 𝑦 ′ ) (distinct from (𝑥, 𝑦)) of 𝑜 s.t. (𝑥′ , 𝑦 ′ ) ≺2𝑡 (𝑥, 𝑦)

  For the above, we can follow Denecker et al. [3]’s proof (of Theorem 4), which does not rely on
exactness.


3. Generalized Approximator Sets
In this section, we abstract and generalize the application of AFT on disjunctive hybrid MKNF [12] so
that it works within the confines of AFT and can be applied to other semantics. Namely, we obtain a
general method of lifting deterministic stable revision to nondeterministic semantics. Optionally, in
this framework one can also choose to eliminate select stable fixpoints, namely the stable fixpoints that
correspond to inconsistencies.
   When they apply their AFT to hybrid MKNF knowledge bases, Liu and You [1] couple their approxi-
mator with a condition that checks whether the stable fixpoint corresponds to an MKNF model. This is
a critical step in addressing inconsistencies because it allows us to prevent inconsistent stable fixpoints.
As we will see later on, additional complications w.r.t. ⪯2𝑡 -minimality may arise when lifting this theory
to support nondeterministic semantics.
   We lift approximators to a nondeterministic setting by considering sets of approximators coupled
with a condition to filter unintended stable fixpoints.

Definition 3.1. A (generalized) a-set ⟨𝐻, Θ⟩ is a set of approximators 𝐻 over the complete lattice
⟨ℒ2 , ⪯2𝑝 ⟩ paired with its acceptance relation Θ ⊆ (𝐻 × ℒ2 ).

   By harnessing a family of deterministic approximators, we can characterize nondeterministic seman-
tics. A generalized approximator can have unintended stable fixpoints, that is, stable fixpoints that do
not correspond to the intended semantics. The acceptance relation enables us to filter out unintended
stable fixpoints. However, use of the relation is optional and the theory can be applied without it by
fixing the acceptance relation to be 𝐻 × ℒ2 (the maximal acceptance relation).
   We lift the stable revision operator to a-sets.

Definition 3.2. A pair (𝑥, 𝑦) ∈ ℒ s.t. 𝑥 ⪯ 𝑦 is a (generalized) a-stable fixpoint of an a-set ⟨𝐻, Θ⟩ if

                                (𝑥, 𝑦) ∈ 𝑚𝑖𝑛⪯2𝑡 {𝑆(ℎ)(𝑥, 𝑦) | (ℎ, (𝑥, 𝑦)) ∈ Θ}

   The mechanism above applies stable revision to all approximators in the a-set that are part of the
acceptance relation. Each image has an opportunity to block a pair from being an a-set by computing
a ≺2𝑡 -smaller pair. In their notion of stable revision, Liu and You [1] apply a condition to filter some
stable fixpoints, which we generalize here as the “acceptance relation”. What’s new here is that the
condition also plays a role in determinining whether a computed pair can “block” another pair from
being an a-stable fixpoint. By using the maximal acceptance relation, the condition does not remove
any stable fixpoints (and the definitions can be further simplified). For any a-set stable fixpoint (𝑥, 𝑦)
that is a stable fixpoint of ℎ ∈ 𝐻, we can remove (ℎ, (𝑥, 𝑦)) from Θ to prevent (𝑥, 𝑦) from being an
a-stable fixpoint. Additionally, if a stable fixpoint (𝑥, 𝑦) of ℎ ∈ 𝐻 is not an a-stable fixpoint due to an
approximator ℎ′ ∈ 𝐻 s.t. 𝑆(ℎ′ )(𝑥, 𝑦) ≺2𝑡 (𝑥, 𝑦), we can remove (ℎ′ , (𝑥, 𝑦)) from Θ in effort to make
(ℎ, (𝑥, 𝑦)) an a-stable fixpoint of ⟨𝐻, Θ⟩. This will remove ℎ′ from participating in the consideration of
(𝑥, 𝑦) as an a-stable fixpoint. These points are demonstrated concretely in the coming Example 2.
   The property of ⪯2𝑡 -minimality is critical to stable fixpoints. Given any two stable fixpoints (𝑥′ , 𝑦 ′ )
and (𝑥, 𝑦) of ℎ, we have that (𝑥′ , 𝑦 ′ ) ≺2𝑡 (𝑥, 𝑦) does not hold. By using 𝑚𝑖𝑛⪯2𝑡 on the stable fixpoint
of approximators in 𝐻, we ensure this property also holds for a-stable fixpoints. First, we demonstrate
this property without using the acceptance relation (i.e., we fix the relation to be maximal).
Proposition 3.1. For an a-set ⟨𝐻, (𝐻 × ℒ2 )⟩ and the set 𝑊 , consisting of its a-stable fixpoints, we have
𝑊 = 𝑚𝑖𝑛⪯2𝑡 (𝑊 ).
  Introducing the acceptance relation, i.e., using a smaller relation than in the above, introduces some
complications w.r.t. the minimality of stable fixpoints. The acceptance relation can add or remove
a-stable fixpoints. Thus, truth-minimality may be disrupted. We generalize the above proposition to
handle any acceptance relation by imposing a condition on this relation.
Proposition 3.2. For an a-set ⟨𝐻, Θ⟩ and the set 𝑊 consisting of its a-stable fixpoints, we have 𝑊 =
𝑚𝑖𝑛⪯2𝑡 (𝑊 ) if Φ satisfies the following condition,

                        ∀(ℎ′ , (𝑥′ , 𝑦 ′ ))(ℎ, (𝑥, 𝑦)) ∈ Θ* where (𝑥′ , 𝑦 ′ ) ≺2𝑡 (𝑥, 𝑦) we have
                         ∃(ℎ′′ , (𝑥′′ , 𝑦 ′′ )) ∈ Θ* , s.t. (𝑥′′ , 𝑦 ′′ ) ≺2𝑡 (𝑥, 𝑦), (ℎ′′ , (𝑥, 𝑦)) ∈ Θ

where Θ* denotes the subset of Θ consisting of every pair (ℎ, (𝑥, 𝑦)) s.t. 𝑆(ℎ)(𝑥, 𝑦) = (𝑥, 𝑦).
Proof. Assume the condition holds for ⟨𝐻, Θ⟩ and let (𝑥′ , 𝑦 ′ ) and (𝑥, 𝑦) be two stable fixpoints of ℎ′ ∈ 𝐻
and ℎ ∈ 𝐻 respectively s.t. (𝑥′ , 𝑦 ′ ) ⪯2𝑡 (𝑥, 𝑦) and both pairs are a-stable fixpoints of ⟨𝐻, Θ⟩. We intend
to show (𝑥′ , 𝑦 ′ ) = (𝑥, 𝑦) and it will follow that 𝑊 = 𝑚𝑖𝑛⪯2𝑡 (𝑊 ). Assume for the sake of contradiction,
(𝑥′ , 𝑦 ′ ) ̸= (𝑥, 𝑦). It follows from our initial assumption of (𝑥′ , 𝑦 ′ ) ⪯2𝑡 (𝑥, 𝑦) that (𝑥′ , 𝑦 ′ ) ≺2𝑡 (𝑥, 𝑦).
By the condition, we have a stable fixpoint (𝑥′′ , 𝑦 ′′ ) of ℎ′′ ∈ 𝐻 s.t. (𝑥′′ , 𝑦 ′′ ) ≺2𝑡 (𝑥, 𝑦). We briefly
follow Denecker et al. [3]’s proof (Theorem 4). We have 𝑥′′ ⪯ 𝑥 and 𝑦 ′′ ⪯ 𝑦. The ⪯2𝑝 -monotonicity
of ℎ′′ ensures that ℎ′′ (·, 𝑦 ′ )2 is ⪯-antimonotone, that is, ℎ′′ (𝑥, 𝑦 ′′ )2 ⪯ ℎ′′ (𝑥′′ , 𝑦 ′′ )2 = 𝑦 ′′ . Thus, 𝑦 ′′ is a
prefixpoint of ℎ′′ (𝑥, ·) and the least fixpoint of ℎ′′ (𝑥, ·) is less than 𝑦 ′′ [14]. We have lfp⪯ ℎ′′ (𝑥, ·) ⪯ 𝑦 ′′ ,
with 𝑦 ′′ ⪯ 𝑦, it follows by transitivity that (lfp⪯ ℎ′′ (𝑥, ·)) = 𝑆(ℎ′′ )(𝑥, 𝑦)2 ⪯ 𝑦. We can apply a
similar approach to show 𝑆(ℎ′′ )(𝑥, 𝑦)1 ⪯ 𝑥, thus 𝑆(ℎ′′ )(𝑥, 𝑦) ⪯2𝑡 (𝑥, 𝑦). Because (𝑥, 𝑦) is an a-stable
fixpoint of ⟨𝐻, Θ⟩, we have (𝑥, 𝑦) ∈ 𝑚𝑖𝑛⪯2𝑡 {𝑆(ℎ)(𝑥, 𝑦) | (ℎ, (𝑥, 𝑦)) ∈ Θ}. With (ℎ′′ , (𝑥, 𝑦)) ∈ Θ and
𝑆(ℎ)(𝑥, 𝑦) = (𝑥, 𝑦), it follows that ¬(𝑆(ℎ′′ )(𝑥, 𝑦) ≺2𝑡 (𝑥, 𝑦)). With this and 𝑆(ℎ′′ )(𝑥, 𝑦) ⪯2𝑡 (𝑥, 𝑦), it
follows that 𝑆(ℎ′′ )(𝑥, 𝑦) = (𝑥, 𝑦), that is, (𝑥, 𝑦) is a stable fixpoint of ℎ′′ . With two stable fixpoints
(𝑥′′ , 𝑦 ′′ ) ≺2𝑡 (𝑥, 𝑦) of ℎ′′ , we contradict Proposition 2.1.


 Intuitively, the condition in the proposition above ensures that smaller (w.r.t. ⪯2𝑡 ) stable fixpoints
must block larger stable fixpoints. We demonstrate this concretely in the following.
Example 2. Let ⟨ℒ, ⪯⟩ be a complete lattice s.t. ℒ = {⊥, ⊤} and ⊥ ⪯ ⊤. Let ℎ⊥ and ℎ⊤ be two constant
functions over ℒ2 mapping to (⊥, ⊥) and (⊤, ⊤) respectively. With 𝐻 = {ℎ⊥ , ℎ⊤ }, let Θ1 := 𝐻 × ℒ2 .
Clearly, (⊥, ⊥) and (⊤, ⊤) are stable fixpoints of ℎ⊥ and ℎ⊤ respectively. While (⊥, ⊥) is an a-stable
fixpoint of ⟨𝐻, Θ1 ⟩, (⊤, ⊤) is not because (ℎ⊥ , (⊤, ⊤)) ∈ Θ1 and 𝑆(ℎ⊥ )(⊤, ⊤) ≺2𝑡 (⊤, ⊤).
   For (⊤, ⊤) to be an a-stable fixpoint, we must remove (ℎ⊥ , (⊤, ⊤)) ∈ Θ1 . but this would vio-
late the condition on the acceptance relation in Proposition 3.2. That is, with (⊥, ⊥) ≺2𝑡 (⊤, ⊤) and
(ℎ⊥ , (⊥, ⊥)), (ℎ⊤ , (⊤, ⊤)) ∈ Θ. Without this condition, a-stable fixpoints would not be ⪯2𝑡 -minimal.
   Let Θ2 := {ℎ⊤ } × ℒ2 . We have that (⊤, ⊤) is a a-stable fixpoint of ⟨𝐻, Θ2 ⟩, but (⊥, ⊥) is not. Thus,
altering the acceptance relation can both add and remove a-stable fixpoints.
  A-sets and a-stable fixpoints generalize our prior methods [12] to capture the semantics of disjunctive
hybrid MKNF using a set of operators. Now that we’ve expressed this theory at the algebra level, new
opportunities for its application are unlocked.


4. Application to Hybrid MKNF Knowledge Bases
In this section, we apply the theory from the previous section to disjunctive hybrid MKNF knowledge
bases. This demonstrates that nothing was lost in generalizing the previous theory that used sets of
operators (not approximators) to capture the semantics [12]. First, we cover the necessary preliminaries.
4.1. Preliminaries: Disjunctive Logic Programs
Disjunctive stable semantics extends answer set programming by allowing rules with disjunctions in
their heads [15]. This feature raises the expressivity class of programs by enabling them to capture
problems in a higher level of the polynomial hierarchy [16]. Furthermore, disjunctive rules allow
succinct representation of nondeterministic solutions to problems.
   The partial stable model semantics extend stable model semantics by adding an additional truth value
(undefined), which is to be assigned to atoms with an unknown truth value. We introduce Przymusinski
[17]’s three-valued semantics for disjunctive logical programs. A disjunctive logic program (DLP) 𝒫 is a
set of rules, objects with three components: a head, a positive body, and a negative body. We denote
these components as head(𝑟), body + (𝑟), and body − (𝑟) respectively, and each is a set of ground atoms
from a propositional language 𝐴𝑡𝑜𝑚𝑠(𝒫). We write a rule 𝑟 as follows.
                            ℎ1 , . . . , ℎ𝑖 ← 𝑝1 , . . . , 𝑝𝑗 , not 𝑛1 , . . . , not 𝑛𝑘
where head(𝑟) = {ℎ1 , . . . , ℎ𝑖 }, body + (𝑟) = {𝑝1 , . . . , 𝑝𝑗 }, and body − (𝑟) = {𝑛1 , . . . , 𝑛𝑘 }. We use
body(𝑟) to denote the entire expression to the right of the arrow above (maintaining the not syntax).
A rule 𝑟 is normal if its head contains exactly one atom (i.e. |head(𝑟)| = 1), and a program 𝒫 is normal
if it consists solely of normal rules.
    A (three-valued) interpretation (𝑇, 𝑃 ) of a disjunctive logic program 𝒫 is a pair of sets containing
atoms from 𝐴𝑡𝑜𝑚𝑠(𝒫) s.t. 𝑇 ⊆ 𝑃 ⊆ 𝐴𝑡𝑜𝑚𝑠(𝒫). An interpretation (𝑇, 𝑃 ) assigns each atom 𝑎 ∈
𝐴𝑡𝑜𝑚𝑠(𝒫) to one of three truth values: t𝑟𝑢𝑒 (iff 𝑎 ∈ 𝑇 ∧ 𝑎 ∈ 𝑃 ), undefined (iff 𝑎 ̸∈ 𝑇 ∧ 𝑎 ∈ 𝑃 ), and
f 𝑎𝑙𝑠𝑒 (iff 𝑎 ̸∈ 𝑇 ∧ 𝑎 ̸∈ 𝑃 ). This logic leverages two orderings between interpretations, a truth ordering
⪯2𝑡 and a precision ordering ⪯2𝑝 . Both ordering are obtained from the bilattice on ⟨℘(𝐴𝑡𝑜𝑚𝑠(𝒫)), ⊆⟩.
Note that ℘(𝐴𝑡𝑜𝑚𝑠(𝒫)) contains inconsistent pairs, i.e., not every pair is an interpretation. The ⪯2𝑡
ordering respects the linear ordering f ≤ u ≤ t while the latter uses the partial ordering composed
of u ≤ f and u ≤ t where f and t are incomparable. Intuitively, a rule is satisfied if some atom in
its head is at least as true (w.r.t. f ≤ u ≤ t) as the conjunction of its body atoms. Negation changes
f to t and t to f while mapping u to itself. We use the bilattices [18] that lift the truth-ordering
(f ≤ u ≤ t) and precision-ordering (u ≤ 𝑠, 𝑠 ∈ {t, f }) to the complete lattices ⟨𝐴𝑡𝑜𝑚𝑠(𝒫)2 , ⪯2𝑡 ⟩ and
⟨𝐴𝑡𝑜𝑚𝑠(𝒫)2 , ⪯2𝑝 ⟩ respectively. We have an element (𝑇, 𝑃 ) ∈ ℘(𝐴𝑡𝑜𝑚𝑠(𝒫))2 where 𝑇 ̸⊆ 𝑃 , thus not
every element in ℘(𝐴𝑡𝑜𝑚𝑠(𝒫))2 is an interpretation. If we restrict our focus to interpretations (i.e.,
pairs s.t. 𝑇 ⊆ 𝑃 ), the lattice orderings above compare the individual truth evaluations of atoms. For
example, an interpretation that assigns t to an atom 𝑎 is greater (for both lattices) than an interpretation
that assigns u to 𝑎 (assuming other atoms have the same truth values).
    We formally define rule satisfaction. Given a pair of sets 𝐴, 𝐵 ⊆ 𝐴𝑡𝑜𝑚𝑠(𝒫) (not necessarily an
interpretation) we define satisfied(𝐴,𝐵) (𝒫) as the subset of 𝒫, {𝑟 ∈ 𝒫 | body + (𝑟) ⊆ 𝐴, body − (𝑟) ∩ 𝐵 =
∅}. For an interpretation (𝑇, 𝑃 ), the set satisfied(𝑇,𝑃 ) (𝒫) contains all rules whose body evaluates as
true (satisfied without undefined atoms), while satisfied (𝑃,𝑇 ) (𝒫) contains all rules whose body evaluates
as possibly true (satisfied with or without undefined atoms). We say an interpretation (𝑇, 𝑃 ) is a
model of a program 𝒫 if all rules are satisfied by (𝑇, 𝑃 ), i.e., for each 𝑟 ∈ 𝒫,
                           (𝑟 ∈ satisfied (𝑇,𝑃 ) (𝒫)) ⇒ (head(𝑟) ∩ 𝑇 ̸= ∅), and
                            (𝑟 ∈ satisfied (𝑃,𝑇 ) (𝒫)) ⇒ (head(𝑟) ∩ 𝑃 ̸= ∅)
The model condition ensures every satisfied rule has an atom in its head with an appropriate truth value.
A stable model minimizes truth while keeping negation stable [19]. Intuitively, we do not want to lower
the truth values of atoms if it results in rules deriving higher truth values for some of those atoms.
To accommodate this, when shrinking an interpretation (𝑇, 𝑃 ) w.r.t. ⪯2𝑡 , we evaluate the negative
bodies of rules against the original interpretation (𝑇, 𝑃 ) while the positive bodies and rule heads are
evaluated against the shrunken interpretation (𝑋, 𝑌 ). We outline this formally in the following. Given
two interpretations (𝑋, 𝑌 ) and (𝑇, 𝑃 ), we say (𝑋, 𝑌 ) is a model of the reduct of 𝒫 w.r.t. (𝑇, 𝑃 ) if for
each 𝑟 ∈ 𝒫,
                           (𝑟 ∈ satisfied (𝑋,𝑃 ) (𝒫)) ⇒ (head(𝑟) ∩ 𝑋 ̸= ∅), and
                                (𝑟 ∈ satisfied (𝑌,𝑇 ) (𝒫)) ⇒ (head(𝑟) ∩ 𝑌 ̸= ∅)

A model is stable if it’s the smallest model (w.r.t. truth) of its reduct.

Definition 4.1. A model (𝑇, 𝑃 ) of a DLP 𝒫 is a (partial) stable model of 𝒫 if there is no model (𝑋, 𝑌 )
of the reduct of 𝒫 w.r.t. (𝑇, 𝑃 ) s.t. (𝑋, 𝑌 ) ≺2𝑡 (𝑇, 𝑃 ).

      Partial stable models correspond to answer sets when 𝑇 = 𝑃 .

4.2. Preliminaries: Hybrid MKNF Knowledge Bases
Defined by Motik and Rosati [10], hybrid MKNF knowledge bases (HMKNF) are a logic designed to
combine ontologies with answer set programming faithfully. Ontologies operate under the open-world
assumption where a fact is only false if it can be proven as such (e.g., through classical reasoning).
Conversely, answer set programming operates under the closed-world assumption, where facts are
assumed to be false if they cannot be proven.
   A critical goal of hybrid MKNF is to construct a hybrid logic that does not simply layer ontologies on
top of answer set programs or vice-versa. A logic is tight [10] if we can perform interleaved reasoning
between ontological concepts and rules. For example, because hybrid MKNF satisfies this property, a
consequence can follow from something in the ontology which follows from a rule, which follows from
the ontology.
   In this paper, we focus very little on ontologies and instead treat them as decidable, polynomial
first-order formulas akin to reasoning black boxes that can perform an entailment function. As such, we
introduce a stripped-down (yet equivalent) version of hybrid MKNF that deals primarily with answer
set programs.
   We give a summary of the semantics of hybrid MKNF knowledge bases using the three-valued
semantics that were introduced by Knorr et al. [20]. A (disjunctive) hybrid MKNF knowledge base
𝒦 = (𝒪, 𝒫) (henceforth, a HMKNF KB) is a disjunctive logic program 𝒫 coupled with an ontology
𝒪 [10]. Here, an ontology 𝒪 is simply an object that can be translated to a first-order formula 𝜋(𝒪),
whose entailment relation can be computed in polynomial-time. For an ontology 𝒪 and a set of atoms
𝑆 ⊆ 𝐴𝑡𝑜𝑚𝑠(𝒫)  ⋀︀ the entailment relation OB𝒪,𝑆 |= 𝜑 holds⋀︀ for a propositional formula 𝜑 if 𝜑 is entailed
by 𝜋(𝒪) ∧ ( 𝑆), this relation always holds if 𝜋(𝒪) ∧ ( 𝑆) is inconsistent (the principle of explosion)
and OB𝒪,𝑆 ̸|= 𝑎 holds otherwise.
   An interpretation (𝑇, 𝑃 ) is 𝒪-consistent if 𝜋(𝒪) ∧ ( 𝑃 ) is consistent (i.e. it has at least one
                                                            ⋀︀
model under first-order logic). An 𝒪-consistent (𝑇, 𝑃 ) is 𝒪-saturated if OB𝒪,𝑃 ̸|= 𝑎 for each 𝑎 ∈
(𝐴𝑡𝑜𝑚𝑠(𝒫) ∖ 𝑃 ) and OB𝒪,𝑇 ̸|= 𝑎 for each 𝑎 ∈ (𝐴𝑡𝑜𝑚𝑠(𝒫) ∖ 𝑇 )1 . Intuitively, we cannot derive new
consequences from 𝒪 w.r.t. an 𝒪-saturated interpretation. We call an interpretation (𝑇, 𝑃 ) a model of a
HMKNF KB 𝒦 = (𝒪, 𝒫) if it is a model of 𝒫 and it is 𝒪-saturated.

Definition 4.2. We call a model (𝑇, 𝑃 ) of an HMKNF KB 𝒦 a 𝒫-MKNF model of 𝒦 if for any 𝒪-saturated
interpretation (𝑋, 𝑌 ) s.t. (𝑋, 𝑌 ) ≺2𝑡 (𝑇, 𝑃 ), (𝑋, 𝑌 ) is not a model of the reduct of 𝒫 w.r.t. (𝑇, 𝑃 ).

 This definition very similar to partial stable models (Definition 4.1) with the key difference that (𝑇, 𝑃 )
must be 𝒪-saturated and all smaller interpretations tested against the reduct must also be 𝒪-saturated.
 We give an example knowledge base to instantiate and demonstrate the above definitions.

Example 3. Let 𝒦 = (𝒪, 𝒫) such that 𝜋(𝒪) = ((𝑐 ∨ 𝑎) ∧ 𝑑) and 𝒫 contains the rule (𝑎, 𝑏 ←). The
interpretation ({𝑏}, {𝑏}) is not 𝒪-saturated because 𝑑 ∈ (𝐴𝑡𝑜𝑚𝑠(𝒫) ∖ 𝑇 ) and OB𝒪,{𝑏} |= 𝑑 (more
generally, OB𝒪,∅ |= 𝑑). The interpretation ({𝑏, 𝑑}, {𝑏, 𝑑}) is 𝒪-saturated. Note that even though 𝑐 is false
w.r.t. ({𝑏, 𝑑}, {𝑏, 𝑑}) and 𝜋(𝒪) ∧ ¬𝑐 implies 𝑎, we do not derive 𝑎 because falsely assigned atoms do not
participate in the derivation of positive atoms using the ontology. This is a critical aspect of how hyrbid
MKNF differentiates between classically false atoms and atoms that are false due to negation as failure.
1
    We require (𝑇, 𝑃 ) to be 𝒪-consistent to handle the case where 𝑃 = 𝐴𝑡𝑜𝑚𝑠(𝒫), in all other cases, it is implied by the
    principle of explosion.
   As a result, this knowledge base has two 𝒫-MKNF models, namely ({𝑏, 𝑑}, {𝑏, 𝑑}) and ({𝑎, 𝑑}, {𝑎, 𝑑}).
Note that 𝒫 has two partial stable models (({𝑏}, {𝑏}) and ({𝑎}, {𝑎})) and 𝒪 simply requires that 𝑑 be
true.

   𝒫-MKNF models and partial stable models are closely related. For HMKNF KBs with empty ontologies
(every interpretation is 𝒪-saturated), 𝒫-MKNF models are equivalent to partial stable models. Here, we
present 𝒫-MKNF models instead of hybrid MKNF models (as introduced by Knorr et al. [20]) because the
full introduction of the logic is not necessary for our results. We can limit our focus to the interpretation
of atoms that appear in 𝒫 because it is straightforward to interpret the remaining atoms from 𝒪.

Proposition 4.1. Originally, hybrid MKNF uses MKNF interpretations, sets of first-order interpretations
(interpretations of first-order formulas), to interpret atoms. We can convert a 𝒫-MKNF model to a full
MKNF model of 𝒦 named (𝑀, 𝑁 ).

                            (𝑀, 𝑁 ) = ({𝐼 | OB𝒪,𝑇 |= 𝐼}, {𝐼 | OB𝒪,𝑃 |= 𝐼})

We can also construct an interpretation (𝑇, 𝑃 ) from a MKNF model (𝑀, 𝑁 )

                                𝑇 := {𝑎 ∈ 𝐴𝑡𝑜𝑚𝑠(𝒫) | ∀𝐼 ∈ 𝑀, 𝐼 |= 𝑎}
                                𝑃 := {𝑎 ∈ 𝐴𝑡𝑜𝑚𝑠(𝒫) | ∀𝐼 ∈ 𝑁, 𝐼 |= 𝑎}

  A proof of this proposition can be found in [21], which is based on a prior work [12], where we
showed how the transformation outlined above is related to the usual formulation of partial MKNF
models of hybrid MKNF [20].
  In prior work [22], we shown that, using the transformation outlined above, one can easily generalize
the work in this paper to the usual formulation of hybrid MKNF [10].

4.3. Applying Approximator Sets
Liu and You [1] introduce an approximator for normal
                                                   ⋃︀ HMKNF KBs. We use head(𝒫) to denote the set
of all head atoms in the program 𝒫, i.e., the set ( 𝑟∈𝒫 head(𝑟)).

Definition 4.3 (Liu and You [1]). Given an HMKNF KB 𝒦 = (𝒪, 𝒫)

                             Γ𝒫 (𝑇, 𝑃 ) := head(satisfied(𝑇,𝑃 ) (𝒫))
                            Φ𝒦 (𝑇, 𝑃 )1 := Γ𝒫 (𝑇, 𝑃 ) ∪{𝑎 | OB𝒪,𝑇 |= 𝑎}
                                          (︁                              )︁
                            Φ𝒦 (𝑇, 𝑃 )2 := Γ𝒫 (𝑃, 𝑇 ) ∖ {𝑎 | OB𝒪,𝑇 |= ¬𝑎}
                                                       ∪ {𝑎 | OB𝒪,𝑃 |= 𝑎}

   The above operator is nearly symmetric (i.e. Φ𝒦 (𝑇, 𝑃 )1 = Φ𝒦 (𝑃, 𝑇 )2 ), however, the ontology may
be used to block the derivation of some atoms in the heads of rules (Thus, Φ𝒦 (𝑇, 𝑃 )1 ̸= Φ𝒦 (𝑃, 𝑇 )2 ).
This can result in some stable fixpoints having the property where some rules are not satisfied because
the derivation of a head atom is blocked. This can easily be detected by checking whether Γ𝒫 (𝑃, 𝑇 )1 ∩
{𝑎 | OB𝒪,𝑇 |= ¬𝑎} is empty. When this set is empty, Φ(𝑇, 𝑃 )2 is equal to Φ(𝑃, 𝑇 )1 , i.e., the operator
is symmetric for the given pair.
   We lift this approximator to disjunctive HMKNF KBs by defining an a-set paired with the aforemen-
tioned symmetry condition from Liu and You [1].

Definition 4.4. Let 𝒦 = (𝒪, 𝒫) be a HMKNF KB. We define ⟨𝐻𝒦 , Θ𝒦 ⟩,

                                𝐻𝒦 := {Φ(𝒪,𝒫 ′ ) | 𝒫 ′ ∈ normal(𝒫)}
                                Θ𝒦 := {(ℎ, (𝑇, 𝑃 )) ∈ (𝐻𝒦 × ℒ2 ) |
                                           ℎ(𝑇, 𝑃 ) = (ℎ(𝑇, 𝑃 )1 , ℎ(𝑃, 𝑇 )1 ) and
                                        OB𝒪,𝑃 is consistent }
                                     {︁
                         𝑛𝑜𝑟𝑚𝑎𝑙(𝒫) := {ℎ𝑐(𝑟) | 𝑟 ∈ 𝒫} | ∃ℎ𝑐, ∀𝑟 ∈ 𝒫,
                                                                                }︁
                                             ∃𝑎 ∈ head(𝑟), ℎ𝑐(𝑟) = (𝑎 ← body(𝑟))

   The set normal(𝒫) splits a program into its normal counterparts by mapping each disjunctive rule to
a normal rule with an overlapping head. This set is a subset of split disjunctive databases [23], which
map each rule to several normal rules. This a-set captures three-valued hybrid MKNF semantics.

Theorem 4.1. A pair (𝑇, 𝑃 ) is an a-stable fixpoint of ⟨𝐻𝒦 , Θ𝒦 ⟩ iff it is a 𝒫-MKNF model of 𝒦.

Proof. (⇒ by contrapositive) Let (𝑇, 𝑃 ) be an interpretation s.t. its not an 𝒫-MKNF model of 𝒦. If
(𝑇, 𝑃 ) is OB𝒪,𝑃 is inconsistent, then ¬∃(ℎ, (𝑇, 𝑃 )) ∈ 𝑆(Θ𝒦 ). We assume OB𝒪,𝑃 is consistent as
¬∃(ℎ, (𝑇, 𝑃 )) ∈ Θ𝒦 otherwise. If (𝑇, 𝑃 ) is not 𝒪-saturated, then either

                                                               ̸ ∅, or
                                         {𝑎 ̸∈ 𝑇 | OB𝒪,𝑇 |= 𝑎} =
                                         {𝑎 ̸∈ 𝑃 | OB𝒪,𝑃 |= 𝑎} =
                                                               ̸ ∅

Thus, (𝑇, 𝑃 ) is not a fixpoint (or stable fixpoint) of any Φ ∈ 𝐻𝒦 . We assume (𝑇, 𝑃 ) is 𝒪-saturated.
Suppose (𝑇, 𝑃 ) is not a model of 𝒫. It follows that 𝒫 is not a model of any 𝒫 ′ ∈ 𝑛𝑜𝑟𝑚𝑎𝑙(𝒫). We show
Φ(𝒪,𝒫 ′ ) ̸∈ 𝑆(Θ𝒦 )
   (Case 𝑟 ∈ satisfied (𝑃,𝑇 ) (𝒫) s.t. {𝑎} = head(𝑟) and OB𝒪,𝑇 |= ¬𝑎) We have 𝑎 ̸∈ Φ(𝒪,𝒫 ′ ) (𝑇, 𝑃 )2
yet 𝑎 ∈ Φ(𝒪,𝒫 ′ ) (𝑃, 𝑇 )1 . It follows that (Φ(𝒪,𝒫 ′ ) , (𝑇, 𝑃 )) ̸∈ Θ𝒦 . (Case otherwise) We have some rule
𝑟 ∈ satisfied (𝑃,𝑇 ) (𝒫) (resp. 𝑟 ∈ satisfied (𝑇,𝑃 ) (𝒫)) s.t. head(𝑟)∩𝑃 = ∅ (resp. head(𝑟)∩𝑇 = ∅). In either
case, (𝑇, 𝑃 ) is not a fixpoint (or stable fixpoint) of Φ(𝒪,𝒫 ′ ) . It follows that (Φ(𝒪,𝒫 ′ ) , (𝑇, 𝑃 )) ̸∈ 𝑆(Θ𝒦 ).
We can now assume (𝑇, 𝑃 ) is a model of 𝒦. Because (𝑇, 𝑃 ) is not a 𝒫-MKNF model model of 𝒦 while
it is 𝒪-saturated and a model of (𝑇, 𝑃 ), (𝑇, 𝑃 ) is not a stable model of 𝒫, i.e., there exists (𝑇 ′ , 𝑃 ′ )
s.t. (𝑇 ′ , 𝑃 ′ ) ⪯2𝑡 (𝑇, 𝑃 ) and (𝑇 ′ , 𝑃 ′ ) is a model of the reduct of 𝒫 w.r.t. (𝑇 ′ , 𝑃 ′ ). There exists some
𝒫 ′ ∈ normal(𝒫) s.t. (𝑇 ′ , 𝑃 ′ ) is a model of the reduct of 𝒫 ′ w.r.t. (𝑇, 𝑃 ). (𝑇, 𝑃 ) is a ≺2𝑡 -prefixpoint of
𝑆(Φ(∅,𝒫 ′ ) ) (and also of 𝑆(Φ(𝒪,𝒫 ′ ) )). It follows that (𝑇, 𝑃 ) is not in min⪯2𝑡 {𝑆(𝜑)(𝑇, 𝑃 ) | 𝜑 ∈ 𝐻𝒦 } and
thus it is not an a-stable fixpoint of 𝐻𝒦 .
   (⇐) (By contrapositive) Let (𝑇, 𝑃 ) be an interpretation s.t. it is not an a-stable fixpoint of 𝐻𝒦 . If
(𝑇, 𝑃 ) is not a model of 𝒫 or it is not 𝒪-saturated, then it is not a 𝒫-MKNF model of 𝒦. If we assume
these, it follows that (𝑇, 𝑃 ) is 𝒪-consistent and thus (𝑇, 𝑃 ) ∈ Θ𝒦 . We have some 𝒫 ′ ∈ normal(𝒫)
s.t. 𝑆(Φ(𝒪,𝒫 ′ ) )(𝑇, 𝑃 ) ≺2𝑡 (𝑇, 𝑃 ). It follows that there exists (𝑇 ′ , 𝑃 ′ ) ≺2𝑡 (𝑇, 𝑃 ) such that (𝑇 ′ , 𝑃 ′ ) is
𝒪-saturated and a model of the reduct of 𝒫 ′ w.r.t. (𝑇, 𝑃 ). Thus, (𝑇, 𝑃 ) is not a 𝒫-MKNF model of
𝒦.

   A key factor in the rise of expressivity of DLPs [16] is the possibility for head-cycles (cyclic derivation
between atoms that occur in the same rule head) to allow for multiple atoms in the head of a rule to be
true. We give an example demonstrating the usage of our constructs using a knowledge base with head
cycles.

Example 4. Let 𝒦 = (𝒪, 𝒫) s.t. 𝒪 = (¬𝑎 ∨ 𝑏′ ) ∧ (𝑎′ ∨ ¬𝑏) and 𝒫 is defined as follows.

                                        𝑎, 𝑏 ← 𝑑                      𝑎 ← 𝑎′
                                          𝑑 ← not 𝑐                   𝑏 ← 𝑏′

Here, both 𝑎 and 𝑏 appear together in the head of a rule. If 𝑎 is true, then 𝑏′ follows, then 𝑏. Similarly, if 𝑏 is
true, then 𝑎′ follows, then 𝑎. Thus, a head cycle exists between 𝑎 and 𝑏. We have 𝐻𝒦 = {Φ(𝒪,𝒫𝑎 ) , Φ(𝒪,𝒫𝑏 ) }
where (𝑎 ← 𝑑) ∈ 𝒫𝑎 and (𝑏 ← 𝑑) ∈ 𝒫𝑏 . We sequentially apply the stable operator 𝑆(Φ(𝒪,𝒫𝑎 ) ) to the
⪯2𝑝 -least interpretation (∅, {𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑐, 𝑑}).

                                       𝑆(Φ(𝒪,𝒫𝑎 ) )(∅, {𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑐, 𝑑}) = (∅, {𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑑})
                                                         (𝑐 is removed because it cannot be derived)
                            𝑆(Φ(𝒪,𝒫𝑎 ) )(∅, {𝑎, 𝑎 , 𝑏, 𝑏′ , 𝑑}) = ({𝑑, 𝑎, 𝑏′ , 𝑏, 𝑎′ }, {𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑑})
                                                    ′

                      (𝑑 and 𝑎 are derived because not 𝑐 is true and 𝒫𝑎 “picks” 𝑎 respectively)
                (𝑏 is derived becaue OB𝒪,{𝑎} |= 𝑏′ and 𝑏 is derived from the rule (𝑏 ← 𝑏′ ) )
                  ′

                                                        (Lastly, 𝑎′ is derived becaue OB𝒪,{𝑏} |= 𝑎′ )

The interpretation ({𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑑}, {𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑑}) is a stable fixpoint of 𝑆(Φ(𝒪,𝒫𝑎 ) ). Using similar steps
above, we can show that it is also a stable fixpoint of 𝑆(Φ(𝒪,𝒫𝑏 ) ). In essence, both 𝒫𝑎 and 𝒫𝑏 agree that
both 𝑎 and 𝑏 should be both true. That is, ({𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑑}, {𝑎, 𝑎′ , 𝑏, 𝑏′ , 𝑑}) is an a-stable fixpoint of 𝐻𝒦 ,
and by Theorem 4.1, a 𝒫-MKNF model of 𝒦.
   If we change 𝒪 so that this head cycle is broken, we can observe the minimality check of an a-stable
fixpoint in action. Let 𝒪 = (¬𝑎 ∨ 𝑏′ ). The stable fixpoint of 𝑆(Φ(𝒪,𝒫𝑎 ) ) remains the same, but the stable
fixpoint of 𝑆(Φ(𝒪,𝒫𝑏 ) ) has 𝑎 and 𝑎′ as false. Thus,

                                  lfp⪯2𝑝 (𝑆(Φ(𝒪,𝒫𝑏 ) )) ⪯2𝑡 lfp⪯2𝑝 (𝑆(Φ(𝒪,𝒫𝑎 ) ))

and it follows that lfp⪯2𝑝 (𝑆(Φ(𝒪,𝒫𝑎 ) )) is not an a-stable fixpoint of 𝐻𝒦 .

  Note that in the above example, if we fixed the acceptance relation to be maximal, i.e. Θ𝒦 =
𝐻𝒦 × 𝐴𝑡𝑜𝑚𝑠(𝒫)2 , then the example remains the same. We demonstrate an interesting edge case of
our definitions where the acceptance relation plays a critical role.

Example 5. Let 𝒦 = (𝒪, 𝒫) be the HMKNF KB such that 𝜋(𝒪) := ¬𝑏 and 𝒫 is defined as follows

                      𝑎, 𝑏 ← not 𝑐, not 𝑑                    𝑐 ← not 𝑑                   𝑑 ← not 𝑐

We have normal(𝒫) = {𝒫𝑎 , 𝒫𝑏 } where (𝑎 ← not 𝑐, not 𝑑) ∈ 𝒫𝑎 and (𝑏 ← not 𝑐, not 𝑑) ∈ 𝒫𝑏 . This
knowledge base has one 𝒫-MKNF model which is (∅, {𝑎, 𝑐, 𝑑}), that is, the interpretation that assigns 𝑎, 𝑐,
and 𝑑 to be undefined. This interpretation is 𝒪-saturated (𝜋(𝒪) ∧ {𝑎, 𝑐, 𝑑} is consistent, and no positive
conclusions can be drawn from the ontology), and all the rules are satisfied.
  Because 𝒫 induces two normal programs in normal(𝒫), the set 𝐻Φ𝒦 contains two approximators.

                                            {Φ(𝒪,𝒫𝑎 ) , Φ(𝒪,𝒫𝑏 ) } := 𝐻Φ𝒦

  Notably, we have 𝑆(Φ(𝒪,𝒫𝑏 ) )(∅, {𝑎, 𝑐, 𝑑}) = (∅, {𝑐, 𝑑}). Without the acceptance relation, this prefix-
point of 𝑆(Φ(𝒪,𝒫𝑏 ) ) would prevent (∅, {𝑎, 𝑐, 𝑑}) from being an a-stable fixpoint (due to {𝑐, 𝑑} ⊆ {𝑎, 𝑐, 𝑑}).
  However, we have 𝑆(Φ(𝒪,𝒫𝑏 ) )({𝑎, 𝑐, 𝑑}, ∅)1 = {𝑏, 𝑐, 𝑑} which is not equal to 𝑆(Φ(𝒪,𝒫𝑏 ) )(∅, {𝑎, 𝑐, 𝑑})2 ,
thus (Φ(𝒪,𝒫𝑏 ) , (∅, {𝑏, 𝑐, 𝑑})) ̸∈ Θ𝒦 and 𝒫𝑏 does not participate in determining whether (∅, {𝑎, 𝑐, 𝑑}) is
an a-stable fixpoint.

 We have shown that the extension of AFT proposed by Bi et al. [11] can be lifted to disjunctive
HMKNF KBs with relative ease using a-sets.


5. Discussion and Future Work
Incorporating classical reasoning into answer set programming creates numerous complications for
the use of AFT. We navigate these challenges by adopting a generalized variant of AFT that works
with inconsistent pairs [11], and by working with families of approximators to capture nondetermin-
ism. We arrive at a general-purpose framework that can be applied to characterize nonmonotonic,
nondeterministic systems that incorporate external reasoning, such as hybrid MKNF. Our framework
provides a method to reveal new insights into well-founded propagation which could benefit solvers
and grounders for hybrid MKNF. We believe the framework presented in this paper could be applied to
other hybrid reasoning semantics, but we leave this for future work.
    This work builds upon our previous developments [12] in which we leveraged families of fixpoint
operators to capture the three-valued partial stable semantics of hybrid MKNF knowledge bases. Now
that we have fully linked the idea of using families of operators to AFT, further advancements with
normal hybrid MKNF knowledge bases can lifted to support disjunctive rules. This includes stronger
approximators constructed for normal hybrid MKNF knowledge bases such as our recent approximator
[22] (which wasn’t presented here due to complexity). Our approach to capture disjunctive hybrid
MKNF bears some resemblence to the split programs of Sakama [23]. Our mapping to normal rules is
more strict and we capture partial stable models [17]. While a possible approach could have been to
adopt nondeterministic AFT, which defines nondeterministic stable revision, our approach here has the
advantage that we can leverage existing definitions of traditional AFT, whereas nondeterministic AFT
is a standalone theory. Further, it’s unclear how to lift generalized approximators to nondeterministic
AFT, as nondeterministic AFT does not handle inconsistent pairs.
    To summarize, we have presented a framework that lifts generalized, inconsistent-capable AFT to
handle nondeterministic semantics and we’ve demonstrated that this framework is useful by applying
it to disjunctive hybrid MKNF knowledge bases.


6. Acknowledgments
We would like to thank and acknowledge Alberta Innovates and Alberta Advanced Education for their
financial support of author one.


References
 [1] F. Liu, J.-H. You, Alternating fixpoint operator for hybrid MKNF knowledge bases as an approx-
     imator of AFT, Theory Pract. Log. Program. 22 (2022) 305–334. URL: https://doi.org/10.1017/
     S1471068421000168. doi:10.1017/S1471068421000168.
 [2] J. Heyninck, O. Arieli, B. Bogaerts, Non-deterministic approximation fixpoint theory and its
     application in disjunctive logic programming, Artificial Intelligence 331 (2024) 104110. URL:
     https://www.sciencedirect.com/science/article/pii/S0004370224000468. doi:https://doi.org/
     10.1016/j.artint.2024.104110.
 [3] M. Denecker, V. Marek, M. Truszczyński, Approximations, stable operators, well-founded fixpoints
     and applications in nonmonotonic reasoning, in: Logic-Based Artificial Intelligence, Springer,
     2000, pp. 127–144. doi:10.1007/978-1-4615-1567-8_6.
 [4] N. Pelov, M. Denecker, M. Bruynooghe, Well-founded and stable semantics of logic programs with
     aggregates, Theory and Practice of Logic Programming 7 (2007) 301–353.
 [5] B. Bogaerts, J. Jansen, B. D. Cat, G. Janssens, M. Bruynooghe, M. Denecker, Bootstrapping inference
     in the IDP knowledge base system, New Generation Computing 34 (2016) 193–220.
 [6] C. Antic, T. Eiter, M. Fink, Hex semantics via approximation fixpoint theory, in: Proc. 12th
     International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR-13,
     Corunna, Spain, 2013, pp. 102–115.
 [7] J. Vennekens, D. Gilis, M. Denecker, Splitting an operator: Algebraic modularity results for logics
     with fixpoint semantics, ACM Transactions on Computational Logic 7 (2006) 765–797.
 [8] B. Bogaerts, L. Cruz-Filipe, Fixpoint semantics for active integrity constraints, Artificial Intelle-
     gence 255 (2018) 43–70.
 [9] B. Bogaerts, J. Vennekens, M. Denecker, Safe inductions and their applications in knowledge
     representation, Artificial Intelligence 259 (2018) 167–185.
[10] B. Motik, R. Rosati, Reconciling description logics and rules, J. ACM 57 (2010) 30:1–30:62.
     doi:10.1145/1754399.1754403.
[11] Y. Bi, J.-H. You, Z. Feng, A generalization of approximation fixpoint theory and application, in:
     R. Kontchakov, M.-L. Mugnier (Eds.), 8th International Conference on Web Reasoning and Rule
     Systems, RR 2014, Lecture Notes in Computer Science 8741, Springer, Cham, 2014, pp. 45–59.
[12] S. Killen, J.-H. You, A fixpoint characterization of three-valued disjunctive hybrid MKNF knowledge
     bases, in: Y. Lierler, J. F. Morales, C. Dodaro, V. Dahl, M. Gebser, T. Tekle (Eds.), 38th International
     Conference on Logic Programming, Technical Communications / Doctoral Consortium, Haifa,
     Israel, August 2022, volume 364 of EPTCS, 2022, pp. 51–64. URL: https://doi.org/10.4204/EPTCS.
     364.6. doi:10.4204/EPTCS.364.6.
[13] S. Roman, Lattices and Ordered Sets, Springer New York, 2008. URL: http://link.springer.com/10.
     1007/978-0-387-78901-9. doi:10.1007/978-0-387-78901-9.
[14] A. Tarski, A lattice-theoretical fixpoint theorem and its applications., Pacific Journal of Mathematics
     5 (1955) 285 – 309. doi:10.2140/pjm.1955.5.285.
[15] N. Leone, P. Rullo, F. Scarcello, Disjunctive stable models: Unfounded sets, fixpoint seman-
     tics, and computation 135 (????) 69–112. URL: https://www.sciencedirect.com/science/article/pii/
     S0890540197926304. doi:https://doi.org/10.1006/inco.1997.2630.
[16] T. Eiter, G. Gottlob, On the computational cost of disjunctive logic programming: Propositional
     case, Ann. Math. Artif. Intell. 15 (1995) 289–323. URL: https://doi.org/10.1007/BF01536399. doi:10.
     1007/BF01536399.
[17] T. C. Przymusinski, Stable semantics for disjunctive programs, New Gener. Comput. 9 (1991)
     401–424. doi:10.1007/BF03037171.
[18] N. D. Belnap, A Useful Four-Valued Logic, Springer Netherlands, Dordrecht, 1977, pp. 5–37. URL:
     https://doi.org/10.1007/978-94-010-1161-7_2. doi:10.1007/978-94-010-1161-7_2.
[19] D. Pearce, From Here to There: Stable Negation in Logic Programming, Springer Netherlands,
     Dordrecht, 1999, pp. 161–181. URL: https://doi.org/10.1007/978-94-015-9309-0_8. doi:10.1007/
     978-94-015-9309-0_8.
[20] M. Knorr, J. J. Alferes, P. Hitzler, Local closed world reasoning with description logics under the well-
     founded semantics, Artif. Intell. 175 (2011) 1528–1554. doi:10.1016/j.artint.2011.01.007.
[21] R. Kinahan, S. Killen, K. Wan, J.-H. You, On the foundations of conflict-driven solving for hybrid
     MKNF knowledge bases, in: International Conference on of Logic Programming (ICLP 2024),
     Cambridge, 2024. To appear in a special issue of TPLP.
[22] S. Killen, W. Gao, J.-H. You, Expanding the class of polynomial time computable well-founded
     semantics for hybrid MKNF, in: Workshops co-located with the 39th International Conference
     on Logic Programming (ICLP 2023), London, United Kingdom, July 2023, volume 3437 of CEUR
     Workshop Proceedings, CEUR-WS.org, 2023. URL: https://ceur-ws.org/Vol-3437/paper8ASPOCP.
     pdf.
[23] C. Sakama, Possible model semantics for disjunctive databases, in: Deductive and Object-Oriented
     Databases, Elsevier, 1990, pp. 369–383.

</pre>