Safe Inductions: An Algebraic Study

1 Introduction

In many fields of computational logic, natural forms of induction show up. Such an induction can be seen as a sequence of semantic structures obtained by iterative applications of rules or a semantic operator. For instance, in logic programming, it is natural to think of sequences of interpretations where at each stage a number of rules whose bodies are satisfied are triggered (i.e., their head is added to the current interpretation). For positive logic programs, all such sequences converge to the minimal model. For non-positive programs, this strategy may yield meaningless results. For instance, for the program P = {a, b ← ¬a}, one such sequence is ∅, {b}, {b, a}, the limit of which is not even a supported model of the logic program. Intuitively, what is wrong here is that the rule b ← ¬a is applied before the value of a is established. For stratified programs, like P, this problem has been resolved [Apt et al., 1988]. For the general case, the well-founded semantics [Van Gelder et al., 1991] offers a solution that uses three-valued interpretations instead of twovalued interpretations.

In recent work, the notions of natural and safe inductions for inductive definitions were introduced [Denecker and Vennekens, 2014; Denecker et al., 2017]. It was argued that this kind of processes forms the essence of our understanding of inductive definitions.

∗Bart Bogaerts is a postdoctoral fellow of the Research Foundation - Flanders (FWO).

In this paper, we lift those ideas to a more general setting: we provide a principled study of inductions in approximation fixpoint theory (AFT) (Denecker, Marek and Truszczy´nski (DMT) 2000), an algebraic theory that provides a unifying framework of semantics of nonmonotonic logics. We show convergence of safe inductions in general and study the relationship between safe inductions and various fixpoints defined in approximation fixpoint theory.

By presenting our theory in AFT, our results are broadly applicable. DMT [2000] originally developed AFT to unify semantics of logic programs, autoepistemic logic and default logic. Later, it was also used to define semantics of extensions of logic programs, such as HEX logic programs [Antic et al., 2013] and an integration of logic programs with description logics [Liu et al., 2016]. Strass [2013] showed that many semantics from Dung's argumentation frameworks (AFs) [Dung, 1995] and abstract dialectical frameworks (ADFs) [Brewka et al., 2013] can be obtained by direct applications of AFT. Cruz-Filipe [2016] and Bogaerts and Cruz-Filipe [2017] showed that AFT has applications in database theory, for defining semantics of active integrity constraints [Flesca et al., 2004].

The theory we present in this paper induces for each of the above logics notions of (safe) inductions and a safe semantics. Our complexity results are obtained for general operators and hence can also be transfered to various logics of interest. Throughout the paper, we give examples from logic programming; in Section 6, we apply our theory to autoepistemic logic. There, we show that safe inductions induce a constructive semantics that captures the intended semantics of a class of theories for which classical constructive semantics fail. This failure was recently exposed and solved using a notion of set-inductions which is based on sets of lattice elements instead of intervals (which are standard in AFT) [Bogaerts et al., 2016]. We show that safe inductions provide an alternative solution to this problem. Our solution is more direct: in contrast to set-inductions or well-founded inductions [Denecker and Vennekens, 2007], safe inductions do not require any form of approximation; they are sequences in the original lattice. For logic programming, this means that they are sequences of interpretations such that some atoms are derived in each step. For AEL, this means that they are sequences of possible world structures such that additional knowledge is derived in each step.

2 Preliminaries: Lattices and Operators

A partially ordered set (poset) 〈L, ≤〉 is a set L equipped with a partial order ≤, i.e., a reflexive, antisymmetric, transitive relation. We write x < y for x ≤ y ∧ x ̸= y. We call 〈L, ≤〉 a complete lattice if every subset S of L has a least upper bound ∨ S and a greatest lower bound ∧ S. A complete lattice has a least element ⊥ and a greatest element ⊤. We use notations x ∨ y = ∨({x, y}) and x ∧ y = ∧({x, y}).

An operator O : L → L is monotone if x ≤ y implies that O(x) ≤ O(y). An element x ∈ L is a prefixpoint, a fixpoint, a postfixpoint of O if O(x) ≤ x, respectively O(x) = x, x ≤ O(x). Every monotone operator O in a complete lattice has a least fixpoint [Tarski, 1955], denoted lfp(O), which is also O's least prefixpoint and the limit of any monotone induction, i.e., of any increasing sequence (xi)i≥0 satisfying

• x0 = ⊥,
• xi ≤ xi+1 ≤ O(xi), for successor ordinals i + 1,
• xλ = ∨({xi | i < λ}), for limit ordinals λ.

Logic Programming Let Σ be an alphabet, i.e., a collection of symbols which are called atoms. A logic program P is a set of rules r of the form h ← ϕ, where h is an atom called the head of r, denoted head(r), and ϕ is a conjunction of literals called the body of r, denoted body(r). An interpretation I of Σ is a subset of Σ. The set of interpretations 2Σ forms a lattice equipped with the order ⊆. The truth value (t or f) of a propositional formula ϕ in a structure I, denoted ϕI , is defined as usual. With a logic program P, we associate an immediate consequence operator TP [van Emden and Kowalski, 1976] that maps a structure I to the structure

This is an operator on the lattice 〈2Σ,⊆〉.

3 Safe Inductions

Let L be a lattice and O an operator on L, fixed throughout the rest of this paper.

Definition 3.1. We call y ∈ L derivable from x ∈ L if x ≤ y ≤ x ∨ O(x).

Definition 3.2. Let x be an element of L. An O-induction in x is a sequence (xi)i≤β such that

• x0 = x,
• xi+1 is derivable from xi for each i < β,
• xλ = ∨({xi | i < λ}), for limit ordinals λ ≤ β.

Intuitively, we view O as an operator that constructs certain lattice points. An O-induction is the associated construction process. Intuitively, if we are at a stage xi, O(xi) represents what can be concluded from this given stage. Therefore, the next step xi+1 in the induction is at least xi (xi+1 ≥ xi) and at most the combination of xi and what can be concluded from it (xi+1 ≤ xi ∨ O(xi)). In the context of a powerset lattice (a lattice of the form 〈2S ,⊆〉), this means that xi+1 ⊆ xi∪O(xi), i.e., xi+1 only contains elements that were already in xi or such that O concludes them from xi.

Definition 3.3. Let N = (xi)i≤β and N ′ = (yi)i≤α be two O-inductions. We say that N ′ extends N if α ≥ β and xi = yi for all i ≤ β. The extension is strict if yα ̸= xβ.

Definition 3.4. An O-induction is terminal if there exists no O-induction that strictly extends it.

Proposition 3.5. An O-induction (xi)i≤β is terminal if and only if xβ is a prefixpoint of O.

Proposition 3.6. If O is monotone, all monotone inductions are O-inductions in ⊥ and vice versa.

Corollary 3.7. If O is monotone, all terminal O-inductions in ⊥ converge to lfp(O).

There is a high degree of non-determinism in O-inductions. For monotone operators O, despite this non-determinism, all O-inductions converge to the same point. As such, Oinductions provide (if O is monotone) a way to construct an intended lattice point (lfpO). For non-monotone operators, the situation is quite different: O-inductions might not converge to a single point.

Example 3.8. Let P be the logic program

This is a simple, stratified logic program [Apt et al., 1988; Przymusinski, 1988]. Its intended fixpoint (its so-called perfect model) is {p}. Let TP denote its immediate consequence operator. The following are the three terminal strict TPinductions in ⊥ = ∅.

In Example 3.8 it can be seen that certain derivations in an O-induction happen prematurely. For instance, in N1 and N2, q is derived by the non-monotonic rule q ← ¬p. As soon as p is derived, this rule no longer applies: q ̸∈ TP({p, q}) = {p}. In this sequence, the rule was applied when it was not safe to do so. Below, we define a notion of safety to avoid such premature derivations, i.e., to only derive facts that remain derivable, regardless of what other derivations are made further on in the induction process.

Definition 3.9. Let x′ be derivable from x. We say that x′ is safely derivable from x if for each O-induction (xi)i≤β in x, it holds that x′ ≤ x ∨ O(xβ).

An O-induction (xi)i≤β is safe if xi+1 is safely derivable from xi for each i < β.

In words, x′ is safely derivable from x if no matter what other derivations we make (ending up in xβ), x′ consists at most of what we have in x combined with what O concludes from xβ, i.e., x′ ≤ x ∨O(xβ).

An induction is terminal if it cannot be extended into a strictly larger induction. We define a similar concept for safe inductions.

Definition 3.10. A safe O-induction N is safe-terminal if there exists no strict extension N ′ of N that is safe.

In Example 3.8, we showed that not all terminal Oinductions converge to the same lattice point. Luckily, the safety criterion warrants a better situation.

Theorem 3.11. For each x ∈ L, all safe-terminal Oinductions in x converge to the same lattice point.

In order to prove this theorem, we use the following result.

Lemma 3.12. Let N = (xi)i≤β, N ′ = (yi)i≤γ be two safe O-inductions with x0 = y0. For every i ≤ β, j ≤ γ it holds that if i+1 ≤ β then xi+1∨yj is safely derivable from xi∨yj and if j+1 ≤ γ then xi∨yj+1 is safely derivable from xi∨yj . "

Proof of Theorem 3.11. Let N = (xi)i≤β and N ′ = (yi)i≤γ be two safe-terminal O-inductions. Consider the sequence (zi)i≤β+γ where zi = xi if i ≤ β and zβ+i = xβ ∨ yi if i ≤ γ. By Lemma 3.12, this sequence is a safe O-induction. Since N is safe-terminal, this sequence cannot be a strict extension of N and hence xβ ∨yγ = zβ+γ = xβ, i.e., yγ ≤ xβ. A symmetric argument shows that xβ ≤ yγ, hence xβ = yγ, as desired.

Definition 3.13. The safely defined point by O, denoted safe(O) is the limit of all safe-terminal O-inductions in ⊥.

By Theorem 3.11, the safely defined point is well-defined. We now study some properties of the safely defined point.

Proposition 3.14. For any operator O, safe(O) is a postfixpoint of O, i.e., safe(O) ≤ O(safe(O)).

Example 3.15. Consider a lattice {⊥,⊤} with two elements and an operator O that maps ⊥ to ⊤ and ⊤ to ⊥. The safely defined point by O is ⊥, since ⊤ is not safely derivable (⊤ ̸≤ ⊥∨O(⊤)). Here, the O-induction N = (⊥) is safe-terminal, but not terminal. ▲

Definition 3.16. We call an operator O complete if the safely defined point by O is a fixpoint of O, i.e., if O(safe(O)) = safe (O).

We will be mostly interested in complete operators O, as they uniquely determine a fixpoint of interest of O.

Proposition 3.17. An operator O is complete if and only if every safe-terminal O-induction in ⊥ is terminal.

Proposition 3.18. If O is a monotone operator, then O is complete and safe(O) = lfp(O).

Theorem 3.11 shows that safe O-inductions, despite their non-determinism, uniquely determine a lattice point of interest. Furthermore, if O is monotone, this point is the least fixpoint of O. The question now arises: what if O is nonmonotone? How does the safely defined point by O relate to other points of interest? In particular, how does it relate to fixpoints defined in approximation fixpoint theory? We study this in Section 5. First, we study complexity.

Complexity The height of a finite lattice L is the length n of the longest sequence ⊥ = x0 < x1 < · · · < ⊤ = xn in L. We call y ∈ L a direct successor of x ∈ L if x < y and there is no z such that x < z < y. The branching width of a finite L is the maximum over x ∈ L of the number of direct successors of x. All complexity results presented below are in terms of the sum of the branching width and the height of the input lattice. This means that we use the sum of the branching width and the height as the measure of our input.

In this section, we assume that a class C = {〈L,O〉} of pairs of a finite lattice L and an operator O : L → L is given. Let FC denote the function problem: given one of the 〈L,O〉 in C and p, p′ ∈ L, compute (1) O(p), (2) p ∨ p′ , and (3) {x | x is a direct successor of p}. We assume that FC can be solved in polynomial time.

The kind of setting used here is not so unusual: it is an algebraic variant of data complexity. For instance, in logic programming, each non-ground program P determines a class of lattices and associated operators (immediate consequence operators of the groundings of P with respect to a given domain). The height and branching width of the lattice are then polynomial in terms of the domain size. In this setting, the problem FCP is indeed polynomially solvable.

Theorem3.19. Let C be a class as above. The decision problem given Li ∈ C, x, y ∈ Li, is y safely derivable from x by Oi? is in co-NP.

Sketch of the proof. To prove this, we build a program that nondeterministically traverses an O-induction from x. To determine that y is not safely derivable from x, it suffices to find one run of the algorithm such that y ̸≤ x∨O(s) with s a state in in the O-induction. Such algorithm runs in polynomial time in the height of the lattice.

Theorem3.20. Let C be a class as above. The decision problem given 〈L,O〉 ∈ C, s ∈ L, is safe(O) ≥ s? is in (∆P2 ). For some classes C, this problem is co-NP-hard.

Sketch of the proof. Containment follows from Theorem 3.19. Hardness follows from Theorem 6.10 of Denecker et al. [2017].

4 Preliminaries: AFT

Given a lattice L, approximation fixpoint theory makes use of the lattice L2 . We define projections for pairs as usual: (x, y)1 = x and (x, y)2 = y. Pairs (x, y) ∈ L2 are used to approximate all elements in the interval [x, y] = {z | x ≤ z ∧ z ≤ y}. We call (x, y) ∈ L2 consistent if x ≤ y. We use Lc to denote the set of consistent elements. Elements (x, x) ∈ Lc are called exact. We sometimes use the tuple (x, y) and the interval [x, y] interchangeably. The precision ordering on L2 is defined as (x, y) ≤p (u, v) if x ≤ u and v ≤ y. In case (u, v) is consistent, this means that (x, y) approximates all elements approximated by (u, v), or in other words that [u, v] ⊆ [x, y]. If L is a complete lattice, then 〈L2 , ≤p〉 is also a complete lattice.

AFT studies fixpoints of lattice operators O : L → L through operators approximating O. An operator A : L2 → L2 is an approximator of O if it is ≤p-monotone, and O(x) ∈ A(x, x) for all x ∈ L. Approximators map Lc into Lc . As usual, we restrict our attention to symmetric approximators: approximators A such that for all x and y, A(x, y)1 = A(y, x)2. DMT [2004] showed that the consistent fixpoints of interest (defined below) are uniquely determined by an approximator's restriction to Lc , hence, sometimes we only define approximators on Lc .

AFT studies fixpoints of O using fixpoints of A. The AKripke-Kleene fixpoint is the ≤p-least fixpoint of A and has the property that it approximates all fixpoints of O. A partial A-stable fixpoint is a pair (x, y) such that x = lfp(A(·, y)1)

and y = lfp(A(x, ·)2), where A(·, y)1 denotes the operator L → L : x ↦→ A(x, y)1 and analogously for A(x, ·)2. The A-well-founded fixpoint is the least precise partial A-stable fixpoint. An A-stable fixpoint of O is a fixpoint x of O such that (x, x) is a partial A-stable fixpoint. This is equivalent to the condition that x = lfp(A(·, x)1). A-stable fixpoints are minimal fixpoints of O. The A-Kripke-Kleene fixpoint of O can be constructed by iterative applications of A, starting from (⊥, ⊤). For the A-well-founded fixpoint, a similar constructive characterization has been worked out.

Definition 4.1. An A-refinement of (x, y) is a pair (x′ , y′ ) ∈ L2 satisfying one of the following two conditions:

• (x, y) ≤p (x′ , y′ ) ≤p A(x, y), or
• x′ = x and A(x, y′ )2 ≤ y′ ≤ y.

An A-refinement is strict if (x, y) ̸= (x′ , y′ ).

Definition 4.2. A well-founded induction of A is a sequence (xi, yi)i≤β with β an ordinal such that

• (x0, y0) = (⊥,⊤);
• (xi+1, yi+1) is an A-refinement of (xi, yi), for all i < β;
• (xλ, yλ)= ∨≤p {(xi, yi)|i < λ} for limit ordinals λ ≤ β.

A well-founded induction is terminal if its limit (xβ, yβ) has no strict A-refinements.

Denecker and Vennekens [2007] showed that all terminal A-inductions converge to the A-well-founded fixpoint of O.

Logic Programming For logic programming, DMT showed that Fitting's immediate consequence operator ΨP [Fitting, 2002] is an approximator of TP, that the ΨP-wellfounded fixpoint is the well-founded model of P [Van Gelder et al., 1991] and that ΨP-stable fixpoints are the stable models of P [Gelfond and Lifschitz, 1988].

5 Safe Inductions and AFT

In this section, we study how (safe) O-inductions relate to the fixpoints studied in AFT.

Theorem 5.1. Let O be an operator and A an approximator of O. The A-well-founded fixpoint approximates the safely defined point by O.

The proof makes use of the following proposition.

Proposition 5.2. Let O be an operator and A an approximator of O. Let (xi, yi)i≤β be an A-well-founded induction. The following claims hold:

1. (xi)i≤β is a safe O-induction, and
2. for each i ≤ β and eachO-inductionN = (zj)j≤α with z0 = xi, it holds that zα ≤ yβ

Proof of Theorem 5.1. Let z denote the safely defined point of O and let (xβ, yβ) denote the A-well-founded fixpoint of O. For any terminal A-well-founded induction (xi, yi)i≤β, it holds that xβ ≤ z by the first point of Proposition 5.2. Furthermore, by the second point of Proposition 5.2 it holds that any O-induction stays under yβ; hence z ≤ yβ.

Theorem 5.1 has several consequences.

Corollary 5.3. If the A-well-founded fixpoint of O is exact, i.e., equal to (x, x) for some x ∈ L, then O is complete and safe(O) = x.

Corollary 5.4. Let O be an operator and A an approximator of O. The A-Kripke-Kleene fixpoint of O approximates the safely defined point by O.

Corollary 5.5. If the A-Kripke-Kleene fixpoint of O is exact, i.e., equal to (x, x) for some x ∈ L, then O is complete and safe(O) = x.

Safe O-inductions identify a unique lattice point of interest. Since an operator can have multiple stable fixpoints, we cannot expect a strong link between the safely defined point and stable fixpoints. However, we do find the following relation between stable fixpoints and O-inductions.

Theorem 5.6. Let A be an approximator of O. If x is an A-stable fixpoint of O, then x is the limit of a terminal Oinduction.

Sketch of the proof. If x is an A-stable fixpoint of O, then x = lfp(A(·, x)1). The clue to proving this proposition is to show that monotone inductions of A(·, x)1 are O-inductions. The result then easily follows.

Example 5.7. Consider the logic program

It holds that {p} is a stable model of P (a ΨP-stable fixpoint of TP). Also, {p} is the limit of the TP-induction (∅, {p}). This induction is not safe since (∅, {q}) is also a TP-induction and {p} ̸≤ TP({q}) ∨ ∅ = {q}. ▲

The limit of a terminal O induction is not always a stable fixpoint of O (for some approximator A), as we show below.

Example 5.8. Consider the logic program

In this case (∅, {q}, {q, p}) is the unique terminal TPinduction. It can be verified that this is a safe induction and that TP is complete. The safely defined point is a nonminimal fixpoint of TP, hence it is also non-grounded (see [Bogaerts et al., 2015]) and not an A-stable fixpoint for any approximator A of TP. In the well-founded model of P, all atoms are unknown. ▲

6 Safe Inductions and Autoepistemic Logic

Recently Bogaerts et al. [2016] exposed a problem in several semantics of autoepistemic logic (AEL). They showed that for very simple, stratified theories, the well-founded and other semantics fail to identify the intended model. They solved this problem by defining, algebraically, a new constructive semantics that is based on a refined notion of approximations of a lattice point (more refined than intervals, i.e., elements of L2 ). In this section, we show that safe inductions provide a direct solution to the aforementioned problem without the need for any approximation. First, we recall some background on AEL.

6.1 AFT and Autoepistemic Logic

AEL is a non-monotonic logic for modeling the beliefs or knowledge of a rational agent with perfect introspection capabilities [Moore, 1985].

Let L be the language of propositional logic based on a set of atoms Σ. Extending this language with a modal operator K, which is read "I (the agent) know" 1 , yields a language LK of modal propositional logic. An autoepistemic theory is a set of formulas in LK. A crucial assumption about such theories that distinguishes this logic from the standard modal logic S5 is that all of the agent's knowledge is encoded in the theory: it either belongs to the theory, or can be derived from it. Levesque [1990] called this the "all I know assumption".

A modal formula is a formula of the formKψ; an objective formula is a formula without modal subformulas. If ϕ is a formula, At(ϕ) denotes the set of all atoms that occur in ϕ and AtO(ϕ) the set of all atoms that occur objectively in ϕ, i.e., outside of the scope of an operator K.

An interpretation is a subset of Σ. A possible world structure is a set of interpretations. A possible world structure can be seen as a Kripke structure in which the accessibility relation is total. The set of all possible world structures is denoted WΣ; it forms a lattice with the knowledge order ≤k such that Q ≤k Q′ iff Q ⊇ Q′ . A possible world structure Q is a mathematical object to represent all situations that are possible according to the agent: interpretations q ∈ Q represent possible states of affairs, i.e., states of affairs consistent with the agent's knowledge, and interpretations q ̸∈ Q represent impossible states of affairs, i.e., states of affairs that violate the agent's knowledge.

If ϕ is a formula in LK, Q is a possible world structure and I is an interpretation, satisfaction of ϕ with respect to Q and I (denoted Q, I |= ϕ) is defined as in the modal logic S5 by the standard recursive rules of propositional satisfaction augmented with one additional rule:

In this formula, Q represents the belief of the agent and I represents the actual state of the world. Modal formulas are evaluated with respect to the agent's belief, while objective formulas are evaluated with respect to the state of the actual world. We furthermore define Q |= Kϕ (ϕ is known in Q) if Q, I |= ϕ for every I ∈ Q. Moore [1985] associated with every theory T an operator DT onWΣ as follows:

The intuition behind this operator is that DT (Q) is a revision of Q consisting of all worlds that are consistent with the agent's current beliefs (Q) and the constraints in T .

DMT [2003] defined approximators for DT and showed that AFT induces all main and some new semantics for AFT.

Monotonically Stratified AEL Theories Following Vennekens et al. [2006], we call an autoepistemic theory T stratifiable 2 w.r.t. a partition (Σi)0≤i≤n of its alphabet if there exists a partition (Ti)0≤i≤n of T such that for each i, AtO(Ti) ⊆ Σi and At(Ti) ⊆ ⋃0≤j≤i Σj. This notion of stratification significantly extends the notion from Marek and Truszczy´nski [1991]. A stratification is modally separated if for every modal subformula Kψ of Ti, either At(ψ) ⊆ Σi or At(ψ) ⊆ ⋃0≤j<i Σj .

1 Or, following DMT [2011] "My knowledge entails".

2 As mentioned in the introduction, we restrict to finite stratifications here.

Let Σ1 and Σ2 be two disjoint vocabularies. If Q1 and Q2 are possible world structures over Σ1 and Σ2 respectively, then the extension of Q1 by Q2 is the possible world structure over Σ1 ∪Σ2 defined as Q1 ⊕Q2 def = {I1∪I2 | I1 ∈ Q1∧I2 ∈ Q2}. If Q is a possible world structure over Σ1 ∪ Σ2, the restriction of Q to Σ1 is Q|Σ1 def = {I ∩Σ1 | I ∈ Q}.

DMT [2011] have made strong arguments in favor of a constructive semantics for AEL. Bogaerts et al. [2016], however, showed that the two constructive semantics induced by AFT (well-founded and Kripke-Kleene semantics) are too weak for AEL. They gave the following example.

Example 6.1. Consider the autoepistemic theory

The informal reading of this theory is as follows: I (an introspective autoepistemic agent) only know the following: q holds iff I do not know p and r holds iff I do not know q.

Since p does not occur objectively in T , an agent who only knows T does not have any information about p. Thus, in the intended model, it knows neither p nor ¬p, i.e., ¬Kp and ¬K¬p must hold in the intended model. The first sentence then entails q, hence Kq must hold. Now, the last sentence implies ¬r; the intended model is thus {{p, q}, {q}}, the unique possible world structure in which ¬Kp, ¬K¬p,Kq, and K¬r hold. ▲

Bogaerts et al. [2016] showed that the well-founded semantics (for any approximator) fails to identify the intended model in the above example. They generalized this example to the class of monotonically stratified theories and defined a notion of perfect model for them.

Definition 6.2. We say that T is monotonically stratified with respect to a partition (Σi)0≤i≤n of its alphabet if there is a modally separated stratification (Ti)0≤i≤n of T such that all subformulas Kψ of Ti with At(ψ) ⊆ Σi occur negatively (in the scope of an odd number of negations) in Ti.

The construction of the perfect model of an autoepistemic theory is as follows. In a monotonically stratified theory, each theory Ti defines knowledge of the symbols in Σi in terms of knowledge of symbols in lower strata (Σj with j < i). The last condition guarantees that for a fixed interpretation of the knowledge of lower strata, DTi is a monotone operator and hence its intended fixpoint is clear. The perfect model of T is then constructed by iterated monotone inductions, each of them computing the knowledge of symbols in Σi based on the knowledge of symbols in lower strata. In the example above, first ignorance of p is established; next, knowledge of q is established and in the final stage, knowledge of ¬r is concluded. This construction was formalized as follows.

Proposition 6.3 (Proposition 3.3 from Bogaerts et al. [2016]). Let (Ti)0≤i≤n be a monotonic stratification of T w.r.t.

(Σi)0≤i≤n. For some i, let Qi-1 be a possible world structure over ⋃j<i Σj. The operator Di : WΣi → WΣi : Q ↦→ DTi (Q⊕Qi-1)|Σi is monotone.

Definition 6.4. Let T be a monotonically stratified autoepistemic theory and (Ti)0≤i≤n a monotonic stratification of T . The perfect model of T (denoted pm(T )) is defined by induction on n.

• If n = 0, then DT is monotone and the perfect model of T is the least fixpoint of DT .
• Otherwise, let Qn-1 denote pm(⋃j<n Tj) and let Dn be as in Proposition 6.3; in this case we define pm(T ) as lfp(Dn) ⊕Qn-1.

In general, the construction of the perfect model may not always work as expected. Bogaerts et al. [2016] defined a criterion that guarantees that this construction behaves nicely, called weak permaconsistency.

Definition 6.5. An autoepistemic theory T is called weakly permaconsistent if for every possible world structure Q, there is at least one I such that Q, I |= T .

This resulted in a "sanity criterion" for semantics of autoepistemic logic as follows.

Definition 6.6. We say that a semantics for autoepistemic logic respects stratification if all weakly permaconsistent monotonically stratified theories have exactly one model, namely their perfect model.

6.2 AEL and Safe Inductions

Here, we show that the safely defined point of DT manages to identify the fixpoint of interest for Example 6.1 and that this result generalizes: the safely defined semantics (defined formally below) respects stratification. This result shows that safe inductions can identify the perfect model, without prior information on the stratification and without the need for any form of approximation. Even stronger, the perfect model construction is a terminal safe induction.

Definition 6.7. The safely defined semantics is given by Q |=sd T if Q = safe(DT ) and DT is complete.

The condition that DT is complete has as effect here that the safely defined model of T must be a fixpoint of DT . In other words, the knowledge of the agent must be such that it can no longer be revised by the revision operator.

Example 6.8 (Example 6.1 continued). A first observation is that there are no possible world structures Q such that DT (Q) |= Kp or DT (Q) |= K¬p. Hence, if N = (Qi)i≤β is a DT -induction in ⊥ = 2{p,q,r} , it also has the property that Qi ̸|= Kp and Qi ̸|= K¬p for each i. For each Qi, it then holds that DT (Qi) |= Kq. From this it follows that Qq := {{p, q}, {q}, {p, q, r}, {q, r}}, the ≤k-least possible world structure in which Kq holds, is safely derivable from ⊥. Now, for every possible world structure Q ≥k Qq, it holds that DT (Q) |= K¬r. Thus, this also holds for all possible world structures in a DT -induction from Qq. Hence, it follows that {{p, q}, {q}} is safely derivable fromQq. Since this is a fixpoint of DT , the safe DT -induction

is terminal and hence also safe-terminal. Thus, the perfect model of T is indeed the safely defined point by DT . ▲

We now give a sketch of the proof that the above example is not a coincidence, i.e., that it generalizes to the class of monotonically stratified theories.

Theorem 6.9. The safely defined semantics respects stratification. That is: for each monotonically stratified theory T : if T is weakly permaconsistent, then DT is complete and safe(DT ) is the perfect model of T .

The proof of this theorem makes use of the following two results.

Lemma 6.10. Suppose (Ti)0≤i≤n is a monotone stratification of T w.r.t. (Σi)0≤i≤n. Let Σ′i denote ⋃j≤i Σj for each i. For every possible world structure Q it holds that

Lemma 6.11. Suppose T is monotonically stratified w.r.t. (Σi)0≤i≤n. Furthermore suppose T is weakly permaconsistent. Let Σ′i denote ⋃j≤i Σi for each i. If Q1 and Q2 are two possible world structures such that Q1|Σ′i = Q2|Σ′i , then also DT (Q1)|Σ′i = DT (Q2)|Σ′i .

Lemma 6.10 shows howDT is composed from the various DTi . Lemma 6.11 states that if two possible world structures agree on the lower strata, then so does their image under DT for any weakly permaconsistent theory T . In other words: the knowledge of symbols in a given stratum in DT (Q) only depends on the knowledge of symbols of smaller (or equal) strata in Q.

Sketch of the proof of Theorem 6.9. The central idea in this proof is to turn the construction of the perfect model into a safe DT -induction. To show that it is a DT -induction and to show that it is safe, we repeatedly exploit the fact that if Q agrees with pm(T ) on all strata below i, so does DT (Q).

Completeness follows from the fact that we find a safe DT induction whose limit is the perfect model of T . Since this model is a fixpoint of DT , this induction is terminal and DT is indeed complete.

7 Conclusion

In this paper, we presented the notions of O-inductions and safe O-inductions for a lattice operator O. We studied how they relate to various fixpoints of O studied in AFT. We studied the semantics induced by these inductions in the context of autoepistemic logic, where we find that the safely defined point has interesting properties for a class of operators. It is a topic of future work to study the semantics induced by safe inductions for other application domains of AFT, such as abstract argumentation [Dung, 1995] and active integrity constraints [Flesca et al., 2004; Cruz-Filipe, 2016], where we conjecture that safe inductions will prove helpful to tackle the problems with the well-founded semantics such as Example 18 of Cruz-Filipe [2016].