Eliminating Unintended Stable Fixpoints in Approximation Fixpoint Theory

Abstract

A wide variety of nonmonotonic semantics can be expressed as approximators defined under AFT (Approximation Fixpoint Theory). Using traditional AFT theory, it is dificult to derive falsity from falsity. However, this type of reasoning is essential for systems that incorporate classical negation into nonmonotonic reasoning. In this work, we introduce a methodology that can better leverage falsity in stable revision to capture a more precise semantics. We show that our framework fits within the theoretical confines of AFT and can be utilized without modifying the existing theory.

Keywords

• eol>approximation fixpoint theory
• answer set programming
• bilattices

1. Introduction

←

Informally, an answer set is a minimal set of atoms such that if a rule’s body (the right side) is satisfied,

then the rule’s head (the left side) is contained in the answer set. Since its head is empty, the constraint ← requires that no answer set contains , and the remaining rules work to set up a “choice” between assigning or to be true. This program has one answer set ({}, {}), which assigns to be true and to be false.

A forward-reasoning approximator, such as the one given by Denecker et al., will ignore the constraint and propagate that both and are possibly true (but not necessarily true)1. That is, the interpretation 23rd International Workshop on Nonmonotonic Reasoning, November 11-13, 2025, Melbourne, Australia * Corresponding author. $ [e-mail] (S. Killen); [e-mail] (J. You) € https://sjkillen.ca (S. Killen) 0000-0003-3930-5525 (S. Killen); 0000-0001-9372-4371 (J. You)

© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

1Note that Denecker et al.’s approximator was not designed with constraints in mind. (∅, {, }) that assigns both and to be unknown, is a stable fixpoint. This overly cautious interpretation approximates both ({}, {}) and ({}, {}). Because ({}, {}) is not an answer set, the approximator need not consider it when answer sets are the intended semantics. If we wish to remove the unintended stable fixpoint (∅, {, }), our approximator must leverage backward-reasoning to conclude that is false.

Deceptively so, it appears like we can accomplish this with a simple modification: our approximator must not derive atoms that would satisfy the body of a constraint. However, this approach quickly falls apart when we add some layers of indirection. For example, let us change the constraint to use a new atom and add an additional rule ← .

← ← This program is similar to in that ({}, {}) is the only answer set, however, multiple steps of reasoning are required to conclude that must be false. A reasoning step must conclude that is false (from ← ) for a subsequent reasoning step to conclude that is false (from ← ). Constructing the appropriate approximator is challenging because there is no mechanism to access which atoms were false at the invocation of stable revision. If we invoke the stable operator with an interpretation (, ), the complement of contains the atoms that are false. Yet, the computation of lfp (, · )2, which determines the atoms that are false, has no access to this information.

When stable revision is used for iterative construction, each iteration more atoms with an unknown truth value are assigned a value of either true or false. However, in each iteration, the underlying approximator “forgets” which atoms it assigned false. Thus, from the approximator’s perspective, any atom may become true. In actuality, atoms that are assigned false will remain false on subsequent iterations due to monotonicity.

The primary contribution of this work is a formulation of stable revision that can incorporate false information in its reasoning to conclude that more atoms are false. Surprisingly, our extension does not require a new theory. We simply modify the underlying bilattice on which the approximators operate. As a result, the theory can be easily adopted to extend existing approximators. Our framework can help eliminate unintended stable fixpoints for a semantics if removing these fixpoints requires the propagation of false information.

We are motivated by our approximator defined for hybrid MKNF knowledge bases [ 4 ]. In this work, we formalize a general theory for the approximator defined there. For simplicity, and as a testament to the generality of our theory, we limit our focus to non-disjunctive logic programs with constraints. They serve well as a proxy for hybrid systems with falsity propagation. A hybrid MKNF knowledge base [5] pairs an ontology with a logic program . The ontology is a decidable fragment of first-order logic, thus = ¬ is semantically similar to a rule ← in that it rules out all models with to be true. With the additional reasoning power, our approximator expanded the class of known knowledge bases with polynomial-computable well-founded models [ 4 ].

We organize the paper as follows. Section 2 details lattice theory and the notation adopted throughout this work, Section 2.1 covers approximators and stable revision as used in this work, and Section 2.2 introduces logic programming. In Section 3, we begin by providing an illustrative example and a sketch of a solution. The next subsection expands upon these ideas by formalizing recurrent approximators, approximators defined over a tetralattice, a bilattice formed from a bilattice. These operators operate on 4-tuples (pairs of pairs) and provide a theoretical backing on AFT with an extra parameter of pairs. In Section 4 we ofer an additional use for recurrent approximators by describing how they can be used to make approximators increasing/decreasing. Finally, we wrap up and discuss in Section 5.

2. Preliminaries

We summarize common theory of lattices [6] to establish the notation used throughout this work. A poset ⟨, ⪯ ⟩ is a relation ⪯ over a set of elements that satisfies: reflexivity (∀ ∈ , ⪯ ), transitivity (∀, , ∈ , having both ⪯ and ⪯ implies ⪯ ), and antisymmetry (∀, ∈ , if ⪯ and ⪯ then = ). We refer to a poset ⟨, ⪯ ⟩ simply by when ⪯ is clear from context. Given a poset , 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 () (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 poset ⟨ℒ, ⪯ ⟩ is a complete lattice if every subset ⊆ ℒ has a least upper bound and a greatest lower bound. For a complete lattice ⟨ℒ, ⪯ ⟩ we denote (ℒ) as ⊥⪯ and (ℒ) as ⊤⪯ when ℒ is clear from context or simply as ⊥ and ⊤ when the relation is unambiguous. An operator over a complete lattice ⟨ℒ, ⪯ ⟩ is a function () : ℒ → ℒ. The operator is ⪯ -monotone (resp. ⪯ -antitone) if ∀, ∈ ℒ whenever ⪯ we also have () ⪯ () (resp. () ⪯ ()). An operator is ⪯ -monotone increasing (resp. decreasing) if ∀, ⪯ () (resp. ∀, () ⪯ ). An element of a complete lattice ∈ ℒ is a fixpoint of an operator if () = . The set of all fixpoints of a ⪯ ℒ-monotone operator on a lattice ⟨ℒ, ⪯ ℒ⟩ forms a complete lattice [7]. We call the greatest lower bound of this lattice the least fixpoint and denote it as lfp . This element can be constructed by iteratively applying to ⊥⪯ ℒ . We denote the cartesian ⪯ ℒ product of two sets and with × or 2 if = . , that is, × := {(, ) | ∈ , ∈ }

2 := {(, ) | ∈ , ∈ }

Given a lattice ⟨ℒ, ⪯ ℒ⟩, its induced bilattice [1] consists of the two complete lattices ⟨ℒ2, ⪯ 2⟩

and ⟨ℒ2, ⪯ 2 ⟩. These are the lattices formed from the two orderings ⪯ 2 and ⪯ 2 such that for each , , , ∈ ℒ • (, ) ⪯ 2 (, ) if ⪯ ℒ and ⪯ ℒ (the precision-ordering) • (, ) ⪯ 2 (, ) if ⪯ ℒ and ⪯ ℒ (the truth-ordering)

We denote the powerset of a set , as ℘(). We use subscript notation to denote the projection of particular components of a tuple, for example, given an operator (, ) : ℒ2 → ℒ2, we have (, ) = ((, )1, (, )2) and (, )2,1 = ((, )2, (, )1). We create partial functions by using a “· ” in place of arguments to be filled in, that is, for an operator (, ) : ℒ2 → ℒ2, we write (· , ) (resp. (, · )) to mean . (, ) (resp. . (, )). Naturally, if a “· ” is used within a function application that is then projected, the projections are included within the body of the lambda abstraction For example, (, · )1 = . ( (, )1) (where (, ) : ℒ2 → ℒ2) This makes it possible to write lfp ⪯ ℒ (, · )1.

For convenience and ergonomics, we may write 4-tuples as a pair of 2-tuples or as a tuple with four members. As a general rule, we consider two tuples to be equivalent if they are equal when all nested tuples are “flattened”. For example, the following equivalences hold.

ℒ4 = ℒ2 × ℒ (, , , ) = ((, ), (, ))

2 = (ℒ2)2 ((, ), (, )) = (, , , ) 2.1. Approximation Fixpoint Theory Approximation fixpoint theory (AFT) was first defined by Denecker et al. [ 1 ] to provide a uniform ifxpoint characterization of a multitude of nonmonotonic semantics. This work adopts the generalized framework of AFT described by Liu and You [8]. This theory can be viewed as a relaxation of AFT. Rather than ensuring that stable fixpoints are always consistent, inconsistent stable fixpoints are permitted. One can provide an additional condition to deterimine whether a stable fixpoint is intended (e.g. it must be consistent).

We introduce the definitions of approximators and stable revision.

Definition 1. ⟨ℒ2, ⪯ 2⟩

An approximator is a ⪯ 2-monotone operator (, ) : ℒ2 → ℒ2 on the complete lattice

Traditional AFT [ 1 ] requires some additional properties on approximators, including exactness, symmetry, or consistency. Following Liu and You [8], we do not impose any of these requirements. Definition 2.

Given an approximator : ℒ2

→ ℒ2, we can construct its stable revision operator (). : (︁ ℒ 2 → ℒ ⪯ ℒ 2 ︁)

2 → ℒ → ℒ

2 ()(, ) := (lfp ((· , )1), lfp ⪯ ℒ ((, · )2)) revision is well-defined.

For an approximator , we refer to fixpoints of () as stable fixpoints . Since the operator is ⪯ 2

monotone, it is easy to check that both operators (· , )1 and (, · )2 are ⪯ ℒ-monotone, so stable

To apply AFT to a semantics is to characterize the intended models as stable fixpoints. If there are stable fixpoints that do not correspond to the intended semantics, we say they are unintended stable ifxpoints. Such fixpoints are unavoidable in hybrid reasoning systems[ 8]. They may also appear due to an inability to capture intended semantics (e.g. the intended semantics is super-polynomial but a polynomial approximator is desired).

It is desirable to have fewer unintended stable fixpoints. Ultimate approximation theory [ 9] embodies this ideal by ordering approximators by their ability to capture the intended stable fixpoints. However, climbing this ordering may introduce additional unintended exact stable fixpoints. 2.2. Logic Programming A logic program is a set of rules formed by if/then constraints. Most logic programming semantics seek a truth-minimal assignment to atoms appearing in the program such that every rule is satisfied. Here, we introduce Przymusinski’s [10] extension of answer set semantics, a language which only allows a single atom in the head of each rule and the bodies of rules can leverage negation as failure. Additionally, we allow for integrity constraints.

For a logic program , each rule ∈ consists of a head, a set containing at most one atom, denoted ℎ(), and a set of possibly negated atoms called its body, denoted (). A ℎ ← rule with the parts ℎ() = {ℎ} and () = {1, . . . , , 1, . . . , } is written as 1, . . . , , 1, . . . , . Rules with empty heads are called integrity constraints and are written as above with ℎ omitted. For a program, , we use () to capture the set of such rules, that is, () = { | ∈ , ℎ() = ∅}. For a rule , we also define +() := {1, . . . , } and − () := {1, . . . , } to extract the positive body and the negative body of the rule. Note that the elements in − () are atoms rather than negated atoms. Without loss of generality, we do not consider logic programs with variables.

An interpretation of a logic program is a true/false/unknown assignment to every atom that appears in . If the assignment does not use the value unknown, then it is two-valued and represented as the set of true atoms. Otherwise, the interpretation is three-valued and represented by a pair of sets (, ) such that ⊆ , the set contains the atoms that are true, and contains the atoms that are not false. Every two-valued interpretation has an equivalent three-valued interpretation (, ). The valuation (, )() for an atom w.r.t. an interpretation (, ) is given as follows. (, )() := ⎪ ⎨ ⎧ () ( ) if ∈ ∩ if ̸∈ ∪ ⎪⎩ () if ̸∈ , ∈ () denoting the set containing all atoms appearing in a logic program , The orderings ⪯ 2 and ⪯ 2 defined earlier are extended to interpretations using the underlying ordering ⊆ . These order the interpretations based on the individual valuations of each atom [11]. That is, with (, ) ⪯ 2 ( ′, ′) if ∀ ∈ (), (, )() ⪯ ( ′, ′)() (, ) ⪯ 2 ( ′, ′) if ∀ ∈ (), (, )() ⪯ ( ′, ′)() where ⪯ ⪯ , ⪯ , and ⪯ . The ordering ⪯ 2 is used to minimize truth while ⪯ 2 measures the proximity to a two-valued interpretation. Treated as an interval, an interpretation (, ) contains all two-valued interpretations related by ⪯ 2. That is,

⊆ ⊆ ⇐⇒ (, ) ⪯ 2 (, )

We use the following to relate rules and interpretations by describing the set of rules whose bodies are satisfied by an interpretation.

(, )() := { ∈ | +() ⊆ , − () ∩ = ∅} We use ℎ() to denote {ℎ() | ∈ } for a set of rules .

Przymusinski [10] extends Gelfond and Lifschitz’s [12] answer set semantics to three-valued interpretations. We adopt our own definition due to its close proximity to fixpoint operators [13]. Definition 3.

We call an interpretation (, ) a model of a logic program if

(ℎ((, )()), ℎ((, )())) ⪯ 2 (, ) We say an interpretation ( ′, ′) models the reduct of w.r.t. (, ) if

(ℎ(( ′, )()), ℎ(( ′, )())) ⪯ 2 ( ′, ′) A model (, ) of a logic program is a partial stable model of if there does not exist ( ′, ′) ≺ 2 (, ) s.t. ( ′, ′) models of the reduct of w.r.t. (, ).

Przymusinski [14] shows that partial stable models are faithful to Gelfond and Lifschitz’s answer set semantics [15].

3. Recurrent Approximators

During the computation of stable revision, the underling approximator cannot access the information passed to invoke the stable operator. That is, ()(, )2 cannot be based on . This makes perfect sense given that stable revision removes circular justifications. If ()(, )2 were to introduce conclusions based on atoms in , that would undoubtedly introduce circular reasoning. However, this rationale only holds for positive conclusions. Concluding that an atom should not be in ()(, )2 based on the atoms that are not in can be perfectly valid. This type of reasonig is not possible in AFT. In this section, we demonstrate this limitation and then we introduce an extension of AFT to remedy it. 3.1. An Illustrative Sketch First, return to the example presented in the introduction. We focus on constraints in answer set programming due to their simplicity. A constraint ← can alternatively be represented as a rule ← , . Adopting this representation is possible and straightforward, however, it would only make the coming examples more dificult.

We define the following set of rules.

← ← This program has two partial stable models: (∅, {, }) and ({}, {}). The interpretation ({}, {}) is not a partial stable model because it violates the integrity constraint ← .

Suppose our intended semantics is just the answer sets (the two-valued partial stable models). Eliminating (∅, {, }) as a stable fixpoint is a welcome improvement because it cannot be extended to an answer set, but we cannot remove every stable fixpoint that is not an answer set [9].

We introduce Denecker et al.’s approximator for capturing partial stable models of a program .

Γ (, ) := (ℎ((, )()), ℎ((, )())) Recall that we use ℎ((, )()) to denote {ℎ() | ∈ (, )()}. We have lfp Γ (∅, · )1 = ∅ and lfp Γ (· , {, })2 = {, }. Thus, (∅, {, }) is a stable fixpoint of Γ . Because this approximator was not constructed to support integrity constraints, both ({}, {}) and ({}, {}) are also stable fixpoints.

Let us define a modified version that prevents the derivation of atoms that would satisfy constraints. Γ ′ (, )1 := Γ (, )1 Γ ′ (, )2 := Γ (, )2 ∖ ′ (, )

′ (, ) := { ∈ () | ∃′ ∈ (), ′ ∈ ( ∪{}, ))}

Recall that in (, ) the set is used to evaluate positive atoms in rules and to evaluate negated atoms (e.g. ). Intuitively, the set (, ) is the set of atoms that, if true, would satisfy a constraint. For example, with the constraint ← , , we have ∈ ({}, {, }). Thus, if there were another rule ← , the atom would not be derived in Γ ({}, {, })2. Clearly, as an interpretation (, ) becomes more precise, the set (, ) grows. Because these atoms are extracted from , the function Γ ′ is ⪯ 2-monotone (our only requirement for it to be an approximator). Note that if an interpretation (, ) satisfies some constraint in , then (, ) = (). Thus, inconsistent stable fixpoints, which are not possible in traditional AFT [ 1 ], are possible. Using the generalized AFT of Liu and You [8], we can tolerate inconsistent pairs2.

While we have succeeded in removing the stable fixpoint (∅, {, }) for the small program, our approximator Γ ′ (, ) does not hold up for programs where falsity propagation must be performed over multiple rules. Take the following program to be , which modifies the constraint in the other program to use a new atom and adds an additional rule ← .

← ← ← Because the third rule is not satisfied by (∅, {, }), it is not a model of the program (and thus not a partial stable model). However, it is a stable fixpoint of both Γ and Γ ′. While our modified approximator Γ ′ does block the derivation of , it only blocks constraints, thus, it does not block .

Let us modify Γ ′ so that all rules, and not just constraints, are a part of the backward-chaining. Ω (, )1 := Γ (, )1 Ω (, )2 := Γ (, )2 ∖ Ω(, )

Ω(, ) := { ∈ () | ∃′ ∈ , ℎ(′) ∩ = ∅, ′ ∈ ( ∪{}, ))} Intuitively, Ω functions identically to Γ ′, except it also blocks atoms in the bodies of rules whose heads are false (they do not appear in ). As expected, ({}, {, }) = {, } and Ω ({}, {, }) = ({}, {}). This is, given that is false, we conclude that must also be false. The interpretation ({}, {}) is a fixpoint of Ω (a requirement for it to be a stable fixpoint of Ω ). We show below that Ω can be used to construct the partial stable model ({}, {}). (∅, ()) = {}

Ω (∅, ()) = (∅, {, }) (∅, {, }) = {, } (∅, {}) = {, } Ω (∅, {, }) = (∅, {}) Ω (∅, {}) = ({}, {}) (No rule to derive ) ( is blocked) (With false, can be true)

While approximators can compute some partial stable models, stable revision is required to eliminate cyclic justifications. However, the stable operator of Ω does not behave as expected. 2In practice, this requires pairing stable fixpoint checking with an additional condition to verify an intended model. Here, we can verify stable fixpoints as partial stable models by checking that they are consistent.

To compute the least stable fixpoint of Ω , we begin with (∅, ()), the interpretation that assigns all atoms to be unknown.

(Ω )(∅, ()) = (lfp Ω (· , ()), lfp Ω (∅, · )) Ω (∅, ())1 = ∅ Ω (∅, ∅)2 = Γ (∅, ∅)2 ∖ Ω

(∅, ∅) Γ (∅, ∅)2 = {, } Ω

(∅, ∅) = {, } (Ω )(∅, ∅)2 = {, } ∖ {, } = ∅ (fixpoint ) (fixpoint ) Thus, the least stable fixpoint is (∅, ∅). Due to ⪯ 2-monotonicity and (∅, ()) ⪯ 2 ({}, {}), we can conclude that ({}, {}) is not a stable fixpoint. This can also be easily worked out by hand. Clearly, this approximator does not capture our intended semantics! If we analyze the approximator, it becomes clear that we cannot trust the atoms that are not in to be false. In a constructive computation of (Ω )(, )2, stable revision first “resets” to ∅, thus Ω(, ) will treat every atom as false! Note that while is used in two places in Ω, and we only demonstrated issues with one, both are problematic.

It seems impossible to formulate so that it is powerful enough to perform false backwardchaining. We remedy this issue by introducing a meta operator Φ . When used inside an approximator, Φ has the same value as . When used in stable revision, Φ has the value of that was passed to the stable operator.

We modify Ω to formulate a new operator Γ ′′ by replacing Ω with the following. ′′ (, ) := { ∈ () | ∃′ ∈ , ℎ(′) ∩ Φ = ∅, ′ ∈ ( ∪{},Φ ))} Now, when we compute our least stable fixpoint for Γ ′′ , we get our stable model ({}, {}). (Γ ′′ )(∅, ()) = (lfp Γ ′′ (· , ())2, lfp Γ ′′ (∅, · )2) Γ ′′ (∅, ())1 = ∅ Γ ′′ (∅, ∅)2 = Γ (∅, ∅)2 ∖ ′′ (∅, ∅) Γ (∅, ∅)2 = {, }

Φ = {, , } ′′ (∅, ∅) = {}

Γ ′′ (∅, ∅)2 = {, } ∖ {} = {, } No longer is (∅, ∅) the least stable fixpoint. When we continue the computation of (Γ ′′ )(∅, ()) with (∅, {, }), it is critical that Φ remains as {, , }. With Φ = {, }, that is, with removed, we have ′′ (∅, {, }) = {} and Γ ′′ (∅, {, })2 = {}. Thus, if we update Φ in this way, the function Γ ′′ (∅, · )2 is not monotone and the stable operator is not well-defined.

After we have computed (Γ ′′ )(∅, ()) to be (∅, {, }) we can apply (Γ ′′ ) again with the more precise interpretation (∅, {, }) to use Φ = {, }.

′′ (∅, {, }) = {, } Γ ′′ (∅, {, })2 = {} Γ ′′ (∅, {})2 = {} (fixpoint)

While Φ seems to have solved the issues with Ω , its introduction raises many questions. The introduction of this operator appears to be a significant deviation from AFT. How do we determine if a recurrent approximator is ⪯ 2-monotone? What is the relationship between fixpoints and stable ifxpoints? Do stable fixpoints still exist? To address these questions, we show that Φ fits within the existing AFT theory. Thus, any recurrent approximator can be expressed as an approximator which does not use Φ . Due to this relationship, the properties of AFT continue to hold for recurrent approximators. 3.2. A Formalization of Φ We have shown that making inferences based on false information is limited in stable revision, and we have provided a sketch which extends the stable revision operator with an operator to access false information so that it can be incorporated safely in reasoning. We formalize this operator by establishing a larger complete lattice for approximators to operate on. Intuitively, this lattice is formed by taking the bilattice of the bilattice to form a tetralattice. The additional data in each element is used to store Φ .

For simplicity and throughout the remainder of this work, we assume that every complete lattice ⟨ℒ, ⪯ ℒ⟩ has a complement operation, denoted as c, that satisfies the following two properties . ∀ ∈ ℒ, (c)c =

. ∀, ∈ ℒ, ⪯ ℒ ⇐⇒ c ⪯ ℒ c Not every lattice has such a complement operation, thus it appears limiting, however, this operation is not necessary to apply our theory. We rely upon it only for simplicity. One can instead define orderings diferently so that the criteria of the complement is satisfied.

We intend to isolate a family of approximators defined on a “bilattice formed from a bilattice” that can be used to propagate information from the stable operator to the approximators within. First, we formally describe this lattice.

Definition 4. Given a complete lattice ⟨ℒ, ⪯ ℒ⟩ we construct its bilattice ⟨ℒ2, ⪯ 2 ⟩, ⟨ℒ2, ⪯ 2⟩, and then we define the following pair of complete lattices which we refer to collectively and individually as a tetralattice.

⟨ℒ4, ⪯ 4 ⟩, ⟨ℒ4, ⪯ 4⟩ A tetralattice is the bilattice formed from turning ⟨ℒ2, ⪯ 2 ⟩ into a bilattice. The orderings ⪯ 4 and ⪯ 4 are naturally defined. For the ordering ⪯ 4 and any two 4-tuples ( , , , ), ( ′, ′, ′, ′) ∈ ℒ4, the following three expressions are equivalent • (( , ), (, )) ⪯ 4 (( ′, ′), ( ′, ′)), • ( , ) ⪯ 2 ( ′, ′) ∧ (, ) ⪯ 2 ( ′, ′), and • ⪯ ℒ ′ ∧ ⪯ ℒ ′ ∧ ⪯ ℒ ′ ∧ ⪯ ℒ ′ For ⪯ 4, the following are equivalent • (( , ), (, )) ⪯ 4 (( ′, ′), ( ′, ′)), • ( , ) ⪯ 2 ( ′, ′) ∧ ( ′, ′) ⪯ 2 (, ), • ( , ) ⪯ 2 ( ′, ′) ∧ (, ) ⪯ 2 ( ′, ′), and • ⪯ ℒ ′ ∧ ⪯ ℒ ′ ∧ ′ ⪯ ℒ ∧ ′ ⪯ ℒ

We take the process applied to ⟨, ⪯ ℒ⟩ to obtain ⟨ℒ2, ⪯ 2 ⟩ and ⟨ℒ2, ⪯ 2⟩, then we apply it to the

lattice ⟨ℒ2, ⪯ 2 ⟩. The result is a pair of complete lattices because bilattices are complete lattices [16]. The element of a pair will be used to carry false information, that is, the complement of . We symmetrically define to carry information that is not true, however, does not seem as useful as and our approximators for logic programs do not make use of 3. Most of the approximators defined on the full tetralattice lattice are of no interest here. Thus, we restrict our attention to the approximators which have a complementary relationship between and (also and ). We use the notation 2,3 to project multiple elements from a tuple (e.g. (, , , )2,3 = (, )).

Definition 5. A recurrent operator ( , , , ) : ℒ4 → ℒ4 is an operator on the tetralattice ℒ4 with the inner components fixed such that the following equivalence is satisfied.

( , , , )2,3 = (︀ c, c)︀ We call ⪯ 4-monotone recurrent operators recurrent approximators. 3In Section 4, we make use of to define meta approximators. (⊥⪯ 2 , ⊤⪯ 2 ).

By restricting the class of approximators, we ensure that is a carrier of false information. We complement the information so that we can adopt the same orderings of AFT.

Note that (, , , )2,3 is of type 4 → 2. To construct a recurrent operator, we only need to

define (· , · , · , · )1,4, a traditional approximator that additionally receives an older computation of and (in complement form) and returns a new approximation ( ′, ′). The utility of these additional arguments is not fully apparent until they are embedded in the stable revision operator.

The least element of the lattice ⟨ℒ4, ⪯ 4⟩ is the pair ((⊥ℒ, ⊥ℒ), (⊤ℒ, ⊤ℒ)) which is equivalant to

Example 2. All approximators in AFT can easily be converted to a recurrent approximator. Let : ℒ2 → ℒ be an approximator over ⟨ℒ2, ⪯ 2⟩. We define a recurrent approximator * : ℒ4 → ℒ4 2 This approximator does not make use of or , thus for any (, ) ∈ ℒ2 and , ∈ ℒ * (, , , )1 := (, )1 * (, , , )2 := c * (, , , )3 := c * (, , , )4 := (, )2 (, ) = * (, , , )1,4

Due to its underlying structure (an approximator formed from a bilattice), a recurrent approximator is required to be ⪯ 4-monotone. Because the inner components of the approximator are fixed, we can simplify the process of checking whether a recurrent approximator is monotone. ( ′ c, ′ c).

Lemma 1. For a tetralattice ⟨ℒ4, ⪯ 4⟩, a recurrent operator (, , , ) is ⪯ 4-monotone if for each (, , , ), ( ′, ′, ′, ′) ∈ 4 s.t. (, , , ) ⪯ 4 ( ′, ′, ′, ′), we have (, , , )1,4 ⪯ 2 ( ′, ′, ′, ′)1,4 Proof. (⇒) trivial.

(⇐) It’s suficient to show (, , , )2,3 ⪯ 2 ( ′, ′, ′, ′)2,3. We have (, , , )2 = c and and ( ′, ′, ′2,=′)3 ′ =c. Cle′ca.rlyFrsoinmce ′⪯ ⪯ ℒℒ′,, wwee hhaavveec′ c⪯ ⪯ℒ ℒ ′c.cW.eWheavcoenc(lu,de,(, c, )3c=) ⪯ c ( ′, ′, ′, ′) 2

When defining a new recurrent approximator, we need only focus on the / components in the image when proving monotonicity.

We can now rebuild Γ ′′ from Section 3.1 and show that it is ⪯ 4-monotone. First, we need the

appropriate lattice for interpretations.

Definition 6. A powerset tetralattice ⟨℘(ℒ)4, ⪯ 4⟩ is the tetralattice formed from a powerset lattice ⟨℘(ℒ), ⊆⟩ using c = ℒ ∖ as the complement operation.

Example 3. Define Γ ′′′ as follows.

Γ ′′′(, , , )1 := Γ (, )1 Γ ′′′(, , , )4 := Γ (, )2 ∖ ′′′(, )

′′′(, ) := { ∈ () | ∃′ ∈ , ℎ(′) ⊆ , ′ ∈ ( ∪{}, c))} As Γ ′′′ is a recurrent approximator, Γ ′′′(, , , )2,3 is fixed. As (, , , ) becomes more precise w.r.t.

⪯ 4, the sets and grow. With a larger and , there is more opportunity for a rule s.t. ℎ(′) ⊆ and ′ ∈ ( ∪{}, c). Thus, ′′′(, ) also grows. It follows that Γ ′′′(, , , )4 shrinks 2 and then that Γ ′′′(, , , )1,4 is monotone from ⪯ 4 to ⪯ . With Lemma 1, we can conclude Γ ′′′ is ⪯ 4-monotone.

Now that we’ve established approximators that can capture Φ , it remains to show that stable revision works as expected. Because recurrent approximators are approximators over the lattice ⟨ℒ2, ⪯ 2 ⟩, stable revision is already defined. For convenience, we repeat the definition of the stable revision operator using the tetralattice.

: ︁( ℒ 4 → ℒ 4 ︁)

4 → ℒ → ℒ

4 ()( , , , ) := (lfp⪯ 2 ((· , (, ))1,2), lfp⪯ 2 ((( , ), · )3,4))

The stable operator is itself a recurrent approximator.

Proposition

1. For a recurrent approximator ,

()( , , , )2,3 = ( c, c). we have that () is ⪯ 2-monotone and ( , , , ) ∈ ℒ4. The functions (· , (, ))2 and (( , ), · )3 are constant, therefore Proof. We show (i) that () is a recurrent operator and then (ii) that () is ⪯ 4-monotone. (i) Let ()( , , , )2,3 = (ℒ ∖ , ℒ ∖ ) suficient to show (ii) By [7] and [ 1 ] the () operator is well-defined, that is, has fixpoints that exist when is monotone. Let ( , , , ), ( ′, ′, ′, ′) ∈ 4 such that ( , , , ) ⪯ 4 ( ′, ′, ′, ′). It is (a) lfp⪯ 2 ((· , (, ))1,2) ⪯ 2 lfp⪯ 2 ((· , ( ′, ′))1,2) (b) lfp⪯ 2 ((( ′, ′), · )3,4) ⪯ 2 lfp

⪯ 2 ((( , ), · )3,4) (a) Let = lfp⪯ 2 ((· , ( ′, ′))1,2). By the ⪯ 4-monotonicity of , we have

(, (, )) ⪯ 2 (, ( ′, ′)) it is a recurrent approximator.

Here, is a prefixpoint of (· , (, )). lfp⪯ 2 ((· , (, ))1,2) corresponds to the least prefixpoint of [7], thus lfp⪯ 2 ((· , (, ))1,2) ⪯ 2 . A nearly identical procedure can be used to show that lfp⪯ 2 ((( ′, ′), · )3,4) ⪯ 2 lfp⪯ 2 ((( , ), · )3,4). We conclude that () is ⪯ 4 monotone and with (i)

Least fixpoints can be computed by repeated application of an operator on the least element. We have the following: and with the ⪯ 4-monotonicity of , we have (lfp⪯ 2 ((· , (, ))1,2), lfp⪯ 2 ((( , ), · )3,4)) ⪯ (lfp⪯ 2 ((· , ( ′, ′))1,2), lfp⪯ 2 ((( ′, ′), · )3,4))

4 (⊥⪯ ℒ , ⊥⪯ ℒ , , ) ⪯ 4 (⊥⪯ ℒ , ⊥⪯ ℒ

, ′, ′) ( , , ⊥⪯ ℒ , ⊥⪯ ℒ ) ⪯ 4 ( ′, ′, ⊥⪯ ℒ , ⊥⪯ ℒ

) (⊥⪯ ℒ , ⊥⪯ ℒ , , )1,2 ⪯ 2 (⊥⪯ ℒ , ⊥⪯ ℒ

, ′, ′)1,2 ( ′, ′, ⊥⪯ ℒ , ⊥⪯ ℒ )2,3 ⪯ 2 ( , , ⊥⪯ ℒ , ⊥⪯ ℒ )2,3 With the ⪯ 4-monotonicity of , this relation continues to hold when we reapply the operator inductively: ((⊥⪯ ℒ , ⊥⪯ ℒ , , )1,2, , ) 1,2 ⪯ 2 ((⊥⪯ ℒ , ⊥⪯ ℒ , ′, ′)1,2, ′, ′) 1,2 ( ′, ′, ( ′, ′, ⊥⪯ ℒ , ⊥⪯ ℒ )3,4)3,4 ⪯ 2 ( , , ( , , ⊥⪯ ℒ , ⊥⪯ ℒ )3,4)3,4 We conclude the following

lfp⪯ 2 ((· , (, ))1,2) ⪯ 2 lfp⪯ 2 ((· , ( ′, ′))1,2) lfp⪯ 2 ((( ′, ′), · )3,4) ⪯ 2 lfp⪯ 2 (((, ), · )3,4)

We now return to our example this time to compute the least stable fixpoint.

Example 4. Let be our program from before.

← ←

Using Γ ′′′ from Example 3, we begin to compute its least stable fixpoint, beginning with the least element

(∅, ∅, (), ()). Note that for this element = c and = c. (Γ ′′′)(∅, ∅, (), ()) = (︀ (lfp Γ ′′′(· , · , (), ()))1,2, ︀) (lfp Γ ′′′(∅, ∅, · , · )3,4 Because the first component is computed by Γ and the second component is c, we have lfp Γ ′′′(· , · , (), ()))1,2 = (∅, ()c)

Now for the other side,

lfp Γ ′′′(∅, ∅, · , · )3,4 = (∅c, {, }) Because Φ is empty ( here), we derive and to be unknown as normal. Our resulting four pair is (∅, ∅, (), {, }). However, on the next iteration of stable revision, will be updated. That is, (Γ ′′′)((∅, ∅, (), {, }))2 = {, }c = {} of .

The other components remain unchanged. Now that = {}, our approximator can block the derivation

After several more iterations, we obtain the least stable fixpoint.

(Γ ′′′)((∅, {}, (), {, }))4 = {} (Γ ′′′)(({}, {, }, {}c, {}))1,4 = ({}, {})

We have defined approximators with enhanced stable revision that can leverage false information computed on previous iterations. Because our developments exist within the confines of AFT, that is, every recurrent approximator is an approximator, it has the properties of an approximator. 4. Increasing/Decreasing Approximators Despite both utilizing fixpoint operators, AFT semantics and traditional fixpoint semantics are not always compatible. For example, the solver we define for hybrid MKNF knowledge bases [ 17] performs all of its propagation using a fixpoint operator. In order for the solver to function correctly, this operator must be increasing, that is, Γ * can be defined such that the following holds.

(, ) := (Γ * (, )1 ∪ , Γ * (, )2 ∪ ) While this holds for approximators when applied to pairs that are postfixpoints, a solver must occasionally select some unknown atoms and assign them a value of true or false. The stable revision operator may “revert” these assignments which is undesirable, thus a stable revision operator is not increasing.

We say that an approximator is increasing (resp. decreasing) if every pair (, ) is a postfixpoint (resp. a prefixpoint), that is, (, ) ⪯ 2 (, ) (resp. (, ) ⪯ 2 (, )). Another use for recurrent approximators is a method to turn any approximator into an increasing/descreasing approximator.

Given an approximator : ℘(ℒ2) → ℘(ℒ2), we define variants which are increasing and decreasing,

which we denote as + and − respectively.

+(, , , )1,4 := (︁ ((, )1 ∪ c), ((, )2 ∖ ))︁ − (, , , )1,4 := (︁ ((, )1 ∩ ), ((, )2 ∪ c))︁

Both + and − are recurrent approximators. As an example, if we apply +(, c, c, )1,4, we get ((, )1 ∪ , (, ) ∩ ) which is ⪯ 2-increasing.

Their stable operators are also ⪯ 2-increasing.

Lemma 2. For an approximator (, ) : ℘(ℒ2) → ℘(ℒ2), we have for any pair (, ) (, ) ⪯ 2 (+)(, c, c, )1,4 (− )(, c, c, )1,4 ⪯ 2 (, )

With this, we can repeatedly invoke a stable operator to obtain more precise pairs. We’ve limited the theory above to approximators over the powerset lattice, however, its straightforward to extend it to recurrent approximators over any tetralattice.

The approximator + can be interleaved with any other propagation method within a solver without the worry that a fixpoint will not be reached. In Algorithm 1 below, we briefly sketch a solver that uses Γ ′′′ to find two-valued answer sets of a program . Given an interpretation (, ), the algorithm will attempt to extend it to a two-valued answer set of . It uses the increasing stable revision operator to reduce the search space.

5. Discussion

We have introduced recurrent approximators, a new type of approximator that can leverage additional false information during stable revision. This formalizes the approximators used in our prior work for Algorithm 1 A solver for normal programs with constraints Require: , ∈ ℒ, ⊆ while (Γ ′′′)(, c, c, )1,4 ̸= (, ) do

while ∃ ∈ (), (, )() = do ( ′, ′) ← ((), ∅) while ( ′, ′) ̸= (, ) do ( ′, ′) ← (, ) (, ) ← (Γ ′′′+)(, c, c, )1,4 end while if ∃ ∈ (, )() ∩ () then

backtrack choice or report no answer set. else

choose some where (, )() = to be or end if end while backtrack choice or report no answer set. end while

Terminate: (, ) is an answer set

◁ Use increasing stable revision hybrid MKNF knowledge bases [ 4 ]. The simplicity of this approach is surprising, as approximation ifxpoint theory does not need to be modified to support the technique. As a result, other semantics defined with approximators could be extended to define more precise variations using our method. More uses of recurrent approximators remain to be discovered.

Given that the propagations are well-founded, the technique could allow AFT treatment of grounding procedures. This would be interesting for hybrid MKNF knowledge bases in particular, which have not received a thorough investigation of grounding techniques. For hybrid MKNF knowledge bases, compuing the well-founded model is intractable [18]. In our prior work, we applied recurrent approximators to identify a larger class of polynomial computable well-founded models [ 4 ]. Such has implications for grounding. The ability to perform further propagation with false information can likely be applied to other hybrid reasoning systems such as DL-programs [19] or HEX [20], both of which have received treatment by AFT.

We’ve shown that recurrent approximators can be made ⪯ 2-monotone. The + operator bears some resemblance to stable revision in consistent AFT, which limits the image of ()(, ) s.t. ()(, ) ⪯ 2 (, ). The relationship between consistent and traditional AFT is not yet fully understood. It has been shown that, for nonsymmetric approximators, the stable fixpoints are not the same for stable revision and consistent stable revision [21]. We believe that recurrent approximators could play a role in further understanding this relationship because of their ability to limit a stable operator s.t. ()(, ) ⪯ 2 (, ).

Various techniques in answer set solving involve backward-chaining. The recent s(CASP) system [22] blends forward- and backward-reasoning for answer set programming. Additionally, SAT-solver style answer set solvers, such as Clingo [23], use a variety of backward-chaining techniques to perform constraint propagation. It would be interesting to see if these approaches could be characterized using recurrent AFT.

Acknowledgments

Spencer Killen was partially supported by Alberta Innovates and Alberta Advanced Education.

Declaration on Generative AI

The authors have not employed any Generative AI tools.

References

[1] 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 .

[2] L. Vanbesien , M. Bruynooghe , M. Denecker, Analyzing semantics of aggregate answer set programming using approximation fixpoint theory, Theory Pract . Log. Program. 22 ( 2022 ) 523 - 537 . doi: 10 .1017/S1471068422000126.

[3] S. Marynissen , B. Bogaerts , M. Denecker , On the relation between approximation fixpoint theory and justification theory , in: Z. Zhou (Ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021 , Virtual Event / Montreal, Canada, 19 -27 August 2021 , ijcai .org, 2021 , pp. 1973 - 1980 . doi: 10 .24963/ijcai. 2021 /272.

[4] S. Killen , W. Gao , J. You , Expanding the class of polynomial time computable well-founded semantics for hybrid MKNF , in: J. Arias , S. Batsakis , W. Faber , G. Gupta , F. Pacenza , E. Papadakis , L. Robaldo , K. Rückschloß , E. Salazar , Z. G. Saribatur , I. Tachmazidis , F. Weitkämper , A. Z. Wyner (Eds.), Proceedings of the International Conference on Logic Programming 2023 Workshops colocated with the 39th International Conference on Logic Programming (ICLP 2023 ), London, United