Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics

1 Introduction

Logic programs [Kowalski and Kuehner, 1971; Lloyd, 1987] are an established language not only for programming, but also for knowledge representation and reasoning. However, in classical logic programs, the dichotomy of allowing propositions to only be either true or false can limit expressivity. More precisely, logic programs under two-valued semantics cannot easily represent knowledge that is imprecise, vague, or uncertain. To address this limitation, Lee [1972] proposed to generalize logic programs to enable the use of fuzzy logic in its semantics, which among other things means allowing to use truth values from the real unit interval [0, 1].

This initial proposal of fuzzy logic programs (FLPs) has led to a considerable body of research that continues growing to this day [Shapiro, 1983; van Emden, 1986; Subrahmanian, 1987; Vojt´aˇs, 2001; Medina et al., 2001; Loyer and Straccia, 2002; Loyer and Straccia, 2003; Loyer and Straccia, 2009a; Cornejo et al., 2018; Cornejo et al., 2020], with an increasing interest in frameworks that abstract away from concrete sets of truth values and instead require only some algebraic properties on them, thus also encompassing the classical, two-valued version as a special case. However, there is no uniform approach to syntax, e.g. what kinds of connectives are allowed in rule bodies, and also no universally accepted "standard" semantics. Instead, several proposals exist, e.g. the approximate well-founded semantics by Loyer and Straccia [2009b] or the stable model semantics by Cornejo et al. [2018], but it is not clear how they are related.

In the present paper, we address some of these open questions within the general algebraic framework of approximation fixpoint theory (AFT). For classical logic programming [van Emden and Kowalski, 1976], it is known that the (standard) least-model semantics of definite logic programs can be defined using an operator on interpretations. In a series of papers, Denecker et al. demonstrated that similar constructions are possible for a range of knowledge representation formalisms, obtaining several profound results that uncovered fundamental similarities between semantics of different knowledge representation languages [Denecker et al., 2000; Denecker et al., 2003; Denecker et al., 2004]. Today, approximation fixpoint theory stands as a unifying framework for studying fixpoint-based semantics, in particular in the context of languages allowing for non-monotonicity.

More concretely, in this paper we show that several fuzzy logic programming semantics from the literature can be incorporated into the framework of approximation fixpoint theory:

1. the approximate well-founded semantics by Loyer and Straccia [2009b], a generalization of the well-founded semantics for classical logic programming [van Gelder et al., 1991]; and
2. the stable model semantics by Cornejo et al. [2018], a generalization of the classical stable model semantics [Gelfond and Lifschitz, 1988].

In fact, we will show that both semantics can be obtained by a single operator using standard constructions from approximation fixpoint theory. As direct results, we obtain how the two semantics are related, and that we can also apply other known techniques from AFT directly to fuzzy logic programming, which we demonstrate by generalizing stratification and ultimate approximation. We are not aware of any existing reconstructions of fuzzy logic programming semantics within approximation fixpoint theory; perhaps the closest related work is that on weighted abstract dialectical frameworks [Brewka et al., 2018] (that are conceptually similar to fuzzy logic programs, but with a different area of application) with an existing treatment in AFT [Bogaerts, 2019].

The paper proceeds as follows: We next give necessary background on approximation fixpoint theory (insofar it is relevant for logic programming) and fuzzy logic programming. Afterwards, we define the concrete syntax of fuzzy logic programs and define the operator that we subsequently use to reconstruct the well-founded semantics (Section 4) and the stable model semantics (Section 5). In Section 6, we showcase some applications of AFT to fuzzy logic programming, reaping the immediate benefits of our reconstruction. Finally, we discuss some avenues for further work and conclude.

2 Background

In this section, we briefly introduce AFT, cover basic fuzzy logic principles, and give an overview of (truth-functional) fuzzy logic programming, focusing on the operator defined by Vojt´aˇs [2001] and many-valued modus ponens.

2.1 Approximation Fixpoint Theory

A particular way of defining semantics for programming languages is to associate a program P with a transformation operator TP that transforms a given input-output relation R into an updated relation TP (R). In this view, the semantics of program P is given by the least fixpoint of the operator TP . Van Emden and Kowalski [1976] applied this way of defining semantics to the field of logic programming, developing the first one-step logical consequence operator and employing its monotonicity in conjunction with Tarski's fixpoint theorem [1955] to define the intended semantics of definite logic programs with potentially recursive predicate definitions.

More formally, an operator is a (total) function O : V → V on a set V . We are typically interested in operators on sets V with an internal structure: At the minimum, we require (V,⩽) to be a partially ordered set. More often, (V,⩽) will be a complete lattice, that is, such that every subset S ⊆ V has a least upper bound (lub) ∨S ∈ V and greatest lower bound (glb) ∧S ∈ V ; this entails that (V,⩽) has both a least element 0 = ∧V = ∨∅ and a greatest element 1 = ∨V = ∧∅. An operator O: V → V is monotone iff x ⩽ y implies O(x) ⩽ O(y), and antimonotone iff x ⩽ y implies O(y) ⩽ O(x). An element x ∈ V with O(x) = x is a fixpoint of O; if O(x) ⩽ x then x is a pre-fixpoint of O; if x ⩽ O(x) then x is a post-fixpoint of O. A fundamental result in lattice theory, Tarski's fixpoint theorem [1955], states that whenever O is a monotone operator on a complete lattice (V,⩽), the set {x ∈ V | O(x) = x} of its fixpoints forms a complete lattice itself, and so has a least element lfp(O). While this result is immensely useful, it is not constructive; however, constructive versions exist and tell us how to actually construct least fixpoints [Markowsky, 1976; Cousot and Cousot, 1979]: To this end, one defines, for any x ∈ V , the iterated (transfinite) application of O to x via O0 (x) := x, Oα+1 (x) := O(Oα(x)) for successor ordinals, and Oβ (x):= ∨{Oα(x) | α < β} for limit ordinals. It is then known that (for monotone O) there exists an ordinal α such that Oα(0) = lfp(O) [Bourbaki, 1949].

In order to apply Tarski's fixpoint theorem [1955] (or its constructive versions), it is thus necessary to have an operator that is monotone, a condition that is no longer fulfilled when extending the syntax of logic programs from definite to normal logic programs, i.e., when allowing "negation as failure" to occur in bodies of rules. To still have a useful fixpoint theory in the case of non-monotone operators, Denecker et al. [2000] fundamentally generalized the theory underlying the fixpoint-based approach to semantics, thereby founding what is now known as approximation fixpoint theory. Its underlying idea is that when an operator of interest does not have properties that guarantee the existence of fixpoints, then this operator can be approximated in a more fine-grained algebraic structure where fixpoint existence can be guaranteed.

Formally - following ideas of Belnap [1977], Ginsberg [1988], and Fitting [2002] -, Denecker et al. [2000] moved from a complete lattice (V,⩽) to its associated bilattice on the set V 2 := V × V . So where elements of V correspond to candidates for the semantics (interpretations), the pairs contained in V 2 correspond to approximations of such candidates. More technically, a pair (x, y) ∈ V 2 approximates all z ∈ V with x ⩽ z ⩽ y. A pair (x, y) ∈ V 2 is called consistent iff x ⩽ y, in other words, if the interval [x, y] := {z ∈ V | x ⩽ z ⩽ y} is non-empty; a pair of the form (x, x) is exact. There are two natural orderings on V 2 :

• (x1, y1) ≤t (x2, y2) :⇐⇒ x1 ⩽ x2 and y1 ⩽ y2, the truth ordering extending the (truth) lattice ordering ⩽;
• (x1, y1) ≤p (x2, y2) :⇐⇒ x1 ⩽ x2 and y2 ⩽ y1, the precision ordering comparing intervals by precision of approximation. The greatest lower bound induced by ≤p is denoted by ⊗ and the least upper bound by ⊕, where we have (x1, y1) ⊗ (x2, y2) = (x1 ∧ x2, y1 ∨ y2) and (x1, y1) ⊕ (x2, y2) = (x1 ∨ x2, y1 ∧ y2).

Just as pairs of V 2 approximate elements of V , the main idea of Denecker et al. [2000] was that operators O: V → V can be approximated by operators on V 2 : An approximator is an operator A: V 2 → V 2 that is ≤p-monotone and that maps exact pairs to exact pairs. By virtue of the latter condition, we say that A approximates the operator O: V → V with O(x) = A(x, x)1 (where (x, y)1 = x and (x, y)2 = y); by virtue of the first condition, A is guaranteed to possess (≤pleast) fixpoints. An approximator A is symmetric iff for all (x, y) ∈ V 2 , we have A(x, y)2 = A(y, x)1; thus symmetry allows to specify A by giving only A(·, ·)1.

The main contribution of Denecker et al. [2000] was the association of the stable approximator Ast to an approximator A: For a complete lattice (V,⩽) and an approximator A: V 2 → V 2 , define the stable approximator for A as Ast : V 2 → V 2 by Ast (x, y) := (lfp(A(·, y)1), lfp(A(x, ·)2)), where A(·, y)1 (resp. A(x, ·)2) denotes the operator that maps any z ∈ V to A(z, y)1 (resp. to A(x, z)2). Among other results, Denecker et al. [2000] also showed that this construction is welldefined because both relevant operators A(·, y)1 : V → V and A(x, ·)2 : V → V are ⩽-monotone (as A is an approximator) and thus possess least fixpoints. Furthermore, any approximator maps consistent pairs to consistent pairs, and the stable approximator Ast maps consistent post-fixpoints of A to consistent pairs. Consequently, not only is lfp(A) consistent (and called the Kripke-Kleene fixpoint of A), but so is lfp(Ast ), the well-founded fixpoint of A. Moreover, a fixpoint (x, y) of Ast , called a stable fixpoint of A, is always a ⩽-minimal fixpoint of O (when A approximates O). The term "stable" is not coincidental: When using the definite logic program transformation operator TP by van Emden and Kowalski [1976] as O and defining a suitable approximator A (see Section 3 for a generalization of such an approximator), then the exact fixpoints of Ast correspond one-to-one to the stable models of the logic program P [Denecker et al., 2000].

2.2 Fuzzy Logic Programming

Let us first define the syntax of positive fuzzy formulas, a generalization of the conjunctions of literals that appear in classical definite logic programs. Given a complete lattice (V, ⩽) of truth values, a set Π of propositional atoms, and a family F of fuzzy connectives (where each f ∈ F has an associated arity n ∈ N which we denote by f (n) when important), we designate a finitely representable subset V ′ ⊆ V of truth values that are allowed to be explicitly mentioned in programs, 1 and define the syntax of a positive fuzzy formula via

where c ∈ V ′ , p ∈ Π, and ∧, ∨,@ ∈ F, to which we refer as conjunctors, disjunctors, and aggregators, respectively. A positive logic program rule is an expression of the form

where p ∈ Π, ϑ ∈ V ′ , ← is an implicator and B is a positive fuzzy formula. The atom p is called the head of the rule, B is called the body of the rule and ϑ its weight (whenever ϑ = 1, we will write a rule as p ← B). A positive fuzzy logic program P is then a finite set of rules (2).

Every connective f (n) ∈ F has an associated truth function f · : V n → V on the complete lattice (V, ⩽) of truth values. The truth functions of the (positive) connectives in our language are assumed to satisfy the following properties:

• for each f ∈ F, f · is ⩽-monotone in each argument;
• for each conjunctor ∧ ∈ F, its truth function ∧· satisfies p1 ∧· p2 ⩽ p1, p1 ∧· p2 ⩽ p2, and p ∧· 1 = p = 1 ∧· p;
• for each disjunctor ∨ ∈ F, its truth function ∨· satisfies p1 ⩽ p1 ∨· p2, p2 ⩽ p1 ∨· p2, and p ∨· 0 = p = 0 ∨· p;
• for each implicator ← ∈ F, ←· is monotone in the first argument and antimonotone in the second argument.

If ∧· is also associative and commutative and V = [0, 1] ⊆ R, then ∧· is called a t-norm. However, we do not make any assumptions on associativity, commutativity, or continuity of truth functions in this paper. An example of truth functions are G¨odel's, with x∧·G y = min{x, y}, x∨·G y = max{x, y}, and x ←·G y = x if y > x and x ←·G y = 1 otherwise.

1 Allowing truth values to occur explicitly in formulas is with the intended usage of being able to represent some truth values in rule bodies as we do in Example 2. This does not necessarily work for arbitrary sets of truth values (e.g. it does not work for V = [0, 1] ⊆ R by sheer cardinality) - in those cases we want to allow to restrict the syntax to a meaningful subset of truth values that can be finitely represented, e.g. the rational unit interval V ′ = [0, 1] ∩Q.

For a complete lattice (V, ⩽) of truth values and Π a set of atoms, an interpretation is a total function I : Π → V . The set of all interpretations is denoted by I. It can be shown (and is known) that (I,≤) again is a complete lattice, where I ≤ J iff I(p) ⩽ J(p) for all p ∈ Π. We denote the least and greatest elements of this lattice by 0 := {p ↦→ 0 | p ∈ Π} and 1 := {p ↦→ 1 | p ∈ Π}, respectively. Later, we will work on the associated bilattice I 2 with ≤p-least element (0, 1); glb ⊗ and lub ⊕ carry over from V 2 to I 2 in a pointwise manner, e.g. ((L,U) ⊗ (L′ ,U ′ ))(p) := (L,U)(p) ⊗ (L′ ,U ′ )(p).

We work with truth-functional logic in a narrow sense, whence the truth value of a formula is uniquely determined by the truth value of its constituents. Given an interpretation I, we thus extend the interpretation to arbitrary formulas φ via structural induction, and denote the truth value of φ under I by ˆ I(φ). More precisely, for connective f (n) ∈ F, we define ˆ I(f(φ1, . . . , φn)) := f · (ˆ I(φ1) , . . . , ˆ I(φn)). For example, for G¨odel logic we obtain ˆ I(x ∧G y) = I(x) ∧·G I(y).

We next define how the truth value ˆ I(B) of a body of a rule is propagated towards the head p. The inference rule proposed by Vojt´aˇs [2001] for fuzzy logic programming is based on many-valued modus ponens (H´ajek [1998] gives details):

(MP) should infer a truth value z of the conclusion p when given a truth value x of φ and a truth value y = z ←· x of the implication p ← φ. Let mp denote a candidate function, i.e. a way to compute mp(x, y) = z. To ensure soundness of the inference, mp should be monotone in both of its arguments (increasing truth values of the premises lead to higher truth in the conclusion) and satisfy the boundary conditions mp(0, 1) = mp(1, 0) = 0 and mp(1, 1) = 1. These are the properties of a truth function of a conjunctor ∧. If in addition the truth value of z ←· x is as large as possible, we get

A pair (←· , ∧· ) that satisfies (3) for all x, y, z ∈ V of a partially ordered set (V,⩽) is then called an adjoint pair [Medina et al., 2001]. In order to designate adjoint pairs, we will write them with the same index, i.e. as (←i, ∧i). Intuitively, adjoint pairs guarantee correctness of inference whenever we pair "matching" implicators and conjunctors, e.g. (←G, ∧G).

Given an interpretation I ∈ I, a weighted rule p ϑ←i B is satisfied by I iff ϑ ⩽ I(p) ←·i ˆ I(B). An interpretation I is a model of P iff it satisfies all rules in P. Intuitively, I satisfies a rule if it makes the rule "at least as true" as its weight ϑ. By (3), this translates to: the head is "at least as true" as the body limited by the rule's weight, or formally ϑ ∧·i ˆ I(B) ⩽ I(p).

Vojt´aˇs [2001] and Medina et al. [2001] define a fuzzy generalization of the transformation operator given by van Emden and Kowalski [1976]: For a fuzzy logic program P, the immediate consequence operator TP : I → I is defined by

The semantics of a positive FLP P can then be characterized by the pre-fixpoints of TP [Vojt´aˇs, 2001, Theorem 2.2], i.e. an interpretation I ∈ I is a model of P iff TP (I) ≤ I. This generalizes a classical result by van Emden and Kowalski [1976].

Example 1. Consider the positive fuzzy logic program P = {r ←G 0.3 ∨G (s ∧G 0.6), s ←G s} over ([0, 1],⩽). Any interpretation I with 0.3 ⩽ I(r) is a model of P. The least model of P can be obtained as the least fixpoint of TP via transfinitely iterating TP on 0, leading to the interpretation TP (0) = {r ↦→ 0.3, s ↦→ 0} = I1 = TP (I1) = lfp(TP ).

3 An Approximator for FLPs

The main challenge in defining semantics for (fuzzy) logic programs lies in the treatment of "negation as failure". Syntactically, we now move to normal fuzzy logic programs, that is, we extend the syntax of positive fuzzy formulas by default negation ∼, a unary connective of which we only require that its truth function ∼· : V → V is an antimonotone involution [Ovchinnikov, 1983]. (∼· being an involution means that ∼·∼·v = v for all v ∈ V ; it follows that ∼·0 = 1 and ∼·1 = 0 whence ∼ is a generalization of two-valued negation.) For V = [0, 1] ⊆ R, the typical choice is ∼·x = 1 - x, which we will use in all subsequent examples.

Formally, a normal fuzzy formula is of the form

where c ∈ V ′ , p ∈ Π, and ∧, ∨, @ ∈ F as before. A normal fuzzy logic program is then a finite set of normal fuzzy rules, and the remaining notions involving "normal" carry over from "positive" as expected. In particular, to define the evaluation of a normal fuzzy formula φ under interpretation I ∈ I, we have the additional inductive case ˆ I(∼φ) = ∼· ˆ I (φ).

The one-step consequence operator TP [Vojt´aˇs, 2001; Medina et al., 2001] is likewise extended to the case of normal FLPs, with models of P and pre-fixpoints of TP still being in one-to-one correspondence. However, the resulting operator TP is no longer ≤-monotone and so cannot directly be used to define a least-model semantics for normal programs.

Example 2. Consider the following normal fuzzy logic program P over V = [0, 1] (due to Loyer and Straccia [2009b]):

Any fuzzy interpretation I with 0.3 ⩽ I(r) ⩽ I(p), I(s) ⩽ I(q), and 1-I(p) ⩽ I(q) is a model of P . Whenever I(p) + I(q) = 1, 0.3 ⩽ I(p), I(r) = 0.3, and I(s) = 0, then I is also a minimal model. Consequently, P has an infinite number of minimal models.

Approximation fixpoint theory fortunately provides an elegant solution to this problem - all we have to do is define an approximator to TP , and AFT does the rest.

Definition 1 (Approximator). For a normal FLP P over complete lattice (V,⩽), we associate the symmetric approximator TP : I 2 → I 2 with

where ̂ (L,U)(B), the evaluation of B under interpretation pair (L, U) ∈ I 2 , is defined via structural induction with notable base cases ̂ (L, U )(p):=L(p) and ̂ (L, U )(∼p):=∼·U (p), and straightforward inductive case ̂ (L, U)(f(φ1, . . . , φn)):= f ·(̂ (L, U)(φ1) , . . . ,̂ (L, U )(φn)).

Thus TP (L, U) = (TP (L, U)1, TP (U, L)1) gives the overall approximator. Figure 1 (p. 6) shows how the approximator maps (pairs of) interpretations to others for Example 2.

It is easy to see that TP is well-defined to serve its purpose:

Proposition 1. TP approximates TP and is ≤p-monotone.

Thus TP also approximates the operator by Vojt´aˇs [2001] and generalizes its semantics. Additionally, using the standard definitions of approximation fixpoint theory, Definition 1 also indirectly yields the well-founded semantics of P via lfp(T st P ), as well as the stable model semantics via the exact fixpoints of T st P . In the remainder of the paper, we will relate these semantics (as obtained by AFT directly) to similar semantics that have been manually defined in the literature.

4 Well-Founded Semantics

In this section we show that AFT captures the well-founded semantics for fuzzy logic programs as defined by Loyer and Straccia [2009a]. The first (minor) technical hurdle is that where AFT uses pairs (L,U) of fuzzy interpretations, Loyer and Straccia [2009a] use interpretations that assign a pair of truth values to each atom p ∈ Π. More formally, an approximate interpretation is a total function X: Π→ V ×V ; the set of all approximate interpretations is denoted by C. Loyer and Straccia [2009a] then extend approximate interpretations to normal fuzzy formulas: Firstly, they extend the truth functions of connectives f (n) ∈ F from V to V ×V via f ·· ((ℓ1, u1), . . . , (ℓn, un)) := (f · (ℓ1, . . . , ℓn), f · (u1, . . . , un)), and set ∼·· ((ℓ, u)) := (∼·u,∼·ℓ); secondly, they define ˆX(φ) by structural induction on formulas φ (including default negation ∼), with base cases ˆX(p) = X(p) and ˆX(c) = (c, c) for c ∈ V ′ . Loyer and Straccia [2009a] then define an operator on approximate interpretations via SP (X)(p) = ˆX(Bp) where they assume that every p ∈ Π has a unique rule p ← Bp ∈ P (which is not a restriction because several rules for p can be joined with disjunction ∨). It is clear that the set C of approximate interpretations and the set I 2 of pairs (L,U) of fuzzy interpretations are isomorphic (whence ⊗ and ⊕ carry over to C); for a given X ∈ C, we use ζ(X) to denote (L,U) such that X(p) = (L(p), U(p)) for all p ∈ Π. As our first result in this section, it then follows that modulo this isomorphism on the underlying structures, the operator SP by Loyer and Straccia [2009a] and our approximator TP of Definition 1 coincide.

Lemma 2. For any FLP P and any approximate interpretation X over Π, we have ζ(SP (X)) = TP (ζ(X)).

This result paves the way for our subsequent formal comparison of the well-founded semantics defined by Loyer and Straccia [2009a] and the well-founded semantics given by approximation fixpoint theory [Denecker et al., 2000]. The next definition makes use of two special interpretations: Xf is such that ζ(Xf) = (0, 0) (it assigns false everywhere), and X⊥ is such that ζ(X⊥) = (0, 1) (it assigns unknown everywhere). The closed world operator sP is used to construct the well-founded semantics. We will use the following characterization [Loyer and Straccia, 2009a, Theorem 4]: Given an approximate interpretation X, sP (X) is defined as the least fixpoint of the function FP,X(Y ):=Xf⊗SP (X⊕Y ), that is, sP (X) := lfp≤t (FP,X). The approximate well-founded operator is then defined as: AWP (X) = SP (X) ⊕ sP (X). Finally, the approximate well-founded model is lfp≤p (AWP ).

Lemma 3. For any FLP P and any approximate interpretation X over Π with ζ(X) = (L,U), we have that ζ(sP (X)) = (0, lfp(TP (L, ·)2)).

We now show that the approximate well-founded model is identical to the well-founded fixpoint of TP . Intuitively, we prove this by relating the paths that the operators AWP and T st P traverse when applied iteratively to X⊥ ˆ= (0, 1): every pair visited by T st P is also visited by AWP , but not necessarily vice versa. (This can also be seen in Figure 1.)

Theorem 4. For any FLP P with approximate well-founded model XSWF, we have ζ(XSWF) = lfp(T st P ).

Proof. In what follows, we will denote the sequence used to construct lfp≤p (AWP ) by ⟨Xi⟩i≤α, and ζ(Xi) by (Li,Ui) (for any i ≤ α). 2 We prove the theorem by showing that ⟨(Li, Ui)⟩i≤α is a terminal monotone induction of T st P , i.e. a sequence ⟨(Li, Ui)⟩i≤α such that:

1. (L0,U0) = (0, 1),
2. (Li,Ui) <p (Li+1,Ui+1) ≤p T st P (Li,Ui) for all i < α,
3. (Lσ,Uσ) = ⊕({(Li,Ui) | i < σ}), for every limit ordinal σ < α,
4. there is no (Lα+1,Lα+1) such that ⟨(Li,Ui)⟩i≤α+1 is a monotone induction.

It then follows with [Denecker and Vennekens, 2007, Proposition 1] that ζ(lfp≤p (AWP )) = lfp(T st P ).We denote lfp(TP (L, ·)2) by cT st P (L) to avoid clutter in what follows. Ad 1: Clear from the definition of ζ(lfp≤p (AWP )).

Ad 2: We first show by induction that (†) ⟨(Li+1, Ui+1)⟩ = (TP (Li, Ui)1, cT st P (Li)). The base case is trivial. For the inductive case, suppose that ⟨(Li+1,Ui+1)⟩ = (TP (Li, Ui)1, cT st P (Li)). We show that ⟨(Li+2,Ui+2)⟩ = (TP (Li+1, Ui+1)1, cT st P (Li+1)). Indeed as AWP (Xi+2) = SP (Xi+1)⊗sP (Xi+1) and ζ(sP (Xi+1)) = (0, cT st P (Li+1)) (Lemma 3), it is easy to see that Li+2 = TP (Li+1,Ui+1)1. It remains to show that Ui+2 = cT st P (Li+1). We do this by showing that cT st P (Li+1) ⩽ TP (Li+1, Ui+1). As Li ⩽ Li+1 (as AWP is a ≤p-monotone operator [Loyer and Straccia, 2009a, Theorem 7]) and T st P is ≤p-monotone (which means that cT st P is ⩽-anti monotone), cT st P (Li+1) ⩽ cT st P (Li) =

2 Notice that Loyer and Straccia [2009a] do not define the approximate well-founded semantics in a constructive way, but refer to Tarski [1955] to guarantee the existence of a least fixpoint. However, as explained in Section 2.1 we can (without loss of generality) assume that this least fixpoint was constructed using an iterated (possibly transfinite) application of AWP .

Ui+1. As TP is ≤p-monotone, TP (Li+1, ·)2 is ⩽-monotone, and thus, TP (Li+1, cT st P (Li+1))2 ≤ TP (Li+1,Ui+1)2. As TP (Li+1, cT st P (Li+1))2 = cT st P (Li+1) (after all, cT st P (Li+1) is the least fixed point of cT st P (Li+1, ·), this concludes the proof of †.

Back to the proof of the main claim. That Xi <p Xi+1 follows immediately from that fact that AWP is a ≤p-monotone operator [Loyer and Straccia, 2009a, Theorem 7]. We show that ζ(SP (Xi)) ≤p T st P (ζ(Xi)), by induction on i. The base case is clear. For the inductive case, suppose that Xi ≤p T st P (ζ(Xi-1)). As Xi-1 ≤p Xi (as we just showed), and T st P is a <p-monotone operator, T st P (ζ(Xi-1)) ≤p T st P (ζ(Xi)), and thus we have that ζ(Xi) ≤p T st P (ζ(Xi)). This implies that Li ⩽ T st P (Xi)1. As TP (·,Ui)1 is ⩽-monotone, TP (Li, Ui)1 ⩽ TP (T st P (Xi)1,Ui)1. As T st P (Xi)1 is the least fixpoint of TP (·,Ui)1, TP (T st P (Xi)1,Ui)1 = T st P (Xi)1. We infer that TP (Li, Ui)1 ⩽ T st P (Xi)1, concluding the proof.

Ad 3: This follows immediately from the definition of the iterated application of an operator.

Ad 4: This is clear as we take the least fixpoint of ζ(AWP ), which means that for any extension of the sequence, the condition Xi <p Xi+1 is not satisfied. □

However, this result does not generalize to arbitrary partial stable interpretations (arbitrary fixpoints of T st P ):

Example 3. Consider the normal fuzzy logic program P = {p ←G q, p ←G p, q ←G ∼r, r ←G ∼q}. From Theorem 4, it follows that the least fixpoints of T st P and AWP coincide (modulo isomorphism). However, the approximate interpretation X = {p ↦→ (1, 1), q ↦→ (0, 1), r ↦→ (0, 1)} is a fixpoint of AWP , but ζ(X) is not a fixpoint of T st P . Intuitively, AWP cannot identify the positive cycle p ←G p that is needed to keep p true in X, while T st P can identify it.

5 Stable Model Semantics

We now turn our attention to the stable model semantics for normal fuzzy logic programs as defined by Cornejo et al. [2018]. As for classical (two-valued) normal logic programs, the notion of a stable model of a fuzzy normal logic program is associated with the least model of a positive program (whose consequence operator is monotone and thus has a unique least fixpoint). Given a normal FLP P and an interpretation I, Cornejo et al. [2018] introduce a mechanism to obtain the positive program PI by substituting each rule r = p ϑ←i B in P by a rule rI :=p ϑ←i BI, where BI is formally defined as follows: Firstly, to indicate which atoms are used positively or negatively in the body formula B, we write B[p1, . . . , pm, ∼pm+1, . . . , ∼pn] as used by Cornejo et al. [2018]. Secondly, every formula B[p1, . . . , pn] of our language leads to an n-ary aggregator B[·, . . . , ·]; for example, the formula φ[p, q, r] = p ∧ (q ∨ r) leads to the aggregator φ[·, ·, ·] (that could also produce φ[r, p, q] = r ∧ (p ∨ q)) with associated truth function φ· (x1, x2, x3) = x1 ∧· (x2 ∨· x3). This allows to define the associated truth function of BI via: B·I (x1, . . . , xm) = B·(x1, . . . , xm, ∼·I(pm+1), . . . , ∼·I(pn)) Intuitively, BI evaluates all and only the atoms that appear negatively in B by I, and keeps the atoms that occur positively. The program PI := {rI | r ∈ P} is the reduct of P

w.r.t. I. An I ∈ I is then a stable model of a normal FLP if and only if I is the least model of PI [Cornejo et al., 2018].

In the remainder of this section, we show how to reconstruct the stable model definition of Cornejo et al. [2018] within approximation fixpoint theory. The first result relates our approximator with Cornejo et al.'s definition of reduct.

It is clear that equal operators have equal fixpoints:

This result now allows to prove the main result of this section, namely the correspondence of the two variants of definining the stable model semantics for fuzzy logic programs.

Theorem 7. An exact interpretation (I, I) is a (AFT) stable model of P iff I is a (Cornejo et al.) stable model of P.

Proof. (I, I) is an AFT stable model of P iff T st P (I, I) = (I, I) iff lfp(TP (·, I)1) = I iff lfp(TPI ) = I iff I is a Cornejo et al. stable model of P. □

6 Applying AFT to Fuzzy Logic Programming

In this section, we derive several useful results that follow as straightforward corollaries from the fact that we used AFT as a unifying framework for representing the semantics of FLPs. In more detail, we investigate the relation between wellfounded and stable model semantics (Section 6.1), provide results on stratification (Section 6.2), and introduce the ultimate semantics for fuzzy logic programming (Section 6.3).

6.1 Relationship Between Semantics

One of the benefits of the operator-based characterization given in this paper is that it allows us to straightforwardly derive results on the relationship between different semantics considered here. Firstly we consider the fuzzy well-founded and stable model semantics. In AFT, it is well-known that the well-founded fixpoint is an approximation of every exact stable fixpoint. Combining this insight with the characterizations developed in this paper, we obtain the following result, relating the semantics of Loyer and Straccia [2009a] and Cornejo et al. [2018].

Theorem 8. For any (AFT) stable model (I, I) of P, we have lfp(T st P ) ≤p (I, I). Equivalently, for any (Cornejo et al.) stable model I of P, we have ζ(XSWF) ≤p (I, I).

Secondly, we show that the fuzzy semantics are generalizations of the classical, two-valued semantics. This is not obvious from their original definitions in the literature, but becomes obvious after our reconstruction in AFT.

Proposition 9. Assume the complete lattice of truth values V = {0, 1} with 0 < 1. For every classical normal logic program P: (1) its well-founded model according to Loyer and Straccia [2009a] coincides with its well-founded model according to van Gelder et al. [1991]; (2) its stable models according to Cornejo et al. [2018] coincide one-to-one with its stable models according to Gelfond and Lifschitz [1988].

6.2 Stratification for Fuzzy Logic Programs

We first recall some necessary preliminaries [Vennekens et al., 2006], adapted to our setting. 3 Given an interpretation I ∈ I, and a set of atoms Π′ ⊆ Π, I|Π′ : Π′ → V is defined by I|Π′ (p) = I(p) for any p ∈ Π′ . For elements (L, U) of the bilattice V 2 , we denote (L|Π′ , U|Π′ ) by (L, U)|Π′ . The order ⩽ can likewise be restricted, denoted by ⩽|Π′ . Given an operator O over I relative to a set of atoms Π, where Π1, Π2 forms a partition of Π, O is stratifiable over Π1,Π2 iff for every I 1 , I 2 ∈ I, if I 1 |Π1 = I 2 |Π1 then O(I 1 )|Π1 = O(I 2 )|Π1 . Some of the main results of Vennekens et al. [2006] include that the the construction of (or search for) all major AFT semantics can be split up along the strata an operator is stratifiable over.

We now recall a syntactical criterion for identifying strata based on dependency graphs, again inspired by the work of Vennekens et al. [2006]. This criterion generalizes the wellknown definition known from normal logic programs [Apt et al., 1988; van Gelder, 1988]. We restrict attention to stratifications consisting of two strata for simplicity, but these results can be extended straightforwardly to arbitrary numbers of strata. We first need some additional preliminaries. Given a program P and p, q ∈ Π, we define q ⪯P p iff there is a p ϑ←i B ∈ P such that q ∈ B. We then say that P is stratifiable over the partition Π1,Π2 of Π iff q ⪯P p, q ∈ Πi, and p ∈ Πj imply that i ≤ j. Informally, if two atoms depend on each other, they either occur in the same stratum or the dependent atom occurs in the higher stratum. This is an immediate generalization (at least for the case of two strata) from normal to fuzzy logic programs of the definition of splitting by Vennekens et al. [2006]. The traditional notion of stratification [Apt et al., 1988; van Gelder, 1988] additionally requires that negatively occuring body atoms come from a strictly lower stratum.

3 In the general algebraic setting of Vennekens et al. [2006], these definitions are introduced using the notion of a product lattice, but we could simplify these notions as done above.

Theorem 10. For any FLP P , if P is stratifiable over Π1, Π2, then TP is stratifiable over Π1,Π2.

Proof (Sketch). Suppose that P is stratifiable over Π1,Π2. We show that (†): for any (L1 ,U 1 ), (L2 ,U 2 ) ∈ V 2 , if (L1|Π1 ,U 1 |Π1 ) = (L2|Π1 ,U 2 |Π1 ), then TP (L1 ,U 1 )|Π1 = TP (L2 ,U 2 )|Π1 . Consider some p ∈ Π1, some p ϑ←i B ∈ P and some q ∈ B. Thus q ⪯P p and since P is stratifiable, p ∈ Π1 implies q ∈ Π1. Thus, we have established that p ∈ Π1 implies q ∈ Π1, for any p ϑ←i B ∈ P and q ∈ B. (†) now follows immediately from the definition of TP . □

It follows now from the results of Vennekens et al. [2006] (Theorem 3.11 and Corollary 3.12), that the construction of the well-founded fixpoint and the search for stable fixpoints can be split up along the strata formed in a dependency graph. In practice, this is done by first doing the necessary computations for the lower stratumΠ1, and then transforming the program as to take into account the computed values. More technically, given an interpretation (L1 , U 1 ) for Π1 and a formula B, let B(L1 ,U 1 ) be the formula obtained by replacing every positive p ∈ Π1 by L1 (p) and every negative ∼p by ∼·U 1 (p), and let P(L1 ,U 1 ) = {p ϑ←i B(L1 ,U 1 ) | p ϑ←i B ∈ P}.

Lemma 11. Suppose that P is stratifiable over Π1,Π2. Given an interpretation (L,U) over Π1 ∪ Π2 and an interpretation (L1 ,U 1 ) over Π1, if (L,U)|Π1 = (L1 ,U 1 ) then TP(L1,U1) (L, U)|Π2 = (TP (L, U))|Π2 .

Theorem 12. For any FLP P , if P is stratifiable over Π1, Π2, then (L,U) is a stable [the well-founded] fixpoint of TP iff (L|Π1 ,U|Π1 ) is a stable [the well-founded] fixpoint of (TP )|Π1 and (L|Π2 ,U|Π2 ) is a stable [the well-founded] fixpoint of TP(L1,U1) .

6.3 Ultimate Semantics

For a given operator O: V → V , there will typically be many different approximators A for O, and choosing among them might not be trivial. Denecker et al. [2004] devised a way to construct the most precise approximator possible: The ultimate approximator of O is given by UO : V 2 → V 2 with UO(x, y) = (∧O([x, y]), ∨O([x, y])) where we denote O([x, y]) := {O(z) | x ⩽ z ⩽ y}. 4 The usual AFT definitions of semantics relying on fixpoints of U st O then yield ultimate versions of the semantics, e.g. the ultimate well-founded semantics of UO is given by lfp(U st O ).

The ultimate approximation of the operator TP on normal FLPs (Section 3) is thus given by UTP , which we denote by UP for ease of notation. The following example illustrates the potential advantages of UP in comparison to TP .

4 Most precise here means that for all approximators A of O and pairs (x, y) ∈ V 2 , it holds that A(x, y) ≤p UO(x, y).

While we have TP (0, 1) = (0, 1) for our approximator from Definition 1, the ultimate approximator obtains the strictly better bounds UP (0, 1) = ({p ↦→ 0.5} , 1) = lfp(UP ). Consequently, for the well-founded semantics, we obtain TP (0, 1)1 = 0 and TP (0, 0)2 = 1 whence (0, 1) is the wellfounded fixpoint of TP ; in contrast, using the ultimate approximator we get UP (0, 1)1 = {p ↦→ 0.5} and UP (0, 0)2 = 1 whence ({p ↦→ 0.5} , 1) is the well-founded fixpoint of UP .

For the semantics characterized by least fixpoints, it is known in AFT that the ultimate approximator leads to the most precise version of the semantics [Denecker et al., 2004, Theorem 5.2]. For fuzzy logic programming, we thus get:

Similarly, for semantics characterized by exact fixpoints, ultimate approximators preserve all exact (stable) models of other approximators, and may in general add new models [Denecker et al., 2004, Theorem 5.3].

Proposition 14. For any FLP P and I ∈ I:

1. If (I, I) is a fixpoint of TP , it is a fixpoint of UP ;
2. if (I, I) is a stable fixpoint of TP , it is a stable fixpoint of UP .

Thus, having the semantics reconstructed within AFT, we could not only easily define fuzzy logic programming semantics that are more precise than those in the literature [Loyer and Straccia, 2009a; Cornejo et al., 2018], but also got results on how they relate to the less precise semantics.

7 Discussion and Conclusion

In this paper, we have reconstructed two specific semantics for fuzzy logic programming within approximation fixpoint theory. This reconstruction enabled several novel results on fuzzy logic programming: It allowed us to (1) establish a formal relationship between the two semantics, (2) generalize stratification to the case of fuzzy logic programs, and (3) define ultimate (stable/well-founded) semantics, which provide more information than their ordinary counterparts.

In future work, we want to analyze what current restrictions we could lift while keeping the positive, unifying aspects of our reconstruction. Firstly, we intend to allow for a more general syntax of fuzzy logic programs, thus moving towards (A) extended logic programs, where both classical negation ¬ and default negation ∼ can be used in rules [Gelfond and Lifschitz, 1991], where Cornejo et al. [2020] proposed a (fuzzy) stable model semantics; and/or (B) nested logic programs [Lifschitz et al., 1999], where negation can occur freely in program bodies. Next, we also want to study lifting our requirements on negation; in particular, the condition that negations ∼· must be involutions, so that we can also allow G¨odel negation. Finally, we are interested in the (ordinal) number of steps that are needed to reach the least fixpoint of relevant operators such as TP and T st P . We are fairly confident that for finite programs with only rational explicit truth values and connectives that stay within the rationals, the fixpoint can be reached within ω = |N| steps.

Acknowledgements

This work is partly supported by BMBF (Federal Ministry of Education and Research) in DAAD project 57616814 (SECAI, School of Embedded Composite AI). We also acknowledge funding from BMBF within projects KIMEDS (grant no. GW0552B), MEDGE (grant no. 16ME0529), and SEMECO (grant no. 03ZU1210B).

Jesse Heyninck was partially supported by the project LogicLM: Combining Logic Programs with Language Model with fle number NGF.1609.241.010 of the research programme NGF AiNed XS Europa 2024-1 which is (partly) financed by the Dutch Research Council (NWO).

We thank Bart Bogaerts for discussions on this paper, including suggesting the proof structure of Theorem 4 (inspired by his own work [Bogaerts and Cruz-Filipe, 2024]), and coming up with Example 3.