Approximation fixpoint theory (AFT) is an abstract, algebraic framework for the study of operators and their ifxpoints 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 diferences 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.
Approximation Fixpoint Theory (AFT) [
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. [
However, AFT requires operators to be deterministic and exact. It is incapable of expressing nondeterministic 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 diferent reasoning components together may lead to a conflict, 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 [
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 [
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.
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, duepnpoetrebdoausn⋁d︀s⪯ o(f) ((rreesspp.. agnreuatpepsetrlobwoeurnbdouofndth,edseentootfedalalslo⋀w︀⪯ er(bo)u)nifdist oisf al)o.wAercbomoupnledteoflatthteicese⟨tℒo,f⪯⟩all 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 ifxpoint 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, (, · )1 = (︀ ⇒ ( (, )1)︀) (where (, ) : ℒ2 → ℒ2) This makes it possible to write lfp⪯ (, · )1 to express the ⪯ -least fixpoint of as partially applied with . We use ⪯ () to denote the set ⪯ () := { ∈ | ¬∃′ ∈ , ′ ≺ }.
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
ifxpoints of a stable revision operator. Bi et al. [
First, we define the bilattice on which both original [
Definition 2.1. A (generalized) approximator : ℒ2 → ℒ2 over a complete lattice ⟨ℒ, ⪯⟩ is a ⪯ 2monotone function such that for any element ∈ ℒ if
(, )1 ⪯ (, )2 then (, ) = ((, )1, (, )1)
Traditional AFT [
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 [
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. [
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 [
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 semantics. 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 ifxing 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 [
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 ( ).
2)⟩ and the set , consisting of its a-stable fixpoints, we have
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. [
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 ifxpoint of ⟨, Θ 1⟩, (⊤, ⊤) is not because (ℎ⊥, (⊤, ⊤)) ∈ Θ 1 and (ℎ⊥)(⊤, ⊤) ≺ 2 (⊤, ⊤).
For (⊤, ⊤) to be an a-stable fixpoint, we must remove (ℎ⊥, (⊤, ⊤)) ∈ Θ 1. but this would violate 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.
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.
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 (if ∈ ∧ ∈ ), undefined (if ̸∈ ∧ ∈ ), and f (if ̸∈ ∧ ̸∈ ). This logic leverages two orderings between interpretations, a truth ordering ⪯ 2 and a precision ordering ⪯ 2. Both ordering are obtained from the bilattice on ⟨℘(()), ⊆⟩ . 2 Note that ℘(()) contains inconsistent pairs, i.e., not every pair is an interpretation. The ⪯ 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() ∩ ̸= ∅)
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 = .
Defined by Motik and Rosati [
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 [
In this paper, we focus very little on ontologies and instead treat them as decidable, polynomial ifrst-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
[
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 diference 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 diferentiates between classically false atoms and atoms that are false due to negation as failure. 1We require (, ) to be -consistent to handle the case where = (), in all other cases, it is implied by the principle of explosion. true.
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 MKNF model of named (, ).
-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 (, ) = ({ | 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 [
of all head atoms in the program , i.e., the set (⋃︀∈ head()).
Liu and You [
Γ (, ) := head(satisfied (, )()) Φ (, )1 := Γ (, ) ∪{ | OB, |= } Φ (, )2 := (︁ Γ (, ) ∖ { | OB, |= ¬}
︁) ∪ { | OB, |= } is symmetric for the given pair.
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 ̸= Φ This can result in some stable fixpoints having the property where some rules are not satisfied because (, )2). 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
We lift this approximator to disjunctive HMKNF KBs by defining an a-set paired with the
aforementioned symmetry condition from Liu and You [
Definition 4.4. Let = (, ) be a HMKNF KB. We define ⟨, Θ ⟩, := {Φ (,′) | ′ ∈ normal()} Θ := {(ℎ, (, )) ∈ ( × ℒ 2 ) | ℎ(, ) = (ℎ(, )1, ℎ(, )1) and ( ) := {︁ {ℎ() | ∈ } | ∃ℎ, ∀ ∈ , ∃ ∈ 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 ⟨, Θ ⟩ if 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 { ̸∈ | OB, |= } ̸= ∅, or { ̸∈ | 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. 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 ifxpoint in action. Let = (¬ ∨ ′). The stable fixpoint of (Φ (,)) remains the same, but the stable ifxpoint 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 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 prefixpoint 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. [
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 [
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.
We would like to thank and acknowledge Alberta Innovates and Alberta Advanced Education for their ifnancial support of author one.