Using SAT and Partial MaxSAT for Reasoning with System Z and
                         System W
                         Christoph Beierle1 , Aron Spang1 and Jonas Haldimann1,2,3
                         1
                           Knowledge Based Systems, FernUniversität in Hagen, 58084 Hagen, Germany
                         2
                           Institute of Logic and Computation, TU Wien, 1040 Vienna, Austria
                         3
                           University of Cape Town and CAIR, Cape Town, South Africa


                                         Abstract
                                         Nonmonotonic reasoning from conditional belief bases typically depends on a structure over possible worlds that relies on the verifi-
                                         cation and falsification of conditionals. A major challenge in implementing such reasoning approaches is that the number of worlds
                                         in these structures grows exponentially with the number of propositional variables occurring in the belief base. For addressing this
                                         problem by using the power of current solvers, recently an implementation of reasoning with system W using Partial MaxSAT prob-
                                         lems has been proposed. In this paper, we investigate this approach in more detail, present a formal correctness proof of the system W
                                         inference algorithm SWinf , and extend its empirical evaluation. Furthermore, we show that the approach can be transferred to imple-
                                         menting Pearl’s system Z by using SAT problems, and prove the correctness of the resulting system Z inference algorithm SZinf . Our
                                         implementations of system Z and system W demonstrate that they outperform previous implementations and allow for signature and
                                         knowledge base sizes that have been infeasible before.


                         1. Introduction                                                                                                 • We give a correctness proof for our system Z infer-
                                                                                                                                           ence algorithm SZinf.
                         Conditionals play a major role in knowledge representa-                                                         • We implement system Z correspondingly, outper-
                         tion and reasoning, and many different semantics have been                                                        forming previous implementations and allowing for
                         proposed for conditional belief bases, like probability dis-                                                      signature and knowledge base sizes that have not
                         tributions, plausibility orderings, possibility distributions,                                                    been possible before.
                         ranking functions and special instances of them, or condi-
                         tional objects (see, e.g., [1, 2, 3, 4, 5, 6, 7, 8]). However, soft-                                          This paper is organized as follows. After briefly recalling
                         ware systems implementing any of these inference methods                                                   the background on conditional logic in Section 2 and sys-
                         have attracted much less attention. Any such implementa-                                                   tem W in Section 3, we present and illustrate our algorithm
                         tion of inference with respect to a conditional belief base Δ                                              SWinf for system W in Section 4 and prove its correctness
                         has to cope with the number of worlds growing exponen-                                                     in Section 5. We adapt this approach for system Z in Sec-
                         tially with the number of propositional variables occurring                                                tion 6, illustrate the resulting algorithm SZinf and prove
                         in Δ. For addressing this practical side of nonmonotonic                                                   this algorithm’s correctness in Section 7. Finally we evalu-
                         reasoning, we consider Pearl’s well-known system Z [9],                                                    ate the runtimes of our new algorithms for system W and
                         and system W [10] that exhibits some notable properties like                                               system Z in Section 8 before concluding and pointing out
                         extending system Z and thus rational closure [11], avoid-                                                  future work in Section 9.
                         ing the drowning problem [12], and fully complying with
                         syntax splitting [13, 14] and also with conditional syntax
                         splitting [15]. Because the first implementation of system W                                               2. Background: Conditional Logic
                         [16] severely limits the number of propositional variables
                                                                                                                                    A (propositional) signature is a finite set Σ of propositional
                         in Δ to about 20 for practical applications, corresponding
                                                                                                                                    variables, and ℒΣ denotes the propositional language over Σ.
                         to about one million worlds, recently an implementation of
                                                                                                                                    We may denote a conjunction 𝐴 ∧ 𝐵 by 𝐴𝐵 and a negation
                         reasoning with system W using partial MaxSAT problems
                                                                                                                                    ¬𝐴 by 𝐴. The set of interpretations over a signature Σ,
                         has been developed, with first evaluation results of up to 60
                                                                                                                                    also called worlds, is ΩΣ . We may identify a world with
                         variables and thus 260 worlds [17].
                                                                                                                                    the corresponding complete conjunction of all elements Σ
                            This paper extends our work presented in [17] in several
                                                                                                                                    in either positive or negated form. An 𝜔 ∈ ΩΣ is a model
                         directions, providing the following main contributions:
                                                                                                                                    of 𝐴 ∈ ℒΣ if 𝐴 holds in 𝜔, denoted as 𝜔 |= 𝐴, and the
                                • We elaborate the approach in [17] in more detail and                                              set of models of 𝐴 is Mod Σ (𝐴) = {𝜔 ∈ ΩΣ | 𝜔 |= 𝐴},
                                  provide a formal correctness proof for its system W                                               sometimes denoted as Ω𝐴 . A formula 𝐴 entails a formula 𝐵,
                                  inference algorithm SWinf.                                                                        written 𝐴 |= 𝐵, if Mod Σ (𝐴) ⊆ Mod Σ (𝐵). Furthermore,
                                • We extend its empirical evaluation, demonstrating                                                 for 𝐹 ∈ ℒΣ and 𝑀 ⊆ ℒΣ , we use the notation 𝜔 |= 𝑀 iff
                                  that it scales up system W inference up to 120 vari-                                              𝜔 |= 𝐹𝑖 for every 𝐹𝑖 ∈ 𝑀 ; Ω𝑀 = {𝜔 ∈ ΩΣ | 𝜔 |= 𝑀 };
                                  ables and thus 2120 worlds and to belief bases of up                                              𝑀 = {𝐹 𝑖 | 𝐹𝑖 ∈ 𝑀 }; and 𝐹 ∧ 𝑀 = 𝐹 ∧ 𝐹1 ∧ . . . ∧ 𝐹𝑚
                                  to 200 conditionals.                                                                              for 𝑀 = {𝐹1 , . . . , 𝐹𝑚 }.
                                • We show how the approach can be transferred, yield-                                                  A conditional (𝐵|𝐴) connects two formulas 𝐴, 𝐵 and
                                  ing a SAT-based realization of system Z.                                                          represents the rule “If 𝐴 then usually 𝐵”. The conditional
                          22nd International Workshop on Nonmonotonic Reasoning, November 2-                                        language over Σ is (ℒ|ℒ)Σ = {(𝐵|𝐴) | 𝐴, 𝐵 ∈ ℒΣ }. A
                          4, 2024, Hanoi, Vietnam                                                                                   belief base Δ is a finite set of conditionals. For a world
                              christoph.beierle@fernuni-hagen.de (C. Beierle);                                                      𝜔, a conditional (𝐵|𝐴) is either verified by 𝜔 if 𝜔 |= 𝐴𝐵,
                          aron.spang@fernuni-hagen.de (A. Spang); jonas@haldimann.de                                                falsified by 𝜔 if 𝜔 |= 𝐴𝐵, or not applicable to 𝜔 if 𝜔 |= 𝐴
                          (J. Haldimann)
                                                                                                                                    [18]. An example for semantics of conditionals are functions
                           0000-0002-0736-8516 (C. Beierle); 0000-0002-2618-8721
                          (J. Haldimann)                                                                                            𝜅 : ΩΣ → N such that 𝜅(𝜔) = 0 for at least one 𝜔 ∈
                                     © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License   ΩΣ , called ranking functions or ordinal conditional functions
                                     Attribution 4.0 International (CC BY 4.0).



CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
(OCF), introduced (in a more general form) by Spohn (1988).                                       𝑏𝑝𝑓 𝑤         𝑏𝑝𝑓 𝑤
They express degrees of plausibility where a lower degree
denotes “less surprising”. Each 𝜅 uniquely extends to a                            𝑏𝑝𝑓 𝑤
function 𝜅 : ℒΣ → N ∪ {∞} with 𝜅(𝐴) = min{𝜅(𝜔) |
                                                                                   𝑏𝑝𝑓 𝑤          𝑏𝑝𝑓 𝑤         𝑏𝑝𝑓 𝑤
𝜔 |= 𝐴} where min ∅ = ∞. A ranking function 𝜅 accepts
a conditional (𝐵|𝐴), written 𝜅 |= (𝐵|𝐴), if 𝜅(𝐴𝐵) <                                       𝑏𝑝𝑓 𝑤          𝑏𝑝𝑓 𝑤
𝜅(𝐴𝐵), and 𝜅 accepts Δ, written 𝜅 |= Δ, if 𝜅 accepts all
conditionals in Δ, and Δ is consistent if there is a ranking                       𝑏𝑝𝑓 𝑤          𝑏𝑝𝑓 𝑤         𝑏𝑝𝑓 𝑤
function accepting Δ. Every 𝜅 induces a nonmonotonic
inference relation |∼ 𝜅 between formulas in ℒΣ , given by
                                                                           𝑏𝑝𝑓 𝑤       𝑏𝑝𝑓 𝑤      𝑏𝑝𝑓 𝑤      𝑏𝑝𝑓 𝑤      𝑏𝑝𝑓 𝑤
       𝐴 |∼ 𝜅 𝐵 iff 𝐴 ≡ ⊥ or 𝜅(𝐴𝐵) < 𝜅(𝐴𝐵).                     (1)
                                                                      Figure 1: The preferred structure on worlds <wΔbird in Example 1.
                                                                      An edge 𝜔 → 𝜔 ′ indicates that 𝜔 <w         ′
                                                                                                           Δbird 𝜔 ; edges that can be
3. System W                                                           obtained from transitivity are omitted.

An inductive inference operator completes an explicitly
given belief base to the inference relation representing all
conditional beliefs an agent can derive [13]. One such infer-         Example 1 (Δbird ). Let Σ = {𝑏, 𝑝, 𝑓, 𝑤} represent
ence operator is System W [19, 10] which takes into account           birds, penguins, flying things and winged things, and let
the tolerance information expressed by the Z-partition (also          Δbird contain 𝑟1 = (𝑓 |𝑏), 𝑟2 = (𝑓 |𝑝), 𝑟3 = (𝑏|𝑝), and
called ordered partition) of a belief base Δ, defined in the          𝑟4 = (𝑤|𝑏). E.g., 𝑟1 expresses “birds usually fly”. Then
following.                                                            OP (Δbird ) = (Δ0 , Δ1 ) with Δ0 = {(𝑓 |𝑏), (𝑤|𝑏)} and
                                                                      Δ1 = {(𝑓 |𝑝), (𝑏|𝑝)}. Using <wΔbird (Figure 1), we can check
Definition 1 (Z-partition OP (Δ) [9]). Let Δ =                        that 𝑝 |∼ wΔbird 𝑤 holds, i.e., that penguins usually have
{(𝐵1 |𝐴1 ), . . . , (𝐵𝑛 |𝐴𝑛 )} be a belief base. A conditional        wings is a system W inference in the context of Δbird .
(𝐵|𝐴) is tolerated by a set of conditionals Δ if there exists a
world 𝜔 ∈ ΩΣ that verifies (𝐵|𝐴) and does⋀︀not falsify any               System W captures system Z in the sense that every en-
conditional in Δ, i.e., 𝜔 |= 𝐴𝐵 and 𝜔 |= 𝑛                            tailment that is possible with system Z is also possible with
                                                 𝑖=1 (𝐴𝑖 ∨ 𝐵𝑖 ).
The Z-partition OP (Δ) = (Δ0 , . . . , Δ𝑘 ) of a belief base Δ        system W, i.e., the system W inferences of a belief base Δ
is the partition of Δ where each⋃︀Δ𝑖 is the (with respect to set      are a superset of the system Z inferences of Δ. Further-
inclusion) maximal subset of 𝑘𝑗=𝑖 Δ𝑗 that is tolerated by             more, there are belief bases where this superset relationship
⋃︀𝑘      𝑗                                                            is strict, i.e., where system W licenses strictly more infer-
   𝑗=𝑖 Δ .                                                            ences than system Z [10]. System W strictly extends also
   It is well-known that OP (Δ) exists iff Δ is consistent;           c-inference [21, 10]; further properties of system W and its
moreover, because the Δ𝑖 are chosen inclusion-maximal,                relationshsips to other inductive inference operators are
the Z-partition is unique [20]. System W combines the                 described in [22, 23, 24].
Z-partition with the structural information about which                  For a set 𝑀 and a partial order < on 𝑀 , the minimal
conditionals are falsified by a world, yielding the preferred         elements of 𝑁 ⊆ 𝑀 are denoted by: min(𝑁, <) = {𝑛 ∈
structure on worlds <wΔ underlying system W.                          𝑁 | there is no 𝑛′ ∈ 𝑁 s.t. 𝑛′ < 𝑛}. Because <wΔ is a strict
                                                                      partial order [10], Definition 3 directly implies that is suf-
Definition 2 (𝜉 𝑗 , preferred structure <wΔ on worlds                 fices to consider only the <wΔ -minimal worlds for checking
[19, 10]). Let Δ = {(𝐵1 |𝐴1 ), . . . , (𝐵𝑛 |𝐴𝑛 )} with                whether |∼ wΔ holds.
OP (Δ) = (Δ0 , . . . , Δ𝑘 ). For 𝑗 = 0, . . . , 𝑘, the function 𝜉 𝑗
maps worlds to the set of falsified conditionals from the set         Proposition 1 (|∼ wΔ ). Let Δ be a consistent belief base and
Δ𝑗 :                                                                  𝐴, 𝐵 ∈ ℒΣ . Then

              𝜉 𝑗 (𝜔) := {𝑟𝑖 ∈ Δ𝑗 | 𝜔 |= 𝐴𝑖 𝐵𝑖 },               (2)         𝐴 |∼ wΔ 𝐵 iff for every 𝜔 ′ ∈ min(Ω𝐴𝐵 , <wΔ )
                                                                                          there is an 𝜔 ∈ min(Ω𝐴𝐵 , <wΔ )
The preferred structure on worlds is the binary relation <wΔ                              such that 𝜔 <wΔ 𝜔 ′ .
defined by, for 𝜔, 𝜔 ′ ∈ ΩΣ :

𝜔 <wΔ 𝜔 ′ iff there exists 𝑚 ∈ {0 , . . . , 𝑘} such that              4. Algorithm SWinf : System W
                 𝑖          𝑖   ′
                𝜉 (𝜔) = 𝜉 (𝜔 ) ∀𝑖 ∈ {𝑚 + 1 , . . . , 𝑘}, and             Inference using MaxSAT
                𝜉 𝑚 (𝜔) ⫋ 𝜉 𝑚 (𝜔 ′ ) .                          (3)   In this section we introduce the algorithm SWinf(Δ, 𝐴, 𝐵)
                                                                      (system W inference with Partial MaxSAT, Algorithm 1)
   Thus, 𝜔 <wΔ  𝜔 if and only if 𝜔 falsifies strictly fewer
                     ′
                                                                      [17] which takes a belief base Δ and two formulas 𝐴, 𝐵 as
conditionals than 𝜔 ′ in the partition with the biggest index
                                                                      input and answers the question whether 𝐴 |∼ wΔ 𝐵 holds.
𝑚 where the conditionals falsified by 𝜔 and 𝜔 ′ differ.
                                                                      Implementing system W by computing the relation <wΔ
Definition 3 (system W, |∼ wΔ [10]). Let Δ be a consistent            [16] will work for small signatures but does not scale well
belief base and let 𝐴, 𝐵 ∈ ℒΣ be formulas. Then 𝐵 is a                because of the number of worlds to be considered grows
system W inference from 𝐴 (in the context of Δ), denoted              exponentially with the size of the signature. Therefore, we
𝐴 |∼ wΔ 𝐵, if we have:                                                will employ Partial MaxSAT concepts [25] in SWinf and
                                                                      utilize the power of current SAT-solvers. Given a set of
         for every 𝜔 ′ ∈ Ω𝐴𝐵                                          formulas 𝑆 of soft constraints and a set of formulas 𝐻 of
                                                                (4)   hard constraints the extended partial maximum satisfiability
            there is an 𝜔 ∈ Ω𝐴𝐵 such that 𝜔 <wΔ 𝜔 ′ .
Algorithm 1 SWinf(Δ, 𝐴, 𝐵)                                        𝜔 <wΔ 𝜔 ′ or 𝜔 ̸<wΔ 𝜔 ′ holds after considering 𝜉 𝑗 ; only in
Input: consistent belief base Δ and formulas 𝐴, 𝐵                 case that 𝜉 𝑙 (𝜔) = 𝜉 𝑙 (𝜔 ′ ) for all 𝑙 ∈ {𝑗, . . . , 𝑘} we continue
Output: Yes if 𝐴 |∼ wΔ 𝐵, and No otherwise                        by considering the next lower element Δ𝑗−1 .
                       0        𝑘
  1: let OP (Δ) = (Δ , . . . , Δ )                                   Assume we have Δ with OP (Δ) = (Δ0 , . . . , Δ𝑘 ). The
  2: function recWinf (𝑗, 𝐻)
                                                                  central part of SWinf is the recursive function recWinf
                         𝑗
  3: 𝒱 ← MCS (nf (Δ ), 𝐻 ∪ {𝐴𝐵})
                                                                  that takes the index for one of the sets in the Z-partition
                         𝑗
  4: ℱ ← MCS (nf (Δ ), 𝐻 ∪ {𝐴𝐵})
                                                                  and a set of formulas as arguments. It is initially called
                ′                      ′                          for the last part Δ𝑘 of the Z-partition. Each set in 𝒱 =
  5: if ¬(∀𝑁 ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ) then
                                                                  MCS (nf (Δ𝑘 ), {𝐴𝐵}) corresponds to a maximal selection
  6:     return No
                                                                  of conditionals in Δ𝑘 such that there is a model of 𝐴𝐵
  7: for all 𝑁 ∈ 𝒱 ∩ ℱ do                                         not falsifying them, and thus to a selection of worlds that
  8:     if 𝑗 = 0 then                                            falsify a minimal set of conditionals in Δ𝑘 . Analogously,
  9:       return No                                              this holds for ℱ = MCS (nf (Δ𝑘 ), {𝐴𝐵}) and 𝐴𝐵. If there
 10:     𝐻new ← (nf (Δ𝑗 ) ∖ 𝑁 ) ∪ 𝑁                               is an 𝑁 ∈ ℱ for which there is no 𝑁 ′ ∈ 𝒱 with 𝑁 ⊆ 𝑁 ′ ,
 11:     if recWinf (𝑗 − 1, 𝐻 ∪ 𝐻new ) = No then                  there is a world 𝜔 ′ ∈ Mod Σ (𝐴𝐵) for which there is no
 12:       return No                                              world 𝜔 ∈ Mod Σ (𝐴𝐵) with 𝜉 𝑘 (𝜔) ⊆ 𝜉 𝑘 (𝜔 ′ ). Thus, if the
 13: return Yes                                                   condition in Line 5 holds, we have that 𝐴 ̸|∼ wΔ 𝐵. Otherwise,
 14: end function                                                 we continue to consider the intersection 𝒱 ∩ ℱ. Each set
 15: return recWinf (𝑘, ∅)                                        𝑁 ∈ 𝒱 ∩ ℱ corresponds to a selection of conditionals that
                                                                  is a minimal set of falsified conditionals in Δ𝑘 both for
                                                                  some models of 𝐴𝐵 and 𝐴𝐵. If there is no such 𝑁 , then
problem EPMaxSAT (𝑆, 𝐻) is the optimization problem of            all inclusions we considered in Line 5 are strict inclusions
maximizing the number of satisfied formulas in 𝑆 over all         and we have 𝐴 |∼ wΔ 𝐵. Otherwise, for each such 𝑁 we
interpretations 𝜔 ∈ Ω𝐻 and determining all subsets of 𝑆           need to consider the parts of the Z-partition with lower
that are maximal with this property.                              indices to check whether for each world 𝜔 ′ ∈ Mod Σ (𝐴𝐵)
                                                                  that falsifies the conditionals in 𝑁 there is a world 𝜔 ∈
Definition 4 (MCS (𝑆, 𝐻)). Let 𝑆 = {𝑆1 , . . . , 𝑆𝑠 } ⊆ ℒΣ        Mod Σ (𝐴𝐵) that falsifies the conditionals in 𝑁 . To do this,
be a set of formulas called soft constraints, and let 𝐻 =         we add (nf Δ𝑘 ∖ 𝑁 ) ∪ 𝑁 as hard constraints to fix the
{𝐻1 , . . . , 𝐻ℎ } ⊆ ℒΣ be a set of formulas called hard con-     falsification behaviour on Δ𝑘 and call the function recWinf
straints. A maximal satisfiable subset (MSS) with respect to      recursively.
(𝑆, 𝐻) is a set 𝑀 ⊆ 𝑆 such that 𝑀 ∪ 𝐻 is (classically) con-
                                                                  Example 3. Executing SWinf(Δbird , 𝑝, 𝑤) results in two
sistent and for every 𝑀 ′ ⊆ 𝑆 with 𝑀 ⫋ 𝑀 ′ the set 𝑀 ′ ∪ 𝐻
                                                                  successive calls of recWinf involving the following values
is not consistent. A set 𝑁 ⊆ 𝑆 is a minimal correction subset
                                                                  and conditions, cf. Example 2:
(MCS) with respect to (𝑆, 𝐻) if 𝑆 ∖𝑁 is an MSS w.r.t. (𝑆, 𝐻).
Then, MCS (𝑆, 𝐻) denotes the set of all MCS w.r.t. (𝑆, 𝐻).                recWinf (𝑗 = 1, 𝐻 = ∅)
                                                                          𝒱 = {∅}
  For using the concepts of MSS and MCS in our context,
                                                                          ℱ = {∅}
we rely in particular on the non-falsification of conditionals.
                                                                          (∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ ) = true
For a conditional (𝐵|𝐴), the formula 𝐴 ∨ 𝐵 expressing its
                                                                          𝒱 ∩ ℱ = {∅}
non-f alsification is denoted by nf (𝐵|𝐴), and nf is extended
                                                                          𝑗=1>0
canonically to a set Δ of condtionals. Thus
                                                                          return Yes iff recWinf (0, {𝑝 ∨ 𝑓 , 𝑝 ∨ 𝑏}) =
             nf (Δ) = {𝐴 ∨ 𝐵 | (𝐵|𝐴) ∈ Δ}                                 Yes

             nf (Δ) = {𝐴𝐵 | (𝐵|𝐴) ∈ Δ}                                    recWinf (𝑗 = 0, 𝐻 = {𝑝 ∨ 𝑓 , 𝑝 ∨ 𝑏})
                                                                          𝒱 = {{𝑏 ∨ 𝑓 }}
are the sets of non-falsifying and falsifying formulas, respec-           ℱ = {{𝑏 ∨ 𝑓, 𝑏 ∨ 𝑤}}
tively, for the conditionals in Δ.                                        (∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ ) = true
                                                                          𝒱 ∩ ℱ = ∅ → return Yes
Example 2. Let Δbird and OP (Δbird ) = (Δ0 , Δ1 ) as
in Example 1. For 𝑆 = nf (Δ1 ) and 𝐻 = {𝑝𝑤} we get                   Thus, SWinf(Δbird , 𝑝, 𝑤) returns Yes, and 𝑝 |∼ wΔbird 𝑤.
MSS (nf (Δ1 ), {𝑝𝑤}) = MSS ({𝑝 ∨ 𝑓 , 𝑝 ∨ 𝑏}, {𝑝𝑤}) =                 When asking whether 𝑤 can be inferred from 𝑝 in the con-
{{𝑝 ∨ 𝑓 , 𝑝 ∨ 𝑏}}, and thus MCS (nf (Δ1 ), {𝑝𝑤}) = {∅}.           text of Δbird with system W, SWinf(Δbird , 𝑝, 𝑤) yields No:
For 𝑆 = nf (Δ0 ) and 𝐻 = nf (Δ1 ) ∪ {𝑝𝑤} we get
                                                                          recWinf (𝑗 = 1, 𝐻 = ∅)
          MSS (nf (Δ0 ), nf (Δ1 ) ∪ {𝑝𝑤})                                 𝒱 = {∅}
                                                                          ℱ = {∅}
        =MSS ({𝑏 ∨ 𝑓, 𝑏 ∨ 𝑤}, {𝑝 ∨ 𝑓 , 𝑝 ∨ 𝑏, 𝑝𝑤})                        (∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ ) = true
        ={{𝑏 ∨ 𝑤}}                                                        𝒱 ∩ ℱ = {∅}
                                                                          𝑗=1>0
and thus MCS (nf (Δ0 ), nf (Δ1 ) ∪ {𝑝𝑤}) = {{𝑏 ∨ 𝑓 }}.                    return Yes iff recWinf (0, {𝑝 ∨ 𝑓 , 𝑝 ∨ 𝑏}) =
                                                                          Yes
   In addition to using the minima as in Proposition 1 for
computing |∼ wΔ , SWinf exploits the fact that the under-                 recWinf (𝑗 = 0, 𝐻 = {𝑝 ∨ 𝑓, 𝑝 ∨ 𝑏})
lying relation 𝜔 <wΔ 𝜔 ′ (cf. Equation (2)) can be deter-                 𝒱 = {{𝑏 ∨ 𝑓, 𝑏 ∨ 𝑤}}
mined by iteratively considering the subbases in OP (Δ) =                 ℱ = {{𝑏 ∨ 𝑓 }}
(Δ0 , . . . , Δ𝑘 ) starting from the the highest partition el-            (∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ ) = false →
ement Δ𝑘 . If 𝜉 𝑗 (𝜔) ̸= 𝜉 𝑗 (𝜔 ′ ) we can decide whether                 return No
5. Correctness Proof for SWinf                                           Lemma 2 describes conditions on sets of falsified condi-
                                                                      tionals that require a certain set 𝑆 to be in 𝒱 ∩ ℱ .
An important characteristic of the search space of the al-
gorithm SWinf is described by the falsification and non-              Lemma 2. Let Δ be a consistent belief base with OP (Δ) =
falsification behaviour of the conditionals in Δ𝑗+1 ∪· · ·∪Δ𝑘         (Δ0 , . . . , Δ𝑘 ), let 𝑗 ∈ {0, . . . , 𝑘}, 𝐴, 𝐵 ∈ ℒΣ , and let 𝐻
for a given 𝑗 ∈ {0, . . . , 𝑘}. For formally characterizing this      be an nf/f -condition for (Δ, 𝑗). Let
behaviour we use the following notion.
                                                                                  𝒱 = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}) and
Definition 5 (nf/f -condition for (Δ, 𝑗)). Let OP (Δ) =
                                                                                 ℱ = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}).
(Δ0 , . . . , Δ𝑘 ), and let 𝑗 ∈ {0, . . . , 𝑘}. A set of formulas 𝐻
is a non-falsifying/falsifying condition (nf/f -condition) for        Let 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) such that there is no
(Δ, 𝑗) if there are, for 𝑖 ∈ {𝑗 +1, . . . , 𝑘} sets Δ𝑖nf , Δ𝑖f ⊆ Δ𝑖   𝜔 * ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜉 𝑗 (𝜔 * ) ⫋ 𝜉 𝑗 (𝜔),
such that Δ𝑖 = Δ𝑖nf ∪ Δ𝑖f and Δ𝑖nf ∩ Δ𝑖f = ∅, and                     and let 𝜔 ′ ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) such that there is no
                       ⋃︁                                             𝜔 ′* ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜉 𝑗 (𝜔 ′* ) ⫋ 𝜉 𝑗 (𝜔 ′ ). Then
            𝐻=                    nf (Δ𝑖nf ) ∪ nf (Δ𝑖f )              𝜉 𝑗 (𝜔) = 𝜉 𝑗 (𝜔 ′ ) implies that there is an 𝑆 ∈ 𝒱 ∩ ℱ with
                  𝑖∈{𝑗+1,...,𝑘}                                       𝜔, 𝜔 ′ |= nf (Δ𝑗 ) ∖ 𝑆.

   Thus, an nf/f -condition 𝐻 for (Δ, 𝑗) contains either the          Proof. Assume that 𝜉 𝑗 (𝜔) = 𝜉 𝑗 (𝜔 ′ ). Then 𝑆 = nf (𝜉 𝑗 (𝜔))
non-falsifying formula 𝐴 ∨ 𝐵 or the falsifying formula 𝐴𝐵             is a correction set with respect to (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}),
for every conditional (𝐵|𝐴) ∈ Δ𝑗+1 ∪. . .∪Δ𝑘 ; this way the           because 𝜔 is a model of all nf (𝑟) with 𝑟 ∈ Δ𝑗 ∖ 𝜉 𝑗 (𝜔). We
nf/f -condition 𝐻 ensures that for any two worlds 𝜔, 𝜔 ′ ∈            need to show that 𝑆 is a minimal correction set. Towards a
ΩΣ with 𝜔 |= 𝐻 and 𝜔 ′ |= 𝐻 we have 𝜉 𝑙 (𝜔) = 𝜉 𝑙 (𝜔 ′ ) for          contradiction assume that there is an 𝑅 ∈ nf (𝜉 𝑗 (𝜔)) such
all 𝑙 ∈ {𝑗 + 1, . . . , 𝑘}.                                           that 𝐶 = (𝐻 ∪ {𝐴𝐵}) ∪ nf (Δ𝑗 ) ∖ nf (𝜉 𝑗 (𝜔)) ∪ {𝑅} is
   To prove the correctness of SWinf, we prove the follow-            consistent. Let 𝜔 𝑐 be a model of 𝐶. The world 𝜔 𝑐 does not
ing three lemmas first. Lemma 1 describes the condition in            falsify any of the conditionals in Δ𝑗 ∖ 𝜉 𝑗 (𝜔) because it is a
Line 5 of SWinf.                                                      model of nf (Δ𝑗 ) ∖ nf (𝜉 𝑗 (𝜔)). There must be an 𝑟 ∈ 𝜉 𝑗 (𝜔)
                                                                      such that nf (𝑟) = 𝑅. The world 𝜔 𝑐 also does not falsify
Lemma 1. Let Δ be a consistent belief base with OP (Δ) =              𝑟 because it is a model of 𝑅. Therefore, 𝜉 𝑗 (𝜔 𝑐 ) ⫋ 𝜉 𝑗 (𝜔).
(Δ0 , . . . , Δ𝑘 ), let 𝑗 ∈ {0, . . . , 𝑘}, 𝐴, 𝐵 ∈ ℒΣ , and 𝐻 be      This contradicts that there is no 𝜔 * ∈ Mod Σ (𝐻 ∧𝐴𝐵) with
an nf/f -condition for (Δ, 𝑗). Let                                    𝜉 𝑗 (𝜔 * ) ⫋ 𝜉 𝑗 (𝜔); therefore 𝑆 is indeed a minimal correction
                                                                      set with respect to (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}).
            𝒱 = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}) and
                                                                          Analogously we can show that 𝑆 = nf (𝜉 𝑗 (𝜔 ′ )) =
            ℱ = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}).                             nf (𝜉 𝑗 (𝜔 ′ )) is a minimal correction set with respect to
                                                                      (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}). In summary, 𝑆 ∈ 𝒱 ∩ ℱ and
Then ¬(∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ ) holds iff there                    𝜔, 𝜔 ′ |= nf (Δ𝑗 ) ∖ 𝑆.
is a world 𝜔 ′ ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) such that for all 𝜔 ∈
Mod Σ (𝐻 ∧ 𝐴𝐵) it holds that 𝜉 𝑗 (𝜔) ̸⊆ 𝜉 𝑗 (𝜔 ′ ).                      Lemma 3 describes an effect of a set 𝑆 ∈ 𝒱 ∩ ℱ on sets
                                                                      of falsified conditionals.
Proof. Direction ⇒:             Assume ¬(∀𝑁 ∈ ℱ ∃𝑁 ∈
                                                  ′

𝒱 . 𝑁 ⊆ 𝑁 ′ ); this is equivalent to ∃𝑁 ′ ∈ ℱ ∀𝑁 ∈ 𝒱 . 𝑁 ̸⊆           Lemma 3. Let Δ be a consistent belief base with OP (Δ) =
𝑁 ′ . Let 𝑁 ′ ∈ ℱ be such a set with ∀𝑁 ∈ 𝒱 . 𝑁 ̸⊆ 𝑁 ′ .              (Δ0 , . . . , Δ𝑘 ), let 𝑗 ∈ {0, . . . , 𝑘}, 𝐴, 𝐵 ∈ ℒΣ , and let 𝐻
   Let 𝜔 ′ ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) be a world that satisfies                 be an nf/f -condition for (Δ, 𝑗). Let
nf (Δ𝑖 ) ∖ 𝑁 ′ ; such a world exists because nf (Δ𝑖 ) ∖ 𝑁 ′ is
consistent by the construction of MCS. Let 𝜔 be any world                         𝒱 = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}) and
in Mod Σ (𝐻 ∧ 𝐴𝐵). Let 𝑁 ∈ 𝒱 such that 𝑁 ⊆ nf (𝜉 𝑗 (𝜔));                         ℱ = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}).
such an 𝑁 exists because nf (𝜉 𝑗 (𝜔)) is a (not necessarily
minimal) correction set. By assumption, 𝑁 ̸⊆ 𝑁 ′ . There-             Then, for 𝑆 ∈ 𝒱 ∩ ℱ and every 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with
fore, also nf (𝜉 𝑗 (𝜔)) ̸⊆ 𝑁 ′ . Because MCS yields minimal           𝜔 |= nf (Δ𝑗 ) ∖ 𝑆, and every 𝜔 ′ ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with
correction sets, 𝜔 ′ falsifies all conditionals 𝑐 ∈ Δ𝑗 with           𝜔 ′ |= nf (Δ𝑗 ) ∖ 𝑆, it holds that 𝜉 𝑗 (𝜔) = 𝜉 𝑗 (𝜔 ′ ) = {𝑟 ∈
nf (𝑐) ∈ 𝑁 ′ , and 𝜔 ′ does not falsify the conditionals 𝑑 ∈ Δ𝑗       Δ𝑗 | nf (𝑟) ∈ 𝑆}.
with nf (𝑑) ∈  / 𝑁 ′ ; in summary nf (𝜉 𝑗 (𝜔)) = 𝑁 ′ . With
nf (𝜉 (𝜔)) ̸⊆ 𝑁 ′ we have 𝜉 𝑗 (𝜔) ̸⊆ 𝜉 𝑗 (𝜔 ′ ).
      𝑗                                                               Proof. Let 𝑅𝑆 = {𝑟 ∈ Δ𝑗 | nf (𝑟) ∈ 𝑆}. Because 𝜔 |=
   Direction ⇐:          We prove this direction by contrapo-         nf (Δ𝑗 ) ∖ 𝑆, we have that 𝜔 falsifies no conditionals in Δ𝑗 ∖
sition. Assume that ∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ . Let 𝜔 ′ be            𝑅𝑆 , i.e., 𝜉 𝑗 (𝜔) ⊆ 𝑅𝑆 . Because 𝑆 is a minimal correction
any world in Mod Σ (𝐻 ∧ 𝐴𝐵); we need to show that there               set in 𝒱, there is no 𝑟 ∈ 𝑅𝑆 that does is not falsified by 𝜔:
is an 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) such that 𝜉 𝑗 (𝜔) ⊆ 𝜉 𝑗 (𝜔 ′ ).              if there were such an 𝑟 then 𝑆 ∖ {nf (𝑟)} would be an even
   Let 𝑁 ′ ∈ ℱ such that 𝑁 ′ ⊆ nf (𝜉 𝑗 (𝜔 ′ )); such an 𝑁 ′           smaller correction set. Therefore, 𝜉 𝑗 (𝜔) = 𝑅𝑆 .
exists because nf (𝜉 𝑗 (𝜔 ′ )) is a (not necessarily minimal)             Analogously we can show that 𝜉 𝑗 (𝜔 ′ ) = 𝑅𝑆 .
correction set. By assumption there is an 𝑁 ∈ 𝒱 such that
                                                                         Now we can use Lemma 1, Lemma 2, and Lemma 3 to
𝑁 ⊆ 𝑁 ′ . Let 𝜔 ∈ Mod Σ (nf (Δ𝑗 ) ∖ 𝑁 ); such a world exists
                                                                      show Proposition 2 on the output of the recursive algorithm
because nf (Δ𝑗 ) ∖ 𝑁 is consistent by the definition of MCS.
                                                                      recWinf .
Because MCS yields minimal correction sets, 𝜔 falsifies all
conditionals 𝑐 ∈ 𝑁 Δ𝑗 with nf (𝑐) ∈ 𝑁 . Furthermore, 𝜔 ′              Proposition 2. Let Δ be consistent with OP (Δ) =
falsifies all conditionals 𝑑 ∈ Δ𝑗 with nf (𝑑) ∈ 𝑁 ′ . There-          (Δ0 , . . . , Δ𝑘 ), let 𝑗 ∈ {0, . . . , 𝑘}, 𝐴, 𝐵 ∈ ℒΣ , and let
fore, 𝑁 ⊆ 𝑁 ′ implies 𝜉 𝑗 (𝜔) ⊆ 𝜉 𝑗 (𝜔 ′ ).
𝐻 be an nf/f -condition for (Δ, 𝑗). Then recWinf (𝑗, 𝐻)           Because 𝑆 is a minimal correction set in both 𝒱 and ℱ, we
returns “Yes” iff                                                 have 𝜔, 𝜔 ′ |= 𝑆. Because the algorithm passes Lines 7–12
                                                                  without returning “No”, for 𝐻new ← (nf (Δ𝑗 ) ∖ 𝑆) ∪ 𝑆 the
  for every 𝜔 ′ ∈ Mod Σ (𝐻 ∧ 𝐴𝐵)                                  function call recWinf (𝑗 − 1, 𝐻 ∪ 𝐻new ) returns “Yes”. By
                                                           (5)
      there is an 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜔 <wΔ 𝜔 ′ .             construction, 𝐻 ∪ 𝐻new is an nf/f -condition for (Δ, 𝑗 − 1).
                                                                  Furthermore, 𝜔 |= 𝐻 ∧𝐴𝐵. Using the induction hypothesis,
Proof. We prove this by induction over 𝑗. Let                     there is an 𝜔 𝑎 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜔 𝑎 <wΔ 𝜔 ′ .
                                                                     In summary, (5) holds.
           𝒱 = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵}) and                          Direction ⇐:         Assume that (5) holds. We need to
           ℱ = MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵})                           show that recWinf (𝑗, 𝐻) returns “Yes”. With Lemma 1 and
                                                                  because 𝐻 is an nf/f -condition for (Δ, 𝑗), we have that
as assigned in Lines 3 and 4 (Algorithm 1).                       ¬(∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ ) does not hold; therefore
  Base Case (𝑗 = 0):      By observing Lines 5 – 9 and 13         the algorithm passes Lines 5 and 6 without returning “No”.
we see that recWinf (𝑗, 𝐻) returns “Yes” iff                         It is left to show that the algorithm passes Lines 7–12
                                                                  without returning “No”. Let 𝑆 be any set in 𝒱 ∩ ℱ. By
 not ¬(∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ ) and 𝒱 ∩ ℱ = ∅. (6)             construction, 𝐻new is an nf/f -condition for (Δ, 𝑗 − 1). Let
                                                                  𝜔 ′ be any world in Mod Σ (𝐻 ∧ 𝐻new ∧ 𝐴𝐵). Because 𝜔 ′ |=
We show that (6) is equivalent to (5) by showing both direc-      𝐻new we have 𝜔 |= nf (Δ𝑗 ) ∖ 𝑆. Because of (5), there
tions of this equivalence.                                        is a world 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜔 <wΔ 𝜔 ′ . Using
    Direction ⇒:            Assume (6) holds. Let 𝜔 ′ be any      ∀𝑁 ′ ∈ ℱ ∃𝑁 ∈ 𝒱 . 𝑁 ⊆ 𝑁 ′ again, we know that 𝜉(𝜔) ⊆
world in Mod Σ (𝐻 ∧ 𝐴𝐵). Because 𝐻 is an nf/f -condition          𝜉(𝜔 ′ ) = {𝑟 ∈ Δ𝑗 | nf (𝑟) ∈ 𝑆} (the last equation holding
for (Δ, 0), every model of 𝐻 falsifies the same conditionals      due to Lemma 3); therefore 𝜔 |= nf (Δ𝑗 )∖𝑆. Using Lemma 3
in Δ1 , . . . , Δ𝑘 . Therefore, we need to show that there is a   again, we have 𝜉 𝑗 (𝜔) = {𝑟 ∈ Δ𝑗 | nf (𝑟) ∈ 𝑆} and
world 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜉 0 (𝜔) ⫋ 𝜉 0 (𝜔 ′ ).               therefore 𝜔 |= 𝐻new . Hence, for every 𝜔 ′ ∈ Mod Σ (𝐻 ∧
    W.l.o.g. assume that there is no 𝜔 ′* with 𝜉 0 (𝜔 ′* ) ⫋      𝐻new ∧ 𝐴𝐵) there is an 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐻new ∧ 𝐴𝐵) with
𝜉 0 (𝜔 ′ ). With Lemma 1 and the first part of (6) we have        𝜔 <wΔ 𝜔 ′ . Employing the induction hypothesis, we have
that there is an 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜉 0 (𝜔) ⊆ 𝜉 0 (𝜔 ′ ).    that recWinf (𝑗 − 1, 𝐻 ∪ 𝐻new ) returns “Yes”.
W.l.o.g. assume that there is no 𝜔 * with 𝜉 0 (𝜔 * ) ⫋ 𝜉 0 (𝜔).      Thus, algorithm passes Lines 7–12 without returning
Towards a contradiction, assume that 𝜉 0 (𝜔) = 𝜉 0 (𝜔 ′ ).        “No”, and then returns “Yes” in Line 13.
With Lemma 2 we have that there is an 𝑆 ∈ 𝒱 ∩ ℱ which
contradicts (6). Therefore, 𝜉 0 (𝜔) ⫋ 𝜉 0 (𝜔 ′ ).                  Now it is straightforward to show the correctness of
    Direction ⇐:          Assume that (5) holds. Because 𝐻 is     SWinfwith Proposition 2.
an nf/f -condition for (Δ, 0), every model of 𝐻 falsifies the
same conditionals in Δ1 , . . . , Δ𝑘 . Therefore, with Lemma 1    Theorem 1. Given a consistent belief base Δ and 𝐴, 𝐵 ∈
it follows that the part left of the and in (6) holds.            ℒΣ , the call SWinf(Δ, 𝐴, 𝐵) always terminates, and it re-
    It is left to show 𝒱 ∩ ℱ = ∅. Towards a contradiction         turns “Yes” iff 𝐴 |∼ wΔ 𝐵.
assume that 𝒱 ∩ ℱ ̸= ∅, i.e., there is an 𝑆 ∈ 𝒱 ∩ ℱ . Because
                                                                  Proof. SWinf(Δ, 𝐴, 𝐵) terminates because 𝒱, ℱ and thus
𝑆 is a correction set of ℱ, there is an 𝜔 ′ ∈ Mod Σ (𝐻 ∧ 𝐴𝐵)
                                                                  also 𝒱 ∩ ℱ are always finite sets, and for every recursive
with 𝜔 ′ |= nf (Δ0 ) ∖ 𝑆. By (5) there is an 𝜔 ∈ Mod Σ (𝐻 ∧
                                                                  call the index 𝑗 is decreased by one. SWinf(Δ, 𝐴, 𝐵) re-
𝐴𝐵) with 𝜔 <wΔ 𝜔 ′ . Because 𝜔 <wΔ 𝜔 ′ and 𝐻 is an nf/f -
                                                                  turns “Yes” iff recWinf (𝑘, ∅) returns “Yes”. Because ∅ is
condition for (Δ, 0) we have 𝜉 0 (𝜔) ⊆ 𝜉 0 (𝜔 ′ ) and therefore
                                                                  an nf/f -condition for (Δ, 𝑘), according to Proposition 2,
𝜔 |= nf (Δ0 ) ∖ 𝑆. W.l.o.g. assume that there is no 𝜔 * ∈
                                                                  this happens iff for every 𝜔 ∈ Mod Σ (∅ ∧ 𝐴𝐵) there is an
Mod Σ (𝐻 ∧ 𝐴𝐵) with 𝜔 * |= nf (Δ0 ) ∖ 𝑆 and 𝜉 0 (𝜔 * ) ⫋
                                                                  𝜔 ′ ∈ Mod Σ (∅ ∧ 𝐴𝐵) with 𝜔 <wΔ 𝜔 ′ , which is equivalent
𝜉 0 (𝜔). By Lemma 3 we have 𝜉 0 (𝜔) = 𝜉 0 (𝜔 ′ ). This implies
                                                                  to 𝐴 |∼ wΔ 𝐵.
𝜉(𝜔) = 𝜉(𝜔 ′ ) and contradicts 𝜔 <wΔ 𝜔 ′ . Therefore, 𝒱 ∩
ℱ = ∅ and (6) holds.
    Induction Step:            Let 𝑗 > 0 and assume the propo-    6. Algorithm SZinf for System Z
sition holds for 𝑗 ′ = 𝑗 − 1. We show that recWinf (𝑗, 𝐻)
returns “Yes” iff (5) holds by showing both directions of this    Pearl’s system Z [20] is a well-known inductive inference
equivalence.                                                      operator that was shown to coincide with rational closure
    Direction ⇒:           Assume that recWinf (𝑗, 𝐻) returns     [26, 27]
“Yes”; therefore the algorithm reaches Line 13 at some point.     Definition 6 (System Z [20]). Let Δ be consistent with
It is left to show that (5) holds. Let 𝜔 ′ be any world in        OP (Δ) = (Δ0 , . . . , Δ𝑘 ). The ranking function 𝜅𝑧Δ is de-
Mod Σ (𝐻 ∧ 𝐴𝐵). W.l.o.g. assume that there is no 𝜔 ′* with        fined as follows: If 𝜔 ∈ ΩΣ does not falsify any conditional
𝜉 𝑗 (𝜔 ′* ) ⫋ 𝜉 𝑗 (𝜔 ′ ).                                         in Δ, then let 𝜅𝑧Δ (𝜔) := 0. Otherwise, let Δ𝑗 be the last part
    The algorithm passes Lines 5 and 6 without returning          in OP (Δ) that contains a conditional falsified by 𝜔, and let
“No”. Therefore, there is a world 𝜔 ∈ Mod Σ (𝐻 ∧ 𝐴𝐵) such         𝜅𝑧Δ (𝜔) := 𝑗 + 1. System Z maps Δ to the inference relation
that 𝜉 𝑗 (𝜔) ⊆ 𝜉 𝑗 (𝜔 ′ ). W.l.o.g. assume that there is no 𝜔 *   |∼ 𝑧Δ induced by 𝜅𝑧Δ according to (1).
with 𝜉 𝑗 (𝜔 * ) ⊊ 𝜉 𝑗 (𝜔). We can distinguish two cases.
    Case 1: 𝜉 𝑗 (𝜔) ⫋ 𝜉 𝑗 (𝜔 ′ ).                                   For any consistent Δ, the function 𝜅𝑧Δ is the unique least
Because 𝐻 is an nf/f -condition for (Δ, 𝑗), all models of         ranking model of Δ [20].
𝐻, including 𝜔 and 𝜔 ′ , falsify the same conditionals in
Δ𝑗+1 , . . . , Δ𝑘 . Therefore, 𝜔 <wΔ 𝜔 ′ .                        Example 4. For the belief base Δbird from Exam-
    Case 2: 𝜉 𝑗 (𝜔) = 𝜉 𝑗 (𝜔 ′ ).                                 ple 1 we have OP (Δbird ) = (Δbird 0 , Δbird 1 ) with
By Lemma 2 there is an 𝑆 ∈ 𝒱 ∩ℱ with 𝜔, 𝜔 ′ |= nf (Δ𝑗 )∖𝑆.        Δbird 0 = {𝑟1 , 𝑟4 } and Δbird 1 = {𝑟2 , 𝑟3 }. The
                    𝜔          𝜅𝑧Δ
                                       bird
                                              (𝜔)                   falsifies no conditionals in Δ𝑗 for each 𝐵  ˙ ∈ {𝐵, 𝐵}. This
                  𝑏𝑝𝑓 𝑤                 2                           does not even require solving a Partial MaxSAT problem;
                  𝑏𝑝𝑓 𝑤                 2                           instead we just have to check two sets of formulas for their
                  𝑏𝑝𝑓 𝑤                 1                           satisfiability.
                  𝑏𝑝𝑓 𝑤                 1                              Second, because there are no different minimal sets of
                  𝑏𝑝𝑓 𝑤                 0                           falsified conditionals to choose from, we do not need an ar-
                  𝑏𝑝𝑓 𝑤                 1                           gument 𝐻 of the recursive function to keep track of the
                  𝑏𝑝𝑓 𝑤                 1                           (non-)falsified conditionals in the previously considered
                  𝑏𝑝𝑓 𝑤                 1                           parts of OP (Δ). ⋃︀ Instead, we straightforwardly    check the
                  𝑏𝑝𝑓 𝑤                 2                           satisfiability of 𝑘𝑖=𝑗 nf (Δ𝑖 )∪{𝐴𝐵  ˙ }.
                  𝑏𝑝𝑓 𝑤                 2                              For determining whether 𝐴 entails 𝐵, SZinf(Δ, 𝐴, 𝐵)
                  𝑏𝑝𝑓 𝑤                 2                           considers the parts in OP (Δ) beginning with the latest
                  𝑏𝑝𝑓 𝑤                 2                           Δ𝑘 . The main part of SZinf is a recursive function
                  𝑏𝑝𝑓 𝑤                 0                           recZinf (𝑗) whose argument is the index of the part
                  𝑏𝑝𝑓 𝑤                 0                           of OP (Δ) that is considered next.
                  𝑏𝑝𝑓 𝑤                 0                                                                  ⋃︀𝑘 For each   Δ𝑗 , the
                                                                    algorithm determines 𝑉 = SAT( 𝑖=𝑗 nf (Δ )∪{𝐴𝐵})
                                                                                               𝑗                       𝑖
                  𝑏𝑝𝑓 𝑤                 0
                                                                    and 𝐹 𝑗 = SAT( 𝑘𝑖=𝑗 nf (Δ𝑖 )∪{𝐴𝐵}). Note that for
                                                                                         ⋃︀

                                                                    𝑗 < 𝑘, recZinf (𝑗) is only called if 𝐹 𝑗+1 = 𝑆𝐴𝑇 (cf. Line
Table 1                                                             7), implying that 𝜅𝑧Δ (𝐴𝐵) < 𝑗 + 2. If 𝑉 = UNSAT, then
System Z ranking function 𝜅𝑧Δ           for Δbird in Example 4.
                                bird                                𝜅𝑧Δ (𝐴𝐵) ⩾ 𝑗 + 1 and thus 𝜅𝑧Δ (𝐴𝐵) ̸< 𝜅𝑧Δ (𝐴𝐵), implying
                                                                    𝐴 ̸|∼ 𝑧Δ 𝐵. If 𝑉 = SAT and 𝐹 = UNSAT, then we can
Algorithm 2 SZinf(Δ, 𝐴, 𝐵)                                          conclude that 𝜅𝑧Δ (𝐴𝐵) < 𝑗 + 1 and 𝜅𝑧Δ (𝐴𝐵) ⩾ 𝑗 + 1
                                                                    and thus 𝜅𝑧Δ (𝐴𝐵) < 𝜅𝑧Δ (𝐴𝐵), implying 𝐴 |∼ 𝑧Δ 𝐵. If
Input: consistent belief base Δ and formulas 𝐴, 𝐵
                                                                    𝑉 = SAT and 𝐹 = SAT, we continue by recursively calling
Output: Yes if 𝐴 |∼ zΔ 𝐵, and No otherwise
                        0       𝑘
                                                                    recZinf (𝑗 − 1) to check the parts of OP (Δ) with a lower
  1: let OP (Δ) = (Δ , . . . , Δ )                                  index. Line 14 contains the initial call to recZinf and
  2: function recZinf (𝑗)                                           the handling of the border case that the antecedent is an
                  ⋃︀𝑘         𝑖
  3: 𝑉 ← SAT( 𝑖=𝑗 nf (Δ )∪{𝐴𝐵})                                     inconsistent formula.
  4: if 𝑉 = UNSAT then                                                 Note that the function recZinf in SZinf can be easily
  5:     return No                                                  rewritten to use a loop instead of recursion, but we decided
                                                                    to present it with recursive calls to point out the similarity
                  ⋃︀𝑘         𝑖
  6: 𝐹 ← SAT( 𝑖=𝑗 nf (Δ )∪{𝐴𝐵})
  7: if 𝐹 = SAT then                                                to SWinf.
  8:     if 𝑗 = 0 then
  9:       return No                                                Example 5. Executing SZinf(Δbird , 𝑝, 𝑤) yields two succe-
                                                                    sive calls of recZinf involving as values and conditions:
 10:     if recZinf (𝑗 − 1) = No then
 11:       return No                                                        recZinf (𝑗 = 1),
 12: return Yes                                                             𝑉 ← SAT ,
 13: end function                                                           𝑉 ̸= UNSAT ,
 14: return if 𝐴 ≡ ⊥ then Yes else recZinf (𝑘)                              𝐹 ← SAT ,
                                                                            𝐹 = SAT ,
                                                                            𝑗 ̸= 0,
                                                                            return No iff recZinf (0) = No
Z-ranking function induced by Δbird is displayed in
Table 1. We have 𝜅𝑧Δbird (𝑝𝑏) = 0 and 𝜅𝑧Δbird (𝑝𝑏) = 2,                    recZinf (𝑗 = 0),
and thus 𝑏 |∼ 𝑧Δbird 𝑝. Analogously, we can check that                     𝑉 ← UNSAT ,
𝜅𝑧Δbird (𝑤𝑝) = 𝜅𝑧Δbird (𝑤𝑝) = 1, yielding 𝑝 ̸|∼ 𝑧Δbird 𝑤.                  𝑉 = UNSAT ⇒ return No
   Note that this also illustrate that system Z, in contrast to,
e.g., system W, suffers from the drowning problem [12] be-            Thus, SZinf(Δbird , 𝑝, 𝑤) returns No, and 𝑝 |̸∼ zΔbird 𝑤.
cause the birds property of having wings is drowned for pen-
guins because penguins are exceptional birds with respect to        7. Correctness Proof for SZinf
the property flying.
                                                                    For proving the correctness of SZinf, we first show the
   Implementations of system Z have to cope with the expo-
                                                                    following lemma connecting the satisfiablility of
nentially growing number of worlds for larger signatures.
Based on the approach of SWinf we design a similar algo-                                      𝑘
rithm SZinf (Algorithm 2) for system Z.                                                𝑗
                                                                                             ⋃︁
                                                                                      𝑆𝐴 =         nf (Δ𝑖 )∪{𝐴}
   One of the main differences between system W and sys-                                     𝑖=𝑗
tem Z is that, while <wΔ compares the sets of conditionals
falsified by each world, 𝜅𝑧Δ only takes into account the latest     to the rank of a formula 𝐴.
𝑗 for which any conditional in Δ𝑗 is falsified by each world.
                                                                    Lemma 4. Let Δ be a consistent belief base with OP (Δ) =
This simplifies the algorithm SZinf compared to SWinf in
                                                                    (Δ0 , . . . , Δ𝑘 ), let 𝑗 ∈ {0, . . . , 𝑘}, and let 𝐴 ∈ ℒΣ .
two ways.
   First, instead of finding a minimal set of falsified con-            1. If 𝑆𝐴
                                                                               𝑗
                                                                                 is consistent, then 𝜅𝑧Δ (𝑆) < 𝑗 + 1.
ditionals in Δ𝑗 with MCS (nf (Δ𝑗 ), 𝐻 ∪ {𝐴𝐵      ˙ }), it is suf-       2. If 𝑆𝐴 is not consistent, then 𝜅𝑧Δ (𝑆) ⩾ 𝑗 + 1.
                                                                               𝑗

ficient to check if there is a world 𝜔 with 𝜔 |= 𝐴𝐵      ˙ that
Proof. Ad (1.): Assume that 𝑆𝐴      𝑗
                                      is consistent. Then there    8. Implementation and Evaluation
is a world 𝜔 with 𝜔 |= 𝑖=𝑗 nf (Δ𝑖 ) and 𝜔 |= 𝐴. Because
                         ⋃︀𝑘
                                                                      Results
𝜔 |= 𝑘𝑖=𝑗 nf (Δ𝑖 ), the world 𝜔 does not falsify any con-
       ⋃︀

ditional in 𝑘𝑖=𝑗 Δ𝑖 , and thus 𝜅𝑧Δ (𝜔) < 𝑗 + 1. Because
              ⋃︀                                                   We implemented SWinf and SZinf in Python and using the
𝜔 |= 𝐴 and 𝜅𝑧Δ (𝐴) = min{𝜅𝑧Δ (𝜔) | 𝜔 |= 𝐴}, this implies           SMT solver Z3 [28] accessed through the pySMT API [29].
𝜅𝑧Δ (𝐴) < 𝑗 + 1.                                                   In the implementation of SWinf, we used the optimizing
   Ad (2.): Assume that 𝑆𝐴     𝑗
                                 is not consistent. Then every     features of the Z3 SMT Solver to find Pareto fronts [30]
world   𝜔   with 𝜔 |= 𝐴  falsifies at least one conditional in     (which, in our case, is equivalent to finding the sets of all
                                                                   MSS and thus allows deriving the set of all MCS).
   𝑖=𝑗 Δ . Therefore, 𝜅Δ (𝐴) ⩾ 𝑗 + 1.
⋃︀𝑘       𝑖             𝑧
                                                                      For checking the correctness of our implementations, we
  Now we can prove the correctness of recZinf .                    verified that the output of the implementations of SWinf
                                                                   and SZinf match the output of earlier implementations of
Proposition 3. Let Δ be a consistent belief base with
                                                                   system W [16] and of system Z [31]. For all queries with
OP (Δ) = (Δ0 , . . . , Δ𝑘 ), let 𝑗 ∈ {0, . . . , 𝑘}, and let
                       𝑗+1          𝑗+1                            respect to all belief bases small enough to be processed by
𝐴, 𝐵 ∈ ℒΣ . If 𝑆𝐴𝐵           and 𝑆𝐴𝐵    are consistent, then
                                                                   these older implementations without running into a timeout,
recZinf (𝑗) returns “Yes” iff 𝜅𝑧Δ (𝐴𝐵) < 𝜅𝑧Δ (𝐴𝐵).                 the different implementations of system W and system Z,
Proof. We prove this by induction over 𝑗.                          respectively, yielded exactly the same result.
                                                                      For evaluating the implementations of SWinf and SZinf,
   Base Case (𝑗 = 0):          By assumption 𝑆𝐴𝐵 𝑗+1
                                                     and 𝑆𝐴𝐵𝑗+1
                                                                   belief bases and queries were constructed by a random-
are consistent, and thus, by Lemma 4 we have 𝜅𝑧Δ (𝐴𝐵) <
                                                                   ized scheme taking a signature Σ as input; a detailed de-
𝑗 + 2 = 2 and 𝜅𝑧Δ (𝐴𝐵) < 𝑗 + 2 = 2, implying that
                                                                   scription of this scheme and algorithms realizing it are
𝜅𝑧Δ (𝐴𝐵), 𝜅𝑧Δ (𝐴𝐵) ∈ {0, 1}.
                                                                   given in [32]. Only consistent belief bases build during
   If 𝑆𝐴𝐵
        𝑗
            is consistent and 𝑆𝐴𝐵 𝑗
                                     is inconsistent, then by
                                                                   this process were used for benchmarking because system W
Lemma 4 we have 𝜅Δ (𝐴𝐵) = 0 and 𝜅𝑧Δ (𝐴𝐵) = 1 and thus
                       𝑧
                                                                   as given in Definition 3 and system Z as given in Defini-
𝜅𝑧Δ (𝐴𝐵) < 𝜅𝑧Δ (𝐴𝐵). In this case the checks in Lines 4 and        tion 6 are defined only for consistent belief bases; reasoning
7 fail and recZinf returns “Yes”.                                  with system W with respect to belief bases that are only
   In all other cases we have 𝜅𝑧Δ (𝐴𝐵) ̸< 𝜅𝑧Δ (𝐴𝐵) and             weakly consistent [33, 34] has been introduced only very re-
recZinf returns “No” because one of the checks in Lines 4          cently [33, 24]. In the evaluation, belief bases with signature
and 7 succeeds.                                                    sizes |Σ| ranging from 6 to 120 and number of conditionals
   In both cases the proposition holds.                            |Δ| ranging from 6 to 200 were considered. For different
   Induction Step:          Let 𝑗 > 0 and assume the proposi-      (|Σ|, |Δ|)-combinations, in summary, 2 800 belief bases and
tion holds for 𝑗 ′ = 𝑗 −1. By assumption 𝑆𝐴𝐵  𝑗+1
                                                  and 𝑆𝐴𝐵
                                                        𝑗+1
                                                             are   28 000 queries were created; the belief bases and queries
consistent, and thus, by Lemma 4 we have 𝜅𝑧Δ (𝐴𝐵) < 𝑗 +2           obtained thereby are available at the CLKR repository [35]
and 𝜅𝑧Δ (𝐴𝐵) < 𝑗 + 2. We can distinguish several cases             at https://www.fernuni-hagen.de/wbs/clkr/ as problem set
   Case 1: 𝑆𝐴𝐵𝑗
                  is inconsistent                                  CLKR-PS004.
By Lemma 4 we have 𝜅𝑧Δ (𝐴𝐵) ⩾ 𝑗 + 1 implying that                     We benchmarked our (Partial Max-)SAT based Python
𝜅𝑧Δ (𝐴𝐵) ̸< 𝜅𝑧Δ (𝐴𝐵). Also, the check in Line 4 succeeds           implementations of SWinf and SZinf against existing Java-
and recZinf returns “No”. The proposition holds.                   based approaches for inference according to system-W (WJ)
   Case 2: 𝑆𝐴𝐵𝑗
                  is consistent and 𝑆𝐴𝐵
                                      𝑗
                                          is inconsistent          and system-Z (ZJ) that both consider all possible worlds
By Lemma 4 we have 𝜅𝑧Δ (𝐴𝐵) < 𝑗+1 and 𝜅𝑧Δ (𝐴𝐵) ⩾ 𝑗+1               explicitly [16, 31]. No other previous system implementa-
implying that 𝜅𝑧Δ (𝐴𝐵) < 𝜅𝑧Δ (𝐴𝐵). The checks in Line 4            tions of system W exist, and to the best of our knowledge all
and 7 fail and recZinf returns “Yes”. The proposition holds.       other existing implementations of system Z, e.g., [36, 37, 38],
   Case 3: 𝑆𝐴𝐵𝑗
                  is consistent and 𝑆𝐴𝐵
                                      𝑗
                                          is consistent            cannot handle belief bases over signature size of 50 or more.
In this case the function recZinf is called recursively for 𝑗 −       Performance was assessed on a machine with an Intel i7-
1. The preconditions for applying this proposition for 𝑗 ′ =       3770 CPU and 32GB RAM under Arch Linux (Linux kernel
𝑗−1 are satisfied, and therefore, by the induction hypothesis,     6) and Python 3.11 (single threaded). Each implementation
recZinf (𝑗) returns “Yes” iff 𝜅𝑧Δ (𝐴𝐵) < 𝜅𝑧Δ (𝐴𝐵). The             was tested on the full set of randomly generated belief bases
proposition holds.                                                 and queries described above. The run times presented in
                                                                   Table 2 are averaged over 1,000 queries across 100 belief
  Using Proposition 3, we can now show the correctness of          bases for every combination of (|Σ|, |Δ|). Time is presented
SZinf.                                                             in ms, timeout was set to 5 minutes.
Theorem 2. Given a consistent belief base Δ and 𝐴, 𝐵 ∈                The evaluation results in Table 2 show that only for the
ℒΣ , the call SZinf(Δ, 𝐴, 𝐵) always terminates, and it re-         very smallest (|Σ|, |Δ|)-combinations with |Σ| = 6 and
turns “Yes” iff 𝐴 |∼ 𝑧Δ 𝐵.                                         |Δ| = 6 the Java-based implementations WJ and ZJ of
                                                                   system W and system Z, respectively, are faster than our im-
Proof. For 𝐴 ≡ ⊥, SWinf(Δ, 𝐴, 𝐵) returns “Yes” (cf. Line           plementations of SWinf and SZinf. Furthermore, for every
14) and 𝐴 |∼ 𝑧Δ 𝐵, thus the theorem holds in this case. For        (|Σ|, |Δ|) combination with |Σ| ⩾ 18 both WJ and ZJ ran
the remainder of the proof assume that 𝐴 ̸≡ ⊥.                     into a timeout in our evaluation scenario, while SWinf and
   SWinf(Δ, 𝐴, 𝐵) terminates because for every recursive           SZinf successfully cope with all (|Σ|, |Δ|) combinations
call of recZinf the index 𝑗 is decreased by one, and the           up to |Σ| = 120 and |Δ| = 200. It is interesting to note
algorithm terminates at latest for 𝑗 = 0. For 𝑗 = 𝑘, the sets      that SZinfconsistently performs faster than SWinf in our
  𝑗+1
𝑆𝐴𝐵   and 𝑆𝐴𝐵
            𝑗+1
                are empty and are thus trivially consistent.       evaluation only by a factor of up to 2 across all (|Σ|, |Δ|)
By Proposition 3, the call SWinf(Δ, 𝐴, 𝐵) returns “Yes” iff        combinations. In summary, this comparative evaluation
𝜅𝑧Δ (𝐴𝐵) < 𝜅𝑧Δ (𝐴𝐵), which is equivalent to 𝐴 |∼ 𝑧Δ 𝐵.             showcases SWinf’s and SZinf’s superior scalability and ef-
  |Σ|    6   8   10    12    14    16 18 20 30 40 50 60 60 60 60 80 80 80 80 100 100 100 100 120 120 120 120 120
  |Δ|    6   8   10    12    14    16 18 20 30 40 50 60 80 100 120 60 80 120 160 60 100 160 200 60 80 120 160 200

  WJ    19 204 4967 248323   to.   to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to.
SWinf 32 37      44    49    53    55 61 64 87 106 157 156 181 218 259 130 212 254 343 135 294 320 407 123 179 785 334 403

  ZJ    11 52 302 1705 10337 80014 to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to. to.
 SZinf 32 35     38    40    42    44 45 46 55 62 74 78 106 129 143 78 95 150 200 75 104 175 219 75 92 128 177 224

    Table 2
    Evaluation of implementations of inference with system W and system Z, time in milliseconds, timeout (to.) is at 5 min.



ficiency, particularly in handling queries on larger belief           [5] D. Dubois, H. Prade, Conditional objects as nonmono-
bases within reasonable time frames.                                      tonic consequence relationships, Special Issue on Con-
                                                                          ditional Event Algebra, IEEE Transactions on Systems,
                                                                          Man and Cybernetics 24 (1994) 1724–1740.
9. Conclusions and Future Work                                        [6] S. Benferhat, D. Dubois, H. Prade, Nonmonotonic
                                                                          reasoning, conditional objects and possibility theory,
In this paper, we presented SAT and Partial MaxSAT based
                                                                          Artificial Intelligence 92 (1997) 259–276.
approaches for implementing nonmonotonic reasoning with
                                                                      [7] G. Kern-Isberner, Conditionals in nonmonotonic rea-
system Z and system W. We presented the corresponding
                                                                          soning and belief revision, volume 2087 of LNAI,
algorithms SZinf and SWinf and gave formal correctness
                                                                          Springer, 2001.
proofs for them. The Python-based implementations of
                                                                      [8] C. Beierle, C. Eichhorn, G. Kern-Isberner, S. Kutsch,
SZinf and SWinf use the power of current SAT and Partial
                                                                          Properties and interrelationships of skeptical, weakly
MaxSAT solvers and scale up reasoning both with system Z
                                                                          skeptical, and credulous inference induced by classes
and system W to a new dimension, easily coping with belief
                                                                          of minimal models, Artificial Intelligence 297 (2021)
bases over 120 variables and containing up to 200 condition-
                                                                          103489. doi:10.1016/j.artint.2021.103489.
als. This advancement also puts larger practical applications
                                                                      [9] M. Goldszmidt, J. Pearl, Qualitative probabilities for
into reach for the first time.
                                                                          default reasoning, belief revision, and causal modeling,
   Our current and future work includes extending the pre-
                                                                          Artificial Intelligence 84 (1996) 57–112.
sented work in multiple ways. For instance, while the eval-
                                                                     [10] C. Komo, C. Beierle, Nonmonotonic reasoning from
uation presented in Section 8 focuses on runtime, we will
                                                                          conditional knowledge bases with system W, Ann.
further evaluate SZinf and SWinf by taking also the mem-
                                                                          Math. Artif. Intell. 90 (2022) 107–144. doi:10.1007/
ory consumption into account. We will also analyse the
                                                                          s10472-021-09777-9.
complexity of the algorithms. While previous practical ap-
                                                                     [11] D. Lehmann, M. Magidor, What does a conditional
plications were limited by small belief base sizes, we will
                                                                          knowledge base entail?, Artif. Intell. 55 (1992) 1–60.
address larger and more realistic scenarios in the medical
                                                                     [12] S. Benferhat, C. Cayrol, D. Dubois, J. Lang, H. Prade,
and bio-medical domain as they have already been modelled
                                                                          Inconsistency Management and Prioritized Syntax-
with conditional logic [39], using the new opportunities
                                                                          Based Entailment, in: Proc. IJCAI’93, volume 1, Mor-
opened up by the enriched power of our new implementa-
                                                                          gan Kaufmann Publishers, San Francisco, CA, USA,
tions of nonmonotonic inference.
                                                                          1993, pp. 640–647.
                                                                     [13] G. Kern-Isberner, C. Beierle, G. Brewka, Syntax split-
Acknowledgments                                                           ting = relevance + independence: New postulates
This work was supported by the Deutsche Forschungs-                       for nonmonotonic reasoning from conditional belief
gemeinschaft (DFG, German Research Foundation) -                          bases, in: D. Calvanese, E. Erdem, M. Thielscher (Eds.),
512363537, grant BE 1700/12-1 awarded to Christoph                        Principles of Knowledge Representation and Reason-
Beierle.                                                                  ing: Proceedings of the 17th International Confer-
                                                                          ence, KR 2020, IJCAI Organization, 2020, pp. 560–571.
                                                                          doi:10.24963/kr.2020/56.
References                                                           [14] J. Haldimann, C. Beierle, Inference with system W
                                                                          satisfies syntax splitting, in: G. Kern-Isberner, G. Lake-
 [1] E. Adams, The Logic of Conditionals, D. Reidel, Dor-                 meyer, T. Meyer (Eds.), Proceedings of the 19th In-
     drecht, 1975.                                                        ternational Conference on Principles of Knowledge
 [2] D. Nute, Topics in Conditional Logic, D. Reidel Pub-                 Representation and Reasoning, KR 2022, Haifa, Is-
     lishing Company, Dordrecht, Holland, 1980.                           rael. July 31 - August 5, 2022, 2022, pp. 405–409.
 [3] W. Spohn, Ordinal conditional functions: a dynamic                   doi:10.24963/kr.2022/41.
     theory of epistemic states, in: W. Harper, B. Skyrms            [15] J. Heyninck, G. Kern-Isberner, T. Meyer, J. P.
     (Eds.), Causation in Decision, Belief Change, and Statis-            Haldimann, C. Beierle, Conditional syntax splitting for
     tics, II, Kluwer Academic Publishers, 1988, pp. 105–                 non-monotonic inference operators, in: B. Williams,
     134.                                                                 Y. Chen, J. Neville (Eds.), Proceedings of the 37th AAAI
 [4] S. Kraus, D. Lehmann, M. Magidor, Nonmonotonic                       Conference on Artificial Intelligence, volume 37, 2023,
     reasoning, preferential models and cumulative logics,                pp. 6416–6424. doi:10.1609/aaai.v37i5.25789.
     Artif. Intell. 44 (1990) 167–207.                               [16] C. Beierle, J. Haldimann, D. Kollar, K. Sauerwald,
     L. Schwarzer, An implementation of nonmonotonic                  (Eds.), Proceedings of the 1st International Confer-
     reasoning with system W, in: R. Bergmann, L. Mal-                ence on Principles of Knowledge Representation and
     burg, S. C. Rodermund, I. J. Timm (Eds.), KI 2022: Ad-           Reasoning (KR’89). Toronto, Canada, May 15-18 1989,
     vances in Artificial Intelligence - 45th German Con-             Morgan Kaufmann, 1989, pp. 212–222.
     ference on AI, Trier, Germany, September 19-23, 2022,       [27] M. Goldszmidt, J. Pearl, On the relation between ratio-
     Proceedings, volume 13404 of LNCS, Springer, 2022,               nal closure and system-z, in: Proceedings of the Third
     pp. 1–8. doi:10.1007/978-3-031-15791-2_1.                        International Workshop on Nonmonotonic Reasoning,
[17] C. Beierle, A. Spang, J. Haldimann, A Partial MaxSAT             May 31 – June 3, 1990, pp. 130–140.
     approach to nonmonotonic reasoning with system              [28] N. Bjørner, L. de Moura, L. Nachmanson, C. M. Winter-
     W, in: Proceedings of the 37th International Florida             steiger, Programming Z3, Engineering Trustworthy
     Artificial Intelligence Research Society Conference,             Software Systems: 4th International School, SETSS
     2024. doi:10.32473/FLAIRS.37.1.135330.                           2018, Chongqing, China, April 7–12, 2018, Tutorial
[18] B. de Finetti, La prévision, ses lois logiques et ses            Lectures 4 (2019) 148–201.
     sources subjectives, Ann. Inst. H. Poincaré 7 (1937)        [29] M. Gario, A. Micheli, Pysmt: a solver-agnostic library
     1–68. Engl. transl. Theory of Probability, J. Wiley &            for fast prototyping of smt- based algorithms, in: SMT
     Sons, 1974.                                                      Workshop 2015, 2015.
[19] C. Komo, C. Beierle, Nonmonotonic inferences with           [30] N. S. Bjørner, A. Phan, L. Fleckenstein, 𝜈z - an op-
     qualitative conditionals based on preferred structures           timizing SMT solver, in: C. Baier, C. Tinelli (Eds.),
     on worlds, in: U. Schmid, F. Klügl, D. Wolter                    Tools and Algorithms for the Construction and Analy-
     (Eds.), KI 2020: Advances in Artificial Intelligence -           sis of Systems - 21st International Conference, TACAS
     43rd German Conference on AI, Bamberg, Germany,                  2015, Held as Part of the European Joint Confer-
     September 21-25, 2020, Proceedings, volume 12325                 ences on Theory and Practice of Software, ETAPS
     of LNCS, Springer, 2020, pp. 102–115. doi:10.1007/               2015, London, UK, April 11-18, 2015. Proceedings,
     978-3-030-58285-2_8.                                             volume 9035 of LNCS, Springer, 2015, pp. 194–199.
[20] J. Pearl, System Z: A natural ordering of defaults               doi:10.1007/978-3-662-46681-0_14.
     with tractable applications to nonmonotonic reason-         [31] S. Kutsch, C. Beierle, InfOCF-Web: An online tool
     ing, in: Proc. of the 3rd Conf. on Theoretical Aspects           for nonmonotonic reasoning with conditionals and
     of Reasoning About Knowledge (TARK’1990), Morgan                 ranking functions, in: Z. Zhou (Ed.), Proceedings of the
     Kaufmann Publ. Inc., San Francisco, CA, USA, 1990,               Thirtieth International Joint Conference on Artificial
     pp. 121–135.                                                     Intelligence, IJCAI 2021, ijcai.org, 2021, pp. 4996–4999.
[21] C. Beierle, C. Eichhorn, G. Kern-Isberner, Skeptical             doi:10.24963/ijcai.2021/711.
     inference based on c-representations and its charac-        [32] M. von Berg, A. Sanin, C. Beierle, An implementation
     terization as a constraint satisfaction problem, in:             of nonmonotonic reasoning with c-representations
     M. Gyssens, G. Simari (Eds.), Foundations of Informa-            using an SMT solver, Int. J. Approx. Reason. 175 (2024)
     tion and Knowledge Systems - 9th International Sym-              109285. doi:10.1016/j.ijar.2024.109285.
     posium, FoIKS 2016, Linz, Austria, March 7–11, 2016.        [33] J. Haldimann, C. Beierle, G. Kern-Isberner, T. Meyer,
     Proceedings, volume 9616 of LNCS, Springer, 2016, pp.            Conditionals, infeasible worlds, and reasoning with
     65–82. doi:10.1007/978-3-319-30024-5_4.                          system W, The International FLAIRS Conference
[22] J. Haldimann, C. Beierle, Properties of system W and             Proceedings 36 (2023). doi:10.32473/flairs.36.
     its relationships to other inductive inference operators,        133268.
     in: I. Varzinczak (Ed.), Foundations of Information and     [34] J. P. Haldimann, T. Meyer, G. Kern-Isberner, C. Beierle,
     Knowledge Systems - 12th International Symposium,                Rational closure extension in spo representable in-
     FoIKS 2022, Helsinki, Finland, June 20-23, 2022, Pro-            ductive inference operators, in: S. Gaggl, M. V.
     ceedings, volume 13388 of LNCS, Springer, 2022, pp.              Martinez, M. Ortiz (Eds.), Logics in Artificial Intel-
     206–225. doi:10.1007/978-3-031-11321-5_12.                       ligence 18th European Conference, JELIA 2023, Dres-
[23] J. Haldimann, C. Beierle, Characterizing multiprefer-            den, Germany, September 20–22, 2023, Proceedings,
     ence closure with system W, in: F. D. de Saint-Cyr,              volume 12678 of LNCS, Springer, 2023, pp. 561–576.
     M. Öztürk-Escoffier, N. Potyka (Eds.), Scalable Uncer-           doi:10.1007/978-3-031-43619-2_38.
     tainty Management - 15th International Conference,          [35] C. Beierle, J. Haldimann, L. Schwarzer, CLKR – Con-
     SUM 2022, Paris, France, October 17-19, 2022, Proceed-           ditional Logic and Knowledge Representation, KI –
     ings, volume 13562 of LNCS, Springer, 2022, pp. 79–91.           Künstliche Intelligenz (2024). URL: https://doi.org/10.
     doi:10.1007/978-3-031-18843-5_6.                                 1007/s13218-024-00842-z.
[24] J. Haldimann, C. Beierle, Approximations of system          [36] M. Thimm, Tweety: A comprehensive collection of
     W for inference from strongly and weakly consistent              java libraries for logical aspects of artificial intelli-
     belief bases, Int. J. Approx. Reason. 175 (2024) 109295.         gence and knowledge representation, in: C. Baral,
     doi:10.1016/j.ijar.2024.109295.                                  G. D. Giacomo, T. Eiter (Eds.), Principles of Knowl-
[25] J. Larrosa, E. Rollon, Towards a better understanding of         edge Representation and Reasoning: Proceedings of
     (partial weighted) MaxSAT proof systems, in: L. Pulina,          the Fourteenth International Conference, KR 2014, Vi-
     M. Seidl (Eds.), Theory and Applications of Satisfia-            enna, Austria, July 20-24, 2014, AAAI Press, 2014, pp.
     bility Testing - SAT 2020 - 23rd International Con-              528–537. URL: http://www.aaai.org/ocs/index.php/KR/
     ference, Alghero, Italy, July 3-10, 2020, Proceedings,           KR14/paper/view/7811.
     volume 12178 of LNCS, Springer, 2020, pp. 218–232.          [37] C. Beierle, C. Eichhorn, S. Kutsch, A practical compar-
     URL: https://doi.org/10.1007/978-3-030-51825-7_16.               ison of qualitative inferences with preferred ranking
[26] D. Lehmann, What does a conditional knowledge base               models, KI – Künstliche Intelligenz 31 (2017) 41–52.
     entail?, in: R. J. Brachman, H. J. Levesque, R. Reiter           doi:10.1007/s13218-016-0453-9.
[38] A. Labecki, System Z default reasoning solver, 2017.
     URL: https://github.com/alabecki/System-Z, (accessed
     on 19/07(2924).
[39] J. Haldimann, A. Osiak, C. Beierle, Modelling and
     reasoning in biomedical applications with qualitative
     conditional logic, in: U. Schmid, F. Klügl, D. Wolter
     (Eds.), KI 2020: Advances in Artificial Intelligence
     - 43rd German Conference on AI, volume 12325 of
     LNCS, Springer, 2020, pp. 283–289. doi:10.1007/
     978-3-030-58285-2_24.