Using SAT and Partial MaxSAT for Reasoning with System Z and System W

Abstract

Nonmonotonic reasoning from conditional belief bases typically depends on a structure over possible worlds that relies on the verification 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 problems 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 implementing 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

Conditionals play a major role in knowledge representation and reasoning, and many diferent semantics have been proposed for conditional belief bases, like probability distributions, plausibility orderings, possibility distributions, ranking functions and special instances of them, or conditional objects (see, e.g., [ 1, 2, 3, 4, 5, 6, 7, 8 ]). However, software systems implementing any of these inference methods have attracted much less attention. Any such implementation of inference with respect to a conditional belief base Δ has to cope with the number of worlds growing exponentially with the number of propositional variables occurring in Δ. For addressing this practical side of nonmonotonic reasoning, we consider Pearl’s well-known system Z [ 9 ], and system W [ 10 ] that exhibits some notable properties like extending system Z and thus rational closure [ 11 ], avoiding 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 [ 16 ] severely limits the number of propositional variables in Δ to about 20 for practical applications, corresponding to about one million worlds, recently an implementation of reasoning with system W using partial MaxSAT problems has been developed, with first evaluation results of up to 60 variables and thus 260 worlds [ 17 ].

This paper extends our work presented in [ 17 ] in several directions, providing the following main contributions: • We elaborate the approach in [ 17 ] in more detail and provide a formal correctness proof for its system W inference algorithm SWinf. • We extend its empirical evaluation, demonstrating that it scales up system W inference up to 120 variables and thus 2120 worlds and to belief bases of up to 200 conditionals. • We show how the approach can be transferred, yielding a SAT-based realization of system Z. 22nd International Workshop on Nonmonotonic Reasoning, November 24, 2024, Hanoi, Vietnam

[e-mail] (C. Beierle); [e-mail] (A. Spang); [e-mail] (J. Haldimann)

0000-0002-0736-8516 (C. Beierle); 0000-0002-2618-8721 (J. Haldimann) © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). • We give a correctness proof for our system Z inference algorithm SZinf. • We implement system Z correspondingly, outperforming previous implementations and allowing for signature and knowledge base sizes that have not been possible before.

This paper is organized as follows. After briefly recalling the background on conditional logic in Section 2 and system W in Section 3, we present and illustrate our algorithm SWinf for system W in Section 4 and prove its correctness in Section 5. We adapt this approach for system Z in Section 6, illustrate the resulting algorithm SZinf and prove this algorithm’s correctness in Section 7. Finally we evaluate the runtimes of our new algorithms for system W and system Z in Section 8 before concluding and pointing out future work in Section 9.

2. Background: Conditional Logic

A (propositional) signature is a finite set Σ of propositional variables, and ℒΣ denotes the propositional language over Σ. We may denote a conjunction ∧ by and a negation ¬ by . The set of interpretations over a signature Σ, also called worlds, is ΩΣ. We may identify a world with the corresponding complete conjunction of all elements Σ in either positive or negated form. An ∈ ΩΣ is a model of ∈ ℒΣ if holds in , denoted as |= , and the set of models of is Mod Σ() = { ∈ ΩΣ | |= }, sometimes denoted as Ω. A formula entails a formula , written |= , if Mod Σ() ⊆ Mod Σ(). Furthermore, for ∈ ℒΣ and ⊆ ℒ Σ, we use the notation |= if |= for every ∈ ; Ω = { ∈ ΩΣ | |= }; = { | ∈ }; and ∧ = ∧ 1 ∧ . . . ∧ for = {1, . . . , }.

A conditional (|) connects two formulas , and represents the rule “If then usually ”. The conditional language over Σ is (ℒ|ℒ)Σ = {(|) | , ∈ ℒΣ}. A belief base Δ is a finite set of conditionals. For a world , a conditional (|) is either verified by if |= , falsified by if |= , or not applicable to if |= [ 18 ]. An example for semantics of conditionals are functions : ΩΣ → N such that () = 0 for at least one ∈ ΩΣ, called ranking functions or ordinal conditional functions (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 |∼ if ≡ ⊥ or () < ().

(1)

3. System W

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 inference operator is System W [ 19, 10 ] which takes into account the tolerance information expressed by the Z-partition (also called ordered partition) of a belief base Δ, defined in the following.

Definition 1 (Z-partition OP (Δ) [ 9 ]). Let Δ = {(1|1), . . . , (|)} be a belief base. A conditional (|) is tolerated by a set of conditionals Δ if there exists a world ∈ ΩΣ that verifies (|) and does not falsify any conditional in Δ, i.e., |= and |= ⋀︀ =1( ∨ ).

The Z-partition OP (Δ) = (Δ0, . . . , Δ) of a belief base Δ is the partition of Δ where each Δ is the (with respect to set inclusion) maximal subset of ⋃︀ = Δ that is tolerated by ⋃︀ = Δ .

It is well-known that OP (Δ) exists if Δ is consistent; moreover, because the Δ are chosen inclusion-maximal, the Z-partition is unique [ 20 ]. System W combines the Z-partition with the structural information about which conditionals are falsified by a world, yielding the preferred structure on worlds <wΔ underlying system W.

Definition 2 ( , preferred structure <wΔ on worlds [ 19, 10 ]). Let Δ = {(1|1), . . . , (|)} with OP (Δ) = (Δ0, . . . , Δ). For = 0, . . . , , the function maps worlds to the set of falsified conditionals from the set Δ : () := { ∈ Δ | |= }, w The preferred structure on worlds is the binary relation <Δ defined by, for , ′ ∈ ΩΣ: <wΔ ′ if there exists ∈ {0 , . . . , } such that () = (′) () ⫋ (′) .

∀ ∈ { + 1 , . . . , }, and

Thus, <wΔ ′ if and only if falsifies strictly fewer conditionals than ′ in the partition with the biggest index where the conditionals falsified by and ′ difer. Definition 3 (system W, |∼ wΔ[ 10 ]). Let Δ be a consistent belief base and let , ∈ ℒΣ be formulas. Then is a system W inference from (in the context of Δ), denoted |∼ wΔ , if we have: for every ′ ∈ Ω there is an ∈ Ω such that <wΔ ′ . (2) (3) (4)

Example 1 (Δbird ). Let Σ = {, , , } represent birds, penguins, flying things and winged things, and let Δbird contain 1 = ( |), 2 = ( |), 3 = (|), and 4 = (|). E.g., 1 expresses “birds usually fly”. Then OP (Δbird ) = (Δ0, Δ1) with Δ0 = {( |), (|)} and w Δ1 = {( |), (|)}. Using <Δbird (Figure 1), we can check that |∼ wΔbird holds, i.e., that penguins usually have wings is a system W inference in the context of Δbird .

System W captures system Z in the sense that every entailment that is possible with system Z is also possible with system W, i.e., the system W inferences of a belief base Δ are a superset of the system Z inferences of Δ. Furthermore, there are belief bases where this superset relationship is strict, i.e., where system W licenses strictly more inferences than system Z [ 10 ]. System W strictly extends also c-inference [ 21, 10 ]; further properties of system W and its relationshsips to other inductive inference operators are described in [ 22, 23, 24 ].

For a set and a partial order < on , the minimal elements of ⊆ are denoted by: min(, <) = { ∈ | there is no ′ ∈ s.t. ′ < }. Because <wΔ is a strict partial order [ 10 ], Definition 3 directly implies that is sufifces to consider only the <wΔ-minimal worlds for checking whether |∼ wΔ holds.

Proposition 1 (|∼ wΔ). Let Δ be a consistent belief base and , ∈ ℒΣ. Then |∼ wΔ if for every ′ ∈ min(Ω , <wΔ) there is an ∈ min(Ω , <wΔ) such that <wΔ ′ .

4. Algorithm SWinf : System W

Inference using MaxSAT

In this section we introduce the algorithm SWinf(Δ, , ) (system W inference with Partial MaxSAT, Algorithm 1) [ 17 ] which takes a belief base Δ and two formulas , as input and answers the question whether |∼ wΔ holds. Implementing system W by computing the relation <wΔ [ 16 ] will work for small signatures but does not scale well because of the number of worlds to be considered grows exponentially with the size of the signature. Therefore, we will employ Partial MaxSAT concepts [ 25 ] in SWinf and utilize the power of current SAT-solvers. Given a set of formulas of soft constraints and a set of formulas of hard constraints the extended partial maximum satisfiability 1: let OP (Δ) = (Δ0, . . . , Δ) Algorithm 1 SWinf(Δ, , ) Input: consistent belief base Δ and formulas , Output: Yes if |∼ wΔ , and No otherwise 2: function recWinf (, ) 3: MCS (nf (Δ ), ∪ {}) 4: MCS (nf (Δ ), ∪ {}) ← ℱ ← 5: if ¬(∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′) then 6: return No 7: for all ∈ ∩ ℱ do 8: if = 0 then 9: return No 10: new ← (nf (Δ ) ∖ ) ∪ 11: if recWinf ( − 1, ∪ new ) = No then 12: return No 13: return Yes 14: end function 15: return recWinf (, ∅) problem EPMaxSAT (, ) is the optimization problem of maximizing the number of satisfied formulas in over all interpretations ∈ Ω and determining all subsets of that are maximal with this property.

Definition 4 (MCS (, )). Let = {1, . . . , } ⊆ ℒ Σ be a set of formulas called soft constraints, and let = {1, . . . , ℎ} ⊆ ℒ Σ be a set of formulas called hard constraints. A maximal satisfiable subset (MSS) with respect to (, ) is a set ⊆ such that ∪ is (classically) consistent and for every ′ ⊆ with ⫋ ′ the set ′ ∪ is not consistent. A set ⊆ is a minimal correction subset (MCS) with respect to (, ) if ∖ is an MSS w.r.t. (, ). Then, MCS (, ) denotes the set of all MCS w.r.t. (, ).

For using the concepts of MSS and MCS in our context, we rely in particular on the non-falsification of conditionals. For a conditional (|), the formula ∨ expressing its non-f alsification is denoted by nf (|), and nf is extended canonically to a set Δ of condtionals. Thus nf (Δ) = { ∨ | (|) ∈ Δ} nf (Δ) = { | (|) ∈ Δ} are the sets of non-falsifying and falsifying formulas, respectively, for the conditionals in Δ.

Example 2. Let Δbird and OP (Δbird ) = (Δ0, Δ1) as in Example 1. For = nf (Δ1) and = {} we get MSS (nf (Δ1), {}) = MSS ({ ∨ , ∨ }, {}) = {{ ∨ , ∨ }}, and thus MCS (nf (Δ1), {}) = {∅}. For = nf (Δ0) and = nf (Δ1) ∪ {} we get

MSS (nf (Δ0), nf (Δ1) ∪ {}) =MSS ({ ∨ , ∨ }, { ∨ , ∨ , }) ={{ ∨ }} and thus MCS (nf (Δ0), nf (Δ1) ∪ {}) = {{ ∨ }}.

In addition to using the minima as in Proposition 1 for computing |∼ wΔ, SWinf exploits the fact that the underlying relation <wΔ ′ (cf. Equation (2)) can be determined by iteratively considering the subbases in OP (Δ) = (Δ0, . . . , Δ) starting from the the highest partition element Δ. If () ̸= (′) we can decide whether <wΔ ′ or ̸<wΔ ′ holds after considering ; only in case that () = (′) for all ∈ {, . . . , } we continue by considering the next lower element Δ− 1.

Assume we have Δ with OP (Δ) = (Δ0, . . . , Δ). The central part of SWinf is the recursive function recWinf that takes the index for one of the sets in the Z-partition and a set of formulas as arguments. It is initially called for the last part Δ of the Z-partition. Each set in = MCS (nf (Δ), {}) corresponds to a maximal selection of conditionals in Δ such that there is a model of not falsifying them, and thus to a selection of worlds that falsify a minimal set of conditionals in Δ. Analogously, this holds for ℱ = MCS (nf (Δ), {}) and . If there is an ∈ ℱ for which there is no ′ ∈ with ⊆ ′, there is a world ′ ∈ Mod Σ() for which there is no world ∈ Mod Σ() with () ⊆ (′). Thus, if the condition in Line 5 holds, we have that ̸|∼ wΔ . Otherwise, we continue to consider the intersection ∩ ℱ . Each set ∈ ∩ ℱ 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 all inclusions we considered in Line 5 are strict inclusions and we have |∼ wΔ . Otherwise, for each such we need to consider the parts of the Z-partition with lower indices to check whether for each world ′ ∈ Mod Σ() that falsifies the conditionals in there is a world ∈ Mod Σ() that falsifies the conditionals in . To do this, we add (nf Δ ∖ ) ∪ as hard constraints to fix the falsification behaviour on Δ and call the function recWinf recursively.

Example 3. Executing SWinf(Δbird , , ) results in two successive calls of recWinf involving the following values and conditions, cf. Example 2: recWinf ( = 1, = ∅) = {∅} ℱ = {∅} (∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′) = true ∩ ℱ = {∅} = 1 > 0 return Yes if recWinf (0, { ∨ , ∨ }) = Yes recWinf ( = 0, = { ∨ , ∨ }) = {{ ∨ }} ℱ = {{ ∨ , ∨ }} (∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′) = true ∩ ℱ = ∅ → return Yes Thus, SWinf(Δbird , , ) returns Yes, and |∼ wΔbird .

When asking whether can be inferred from in the context of Δbird with system W, SWinf(Δbird , , ) yields No: recWinf ( = 1, = ∅) = {∅} ℱ = {∅} (∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′) = true ∩ ℱ = {∅} = 1 > 0 return Yes if recWinf (0, { ∨ , ∨ }) = Yes recWinf ( = 0, = { ∨ , ∨ }) = {{ ∨ , ∨ }} ℱ = {{ ∨ }} (∀ ′ ∈ ℱ ∃ ∈ . ⊆ return No ′) = false →

5. Correctness Proof for SWinf

An important characteristic of the search space of the algorithm SWinf is described by the falsification and nonfalsification behaviour of the conditionals in Δ+1∪· · ·∪ Δ for a given ∈ {0, . . . , }. For formally characterizing this behaviour we use the following notion.

Definition 5 (nf/f -condition for (Δ, )). Let OP (Δ) = (Δ0, . . . , Δ), and let ∈ {0, . . . , }. A set of formulas is a non-falsifying/falsifying condition (nf/f -condition) for (Δ, ) if there are, for ∈ { +1, . . . , } sets Δn f , Δf ⊆ Δ such that Δ = Δn f ∪ Δf and Δn f ∩ Δf = ∅, and =

⋃︁ ∈{+1,...,}

nf (Δn f ) ∪ nf (Δf )

Thus, an nf/f -condition for (Δ, ) contains either the non-falsifying formula ∨ or the falsifying formula for every conditional (|) ∈ Δ+1∪. . .∪Δ; this way the nf/f -condition ensures that for any two worlds , ′ ∈ ΩΣ with |= and ′ |= we have () = (′) for all ∈ { + 1, . . . , }.

To prove the correctness of SWinf, we prove the following three lemmas first. Lemma 1 describes the condition in Line 5 of SWinf.

Lemma 1. Let Δ be a consistent belief base with OP (Δ) = (Δ0, . . . , Δ), let ∈ {0, . . . , }, , ∈ ℒΣ, and be an nf/f -condition for (Δ, ). Let = MCS (nf (Δ ), ∪ {}) and ℱ = MCS (nf (Δ ), ∪ {}).

Then ¬(∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′) holds if there is a world ′ ∈ Mod Σ( ∧ ) such that for all ∈ Mod Σ( ∧ ) it holds that () ̸⊆ (′).

Proof. Direction ⇒: Assume ¬(∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′); this is equivalent to ∃ ′ ∈ ℱ ∀ ∈ . ̸⊆ ′. Let ′ ∈ ℱ be such a set with ∀ ∈ . ̸⊆ ′.

Let ′ ∈ Mod Σ( ∧ ) be a world that satisfies nf (Δ) ∖ ′; such a world exists because nf (Δ) ∖ ′ is consistent by the construction of MCS. Let be any world in Mod Σ( ∧ ). Let ∈ such that ⊆ nf ( ()); such an exists because nf ( ()) is a (not necessarily minimal) correction set. By assumption, ̸⊆ ′. Therefore, also nf ( ()) ̸⊆ ′. Because MCS yields minimal correction sets, ′ falsifies all conditionals ∈ Δ with nf () ∈ ′, and ′ does not falsify the conditionals ∈ Δ with nf () ∈/ ′; in summary nf ( ()) = ′. With nf ( ()) ̸⊆ ′ we have () ̸⊆ (′).

Direction ⇐: We prove this direction by contraposition. Assume that ∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′. Let ′ be any world in Mod Σ( ∧ ); we need to show that there is an ∈ Mod Σ( ∧ ) such that () ⊆ (′).

Let ′ ∈ ℱ such that ′ ⊆ nf ( (′)); such an ′ exists because nf ( (′)) is a (not necessarily minimal) correction set. By assumption there is an ∈ such that because ′n.fL(eΔt )∈∖ MoidsΣc(onnfsi(sΔten)t ∖byt)h;esudcehfiniatiownorolfdMexCiSst.s ⊆ Because MCS yields minimal correction sets, falsifies all conditionals ∈ Δ with nf () ∈ . Furthermore, ′ falsifies all conditionals ∈ Δ with nf () ∈ ′. Therefore, ⊆ ′ implies () ⊆ (′).

Lemma 2 describes conditions on sets of falsified conditionals that require a certain set to be in ∩ ℱ . Lemma 2. Let Δ be a consistent belief base with OP (Δ) = (Δ0, . . . , Δ), let ∈ {0, . . . , }, , ∈ ℒΣ, and let be an nf/f -condition for (Δ, ). Let = MCS (nf (Δ ), ∪ {}) and ℱ = MCS (nf (Δ ), ∪ {}).

Let ∈ Mod Σ( ∧ ) such that there is no * ∈ Mod Σ( ∧ ) with (* ) ⫋ (), and let ′ ∈ Mod Σ( ∧ ) such that there is no ′* ∈ Mod Σ( ∧ ) with (′* ) ⫋ (′). Then () = (′) implies that there is an ∈ ∩ ℱ with , ′ |= nf (Δ ) ∖ .

Proof. Assume that () = (′). Then = nf ( ()) is a correction set with respect to (nf (Δ ), ∪ {}), because is a model of all nf () with ∈ Δ ∖ (). We need to show that is a minimal correction set. Towards a contradiction assume that there is an ∈ nf ( ()) such that = ( ∪ {}) ∪ nf (Δ ) ∖ nf ( ()) ∪ {} is consistent. Let be a model of . The world does not falsify any of the conditionals in Δ ∖ () because it is a model of nf (Δ ) ∖ nf ( ()). There must be an ∈ () such that nf () = . The world also does not falsify because it is a model of . Therefore, () ⫋ (). This contradicts that there is no * ∈ Mod Σ( ∧) with (* ) ⫋ (); therefore is indeed a minimal correction set with respect to (nf (Δ ), ∪ {}).

Analogously we can show that = nf ( (′)) = nf ( (′)) is a minimal correction set with respect to (nf (Δ ), ∪ {}). In summary, ∈ ∩ ℱ and , ′ |= nf (Δ ) ∖ .

Lemma 3 describes an efect of a set ∈ ∩ ℱ on sets of falsified conditionals.

Lemma 3. Let Δ be a consistent belief base with OP (Δ) = (Δ0, . . . , Δ), let ∈ {0, . . . , }, , ∈ ℒΣ, and let be an nf/f -condition for (Δ, ). Let = MCS (nf (Δ ), ∪ {}) and ℱ = MCS (nf (Δ ), ∪ {}). Δ | nf () ∈ }.

Then, for ∈ ∩ ℱ and every ∈ Mod Σ( ∧ ) with ′ |=|= nnff((ΔΔ))∖∖,,aintdhoelvdesrythat′ ∈ (M)od=Σ( (∧′)=){wit∈h Proof. Let = { ∈ Δ | nf () ∈ }. Because |= nf (Δ ) ∖ , we have that falsifies no conditionals in Δ ∖ , i.e., () ⊆ . Because is a minimal correction set in , there is no ∈ that does is not falsified by : if there were such an then ∖ {nf ()} would be an even smaller correction set. Therefore, () = .

Analogously we can show that (′) = .

Now we can use Lemma 1, Lemma 2, and Lemma 3 to show Proposition 2 on the output of the recursive algorithm recWinf .

Proposition 2. Let Δ be consistent with OP (Δ) = (Δ0, . . . , Δ), let ∈ {0, . . . , }, , ∈ ℒΣ, and let be an nf/f -condition for (Δ, ). Then recWinf (, ) returns “Yes” if for every ′ ∈ Mod Σ( ∧ ) there is an ∈ Mod Σ( ∧ ) with <wΔ ′. (5) Proof. We prove this by induction over . Let We show that (6) is equivalent to (5) by showing both directions of this equivalence.

Direction ⇒: Assume (6) holds. Let ′ be any world in Mod Σ( ∧ ). Because is an nf/f -condition for (Δ, 0), every model of falsifies the same conditionals in Δ1, . . . , Δ. Therefore, we need to show that there is a world ∈ Mod Σ( ∧ ) with 0() ⫋ 0(′).

W.l.o.g. assume that there is no ′* with 0(′* ) ⫋ 0(′). With Lemma 1 and the first part of (6) we have that there is an ∈ Mod Σ( ∧ ) with 0() ⊆ 0(′). W.l.o.g. assume that there is no * with 0(* ) ⫋ 0(). Towards a contradiction, assume that 0() = 0(′). With Lemma 2 we have that there is an ∈ ∩ ℱ which contradicts (6). Therefore, 0() ⫋ 0(′).

Direction ⇐: Assume that (5) holds. Because is an nf/f -condition for (Δ, 0), every model of falsifies the same conditionals in Δ1, . . . , Δ. Therefore, with Lemma 1 it follows that the part left of the and in (6) holds.

It is left to show ∩ ℱ = ∅. Towards a contradiction assume that ∩ ℱ ̸= ∅, i.e., there is an ∈ ∩ ℱ . Because is a correction set of ℱ , there is an ′ ∈ Mod Σ( ∧ ) with ′ |= nf (Δ0) ∖ . By (5) there is an ∈ Mod Σ( ∧ ) with <wΔ ′. Because <wΔ ′ and is an nf/f condition for (Δ, 0) we have 0() ⊆ 0(′) and therefore |= nf (Δ0) ∖ . W.l.o.g. assume that there is no * ∈ Mod Σ( ∧ ) with * |= nf (Δ0) ∖ and 0(* ) ⫋ 0(). By Lemma 3 we have 0() = 0(′). This implies () = (′) and contradicts <wΔ ′. Therefore, ∩ ℱ = ∅ and (6) holds.

Induction Step: Let > 0 and assume the proposition holds for ′ = − 1. We show that recWinf (, ) returns “Yes” if (5) holds by showing both directions of this equivalence.

Direction ⇒: Assume that recWinf (, ) returns “Yes”; therefore the algorithm reaches Line 13 at some point. It is left to show that (5) holds. Let ′ be any world in Mod Σ( ∧ ). W.l.o.g. assume that there is no ′* with (′* ) ⫋ (′).

The algorithm passes Lines 5 and 6 without returning “No”. Therefore, there is a world ∈ Mod Σ( ∧ ) such that () ⊆ (′). W.l.o.g. assume that there is no * with (* ) ⊊ (). We can distinguish two cases.

Case 1: () ⫋ (′).

Because is an nf/f -condition for (Δ, ), all models of , including and ′, falsify the same conditionals in Δ+1, . . . , Δ. Therefore, <wΔ ′.

Case 2: () = (′).

By Lemma 2 there is an ∈ ∩ℱ with , ′ |= nf (Δ )∖. Because is a minimal correction set in both and ℱ , we have , ′ |= . Because the algorithm passes Lines 7–12 without returning “No”, for new ← (nf (Δ ) ∖ ) ∪ the function call recWinf ( − 1, ∪ new ) returns “Yes”. By construction, ∪ new is an nf/f -condition for (Δ, − 1). tFhuerrteheisrmanore, |= ∧. Using the induction hypothesis, ∈ Mod Σ( ∧ ) with <wΔ ′.

In summary, (5) holds.

Direction ⇐: Assume that (5) holds. We need to show that recWinf (, ) returns “Yes”. With Lemma 1 and because is an nf/f -condition for (Δ, ), we have that ¬(∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′) does not hold; therefore the algorithm passes Lines 5 and 6 without returning “No”.

It is left to show that the algorithm passes Lines 7–12 without returning “No”. Let be any set in ∩ ℱ . By construction, new is an nf/f -condition for (Δ, − 1). Let ′ be any world in Mod Σ( ∧ new ∧ ). Because ′ |= new we have |= nf (Δ ) ∖ . Because of (5), there is a world ∈ Mod Σ( ∧ ) with <wΔ ′. Using ∀ ′ ∈ ℱ ∃ ∈ . ⊆ ′ again, we know that () ⊆ (′) = { ∈ Δ | nf () ∈ } (the last equation holding due to Lemma 3); therefore |= nf (Δ )∖. Using Lemma 3 again, we have () = { ∈ Δ | nf () ∈ } and therefore |= new . Hence, for every ′ ∈ Mod Σ( ∧ new ∧ ) there is an ∈ Mod Σ( ∧ new ∧ ) with <wΔ ′. Employing the induction hypothesis, we have that recWinf ( − 1, ∪ new ) returns “Yes”.

Thus, algorithm passes Lines 7–12 without returning “No”, and then returns “Yes” in Line 13.

Now it is straightforward to show the correctness of SWinfwith Proposition 2.

Theorem 1. Given a consistent belief base Δ and , ∈ ℒΣ, the call SWinf(Δ, , ) always terminates, and it returns “Yes” if |∼ wΔ .

Proof. SWinf(Δ, , ) terminates because , ℱ and thus also ∩ ℱ are always finite sets, and for every recursive call the index is decreased by one. SWinf(Δ, , ) returns “Yes” if recWinf (, ∅) returns “Yes”. Because ∅ is an nf/f -condition for (Δ, ), according to Proposition 2, this happens if for every ∈ Mod Σ(∅ ∧ ) there is an ′ ∈ Mod Σ(∅ ∧ ) with <wΔ ′, which is equivalent to |∼ wΔ .

6. Algorithm SZinf for System Z

Pearl’s system Z [ 20 ] is a well-known inductive inference operator that was shown to coincide with rational closure [ 26, 27 ] Definition 6 (System Z [ 20 ]). Let Δ be consistent with OP (Δ) = (Δ0, . . . , Δ). The ranking function Δ is deifned as follows: If ∈ ΩΣ does not falsify any conditional in Δ, then let Δ() := 0. Otherwise, let Δ be the last part in OP (Δ) that contains a conditional falsified by , and let Δ() := + 1. System Z maps Δ to the inference relation |∼ Δ induced by Δ according to (1).

For any consistent Δ, the function Δ is the unique least ranking model of Δ [ 20 ].

Example 4. For the belief base Δbird from Example 1 we have OP (Δbird ) = (Δbird 0, Δbird 1) with Δbird 0 = {1, 4} and Δbird 1 = {2, 3}. The Δbird () Z-ranking function induced by Δbird is displayed in Table 1. We have Δbird () = 0 and Δbird () = 2, and thus |∼ . Analogously, we can check that Δbird () = ΔΔbibridrd () = 1, yielding ̸|∼ Δbird .

Note that this also illustrate that system Z, in contrast to, e.g., system W, sufers from the drowning problem [ 12 ] because the birds property of having wings is drowned for penguins because penguins are exceptional birds with respect to the property flying.

Implementations of system Z have to cope with the exponentially growing number of worlds for larger signatures. Based on the approach of SWinf we design a similar algorithm SZinf (Algorithm 2) for system Z.

One of the main diferences between system W and system Z is that, while <wΔ compares the sets of conditionals falsified by each world, Δ only takes into account the latest for which any conditional in Δ is falsified by each world. This simplifies the algorithm SZinf compared to SWinf in two ways.

First, instead of finding a minimal set of falsified conditionals in Δ with MCS (nf (Δ ), ∪ {˙}), it is sufifcient to check if there is a world with |= ˙ that falsifies no conditionals in Δ for each ˙ ∈ {, }. This does not even require solving a Partial MaxSAT problem; instead we just have to check two sets of formulas for their satisfiability.

Second, because there are no diferent minimal sets of falsified conditionals to choose from, we do not need an argument of the recursive function to keep track of the (non-)falsified conditionals in the previously considered parts of OP (Δ). Instead, we straightforwardly check the = nf (Δ)∪{˙}. satisfiability of ⋃︀

For determining whether entails , SZinf(Δ, , ) considers the parts in OP (Δ) beginning with the latest Δ. The main part of SZinf is a recursive function recZinf () whose argument is the index of the part of OP (Δ) that is considered next. For each Δ , the algorithm determines = SAT(⋃︀= nf (Δ)∪{}) and

= SAT(⋃︀= nf (Δ)∪{}). Note that for < , recZinf () is only called if +1 = (cf. Line 7), implying that Δ() < + 2. If = UNSAT, then Δ() ⩾ + 1 and thus Δ() ̸< Δ(), implying ̸|∼ Δ . If = SAT and = UNSAT, then we can conclude that Δ() < + 1 and Δ() ⩾ + 1 and thus Δ() < Δ(), implying |∼ Δ . If = SAT and = SAT, we continue by recursively calling recZinf ( − 1) to check the parts of OP (Δ) with a lower index. Line 14 contains the initial call to recZinf and the handling of the border case that the antecedent is an inconsistent formula.

Note that the function recZinf in SZinf can be easily rewritten to use a loop instead of recursion, but we decided to present it with recursive calls to point out the similarity to SWinf.

Example 5. Executing SZinf(Δbird , , ) yields two succesive calls of recZinf involving as values and conditions: recZinf ( = 1), ← SAT , ̸= UNSAT , ← SAT , = SAT , ̸= 0, return No if recZinf (0) = No recZinf ( = 0), ← UNSAT , = UNSAT

⇒ return No

Thus, SZinf(Δbird , , ) returns No, and |̸∼ zΔbird .

7. Correctness Proof for SZinf

For proving the correctness of SZinf, we first show the following lemma connecting the satisfiablility of = ⋃︁ nf (Δ)∪{}

= to the rank of a formula .

Lemma 4. Let Δ be a consistent belief base with OP (Δ) = (Δ0, . . . , Δ), let ∈ {0, . . . , }, and let ∈ ℒΣ. 1. If is consistent, then Δ() < + 1. 2. If is not consistent, then Δ() ⩾ + 1.

Proof. Ad (1.): Assume that is consistent. Then there is a world with |= ⋃︀

= nf (Δ) and |= . Because |= ⋃︀

= nf (Δ), the world does not falsify any conditional in ⋃︀

= Δ, and thus Δ() < + 1. Because |= and Δ() = min{ Δ() | |= }, this implies Δ() < + 1.

Ad (2.): Assume that is not consistent. Then every world with |= falsifies at least one conditional in ⋃︀ = Δ. Therefore, Δ() ⩾ + 1.

Now we can prove the correctness of recZinf .

Proposition 3. Let Δ be a consistent belief base with OP (Δ) =ℒΣ( Δ.0,If. ..,Δ+1)a, nldet +∈1 are consistent, then {0, . . . , }, and let , ∈ recZinf () returns “Yes” if Δ() < Δ(). Proof. We prove this by induction over .

Base Case ( = 0): By assumption +1 and +1 are consistent, and thus, by Lemma 4 we have Δ() < + 2 = 2 and Δ() < + 2 = 2, implying that Δ(), Δ() ∈ {0, 1}.

If is consistent and is inconsistent, then by Lemma 4 we have Δ() = 0 and Δ() = 1 and thus Δ() < Δ(). In this case the checks in Lines 4 and 7 fail and recZinf returns “Yes”.

In all other cases we have Δ() ̸< Δ() and recZinf returns “No” because one of the checks in Lines 4 and 7 succeeds.

In both cases the proposition holds.

Induction Step: Let > 0 and assume the proposition holds for ′ = − 1. By assumption +1 and +1 are consistent, and thus, by Lemma 4 we have Δ() < + 2 and Δ() < + 2. We can distinguish several cases

Case 1: is inconsistent By Lemma 4 we have Δ() ⩾ + 1 implying that Δ() ̸< Δ(). Also, the check in Line 4 succeeds and recZinf returns “No”. The proposition holds.

Case 2: is consistent and is inconsistent By Lemma 4 we have Δ() < +1 and Δ() ⩾ +1 implying that Δ() < Δ(). The checks in Line 4 and 7 fail and recZinf returns “Yes”. The proposition holds.

Case 3: is consistent and is consistent In this case the function recZinf is called recursively for − 1. The preconditions for applying this proposition for ′ = − 1 are satisfied, and therefore, by the induction hypothesis, recZinf () returns “Yes” if Δ() < Δ(). The proposition holds.

Using Proposition 3, we can now show the correctness of SZinf.

Theorem 2. Given a consistent belief base Δ and , ∈ ℒΣ, the call SZinf(Δ, , ) always terminates, and it returns “Yes” if |∼ Δ .

Proof. For Δ≡⊥, ,thSuWs itnhfe( Δth,eor,em) hreotludrsnisn“tYheiss”c(acsfe..LFinoer 14) and |∼ the remainder of the proof assume that ̸≡ ⊥ .

SWinf(Δ, , ) terminates because for every recursive call of recZinf the index is decreased by one, and the algorithm terminates at latest for = 0. For = , the sets +1 and +1 are empty and are thus trivially consistent.

By Proposition 3, the call SWinf(Δ, , ) returns “Yes” if Δ() < Δ(), which is equivalent to |∼ Δ .

8. Implementation and Evaluation

Results

We implemented SWinf and SZinf in Python and using the SMT solver Z3 [ 28 ] accessed through the pySMT API [ 29 ].

In the implementation of SWinf, we used the optimizing features of the Z3 SMT Solver to find Pareto fronts [ 30 ] (which, in our case, is equivalent to finding the sets of all MSS and thus allows deriving the set of all MCS).

For checking the correctness of our implementations, we verified that the output of the implementations of SWinf and SZinf match the output of earlier implementations of system W [ 16 ] and of system Z [ 31 ]. For all queries with respect to all belief bases small enough to be processed by these older implementations without running into a timeout, the diferent implementations of system W and system Z, respectively, yielded exactly the same result.

For evaluating the implementations of SWinf and SZinf, belief bases and queries were constructed by a randomized scheme taking a signature Σ as input; a detailed description of this scheme and algorithms realizing it are given in [ 32 ]. Only consistent belief bases build during this process were used for benchmarking because system W as given in Definition 3 and system Z as given in Definition 6 are defined only for consistent belief bases; reasoning with system W with respect to belief bases that are only weakly consistent [ 33, 34 ] has been introduced only very recently [ 33, 24 ]. In the evaluation, belief bases with signature sizes |Σ| ranging from 6 to 120 and number of conditionals |Δ| ranging from 6 to 200 were considered. For diferent (|Σ|, |Δ|)-combinations, in summary, 2 800 belief bases and 28 000 queries were created; the belief bases and queries obtained thereby are available at the CLKR repository [ 35 ] at https://www.fernuni-hagen.de/wbs/clkr/ as problem set CLKR-PS004.

We benchmarked our (Partial Max-)SAT based Python implementations of SWinf and SZinf against existing Javabased approaches for inference according to system-W (WJ) and system-Z (ZJ) that both consider all possible worlds explicitly [ 16, 31 ]. No other previous system implementations of system W exist, and to the best of our knowledge all other existing implementations of system Z, e.g., [ 36, 37, 38 ], cannot handle belief bases over signature size of 50 or more.

Performance was assessed on a machine with an Intel i73770 CPU and 32GB RAM under Arch Linux (Linux kernel 6) and Python 3.11 (single threaded). Each implementation was tested on the full set of randomly generated belief bases and queries described above. The run times presented in Table 2 are averaged over 1,000 queries across 100 belief bases for every combination of (|Σ|, |Δ|). Time is presented in ms, timeout was set to 5 minutes.

The evaluation results in Table 2 show that only for the very smallest (|Σ|, |Δ|)-combinations with | | = 6 and

Σ |Δ| = 6 the Java-based implementations WJ and ZJ of system W and system Z, respectively, are faster than our implementations of SWinf and SZinf. Furthermore, for every (|Σ|, |Δ|) combination with |Σ| ⩾ 18 both WJ and ZJ ran into a timeout in our evaluation scenario, while SWinf and SZinf successfully cope with all (|Σ|, |Δ|) combinations up to |Σ| = 120 and |Δ| = 200. It is interesting to note that SZinfconsistently performs faster than SWinf in our evaluation only by a factor of up to 2 across all (|Σ|, |Δ|) combinations. In summary, this comparative evaluation showcases SWinf’s and SZinf’s superior scalability and ef|Σ| |Δ| WJ 16 18 20 30 40 50 60 80 100 120 60 80 120 160 60 100 160 200 60 80 120 160 200 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. ifciency, particularly in handling queries on larger belief bases within reasonable time frames.

9. Conclusions and Future Work

In this paper, we presented SAT and Partial MaxSAT based approaches for implementing nonmonotonic reasoning with system Z and system W. We presented the corresponding algorithms SZinf and SWinf and gave formal correctness proofs for them. The Python-based implementations of SZinf and SWinf use the power of current SAT and Partial MaxSAT solvers and scale up reasoning both with system Z and system W to a new dimension, easily coping with belief bases over 120 variables and containing up to 200 conditionals. This advancement also puts larger practical applications into reach for the first time.

Our current and future work includes extending the presented work in multiple ways. For instance, while the evaluation presented in Section 8 focuses on runtime, we will further evaluate SZinf and SWinf by taking also the memory consumption into account. We will also analyse the complexity of the algorithms. While previous practical applications were limited by small belief base sizes, we will address larger and more realistic scenarios in the medical and bio-medical domain as they have already been modelled with conditional logic [ 39 ], using the new opportunities opened up by the enriched power of our new implementations of nonmonotonic inference.

Acknowledgments This work was supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) 512363537, grant BE 1700/12-1 awarded to Christoph Beierle.

References

[1] E. Adams , The Logic of Conditionals, D. Reidel, Dordrecht, 1975 .

[2] D. Nute , Topics in Conditional Logic, D. Reidel Publishing Company, Dordrecht, Holland, 1980 .

[3] W. Spohn , Ordinal conditional functions: a dynamic theory of epistemic states , in: W. Harper, B. Skyrms (Eds.), Causation in Decision, Belief Change , and Statistics, II , Kluwer Academic Publishers, 1988 , pp. 105 - 134 .

[4] S. Kraus , D. Lehmann , M. Magidor , Nonmonotonic reasoning, preferential models and cumulative logics , Artif. Intell . 44 ( 1990 ) 167 - 207 .

[5] D. Dubois , H. Prade , Conditional objects as nonmonotonic consequence relationships, Special Issue on Conditional Event Algebra , IEEE Transactions on Systems, Man and Cybernetics 24 ( 1994 ) 1724 - 1740 .

[6] S. Benferhat , D. Dubois , H. Prade , Nonmonotonic reasoning, conditional objects and possibility theory , Artificial Intelligence 92 ( 1997 ) 259 - 276 .

[7] G. Kern-Isberner , Conditionals in nonmonotonic reasoning and belief revision , volume 2087 of LNAI , Springer, 2001 .

[8] C. Beierle , C. Eichhorn , G. Kern-Isberner , S. Kutsch , Properties and interrelationships of skeptical, weakly skeptical, and credulous inference induced by classes of minimal models , Artificial Intelligence 297 ( 2021 ) 103489 . doi: 10 .1016/j.artint. 2021 . 103489 .

[9] M. Goldszmidt , J. Pearl , Qualitative probabilities for default reasoning, belief revision, and causal modeling , Artificial Intelligence 84 ( 1996 ) 57 - 112 .

[10] C. Komo , C. Beierle , Nonmonotonic reasoning from conditional knowledge bases with system W, Ann . Math. Artif. Intell. 90 ( 2022 ) 107 - 144 . doi: 10 .1007/ s10472-021-09777-9.

[11] D. Lehmann , M. Magidor , What does a conditional knowledge base entail? , Artif. Intell . 55 ( 1992 ) 1 - 60 .

[12] S. Benferhat , C. Cayrol , D. Dubois , J. Lang , H. Prade , Inconsistency Management and Prioritized SyntaxBased Entailment , in: Proc. IJCAI'93 , volume 1 , Morgan Kaufmann Publishers, San Francisco, CA, USA, 1993 , pp. 640 - 647 .

[13] G. Kern-Isberner , C. Beierle , G. Brewka, Syntax splitting = relevance + independence: New postulates for nonmonotonic reasoning from conditional belief bases , in: D. Calvanese , E. Erdem, M. Thielscher (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the 17th International Conference, KR 2020 , IJCAI Organization, 2020 , pp. 560 - 571 . doi: 10 .24963/kr.2020/56.

[14] J. Haldimann , C. Beierle , Inference with system W satisfies syntax splitting , in: G. Kern-Isberner , G. Lakemeyer, T. Meyer (Eds.), Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning , KR 2022, Haifa, Israel. July 31 - August 5 , 2022 , 2022 , pp. 405 - 409 . doi: 10 .24963/kr.2022/41.

[15] J. Heyninck , G. Kern-Isberner , T. Meyer, J. P. Haldimann , C. Beierle , Conditional syntax splitting for non-monotonic inference operators , in: B. Williams , Y. Chen , J. Neville (Eds.), Proceedings of the 37th AAAI Conference on Artificial Intelligence , volume 37 , 2023 , pp. 6416 - 6424 . doi: 10 .1609/aaai.v37i5. 25789 .

[16] C. Beierle , J. Haldimann , D. Kollar , K. Sauerwald , L. Schwarzer , An implementation of nonmonotonic reasoning with system W , in: R. Bergmann , L. Malburg , S. C. Rodermund , I. J . Timm (Eds.), KI 2022: Advances in Articfiial Intelligence - 45th German Conference on AI , Trier, Germany, September 19-23 , 2022 , Proceedings, volume 13404 of LNCS , Springer, 2022 , pp. 1 - 8 . doi: 10 .1007/978-3- 031 -15791- 2 _ 1 .

[17] C. Beierle , A. Spang , J. Haldimann , A Partial MaxSAT approach to nonmonotonic reasoning with system W , in: Proceedings of the 37th International Florida Artificial Intelligence Research Society Conference , 2024 . doi: 10 .32473/FLAIRS.37.1.135330.

[18] B. de Finetti , La prévision, ses lois logiques et ses sources subjectives , Ann. Inst. H. Poincaré 7 ( 1937 ) 1 - 68 . Engl. transl. Theory of Probability, J. Wiley & Sons, 1974 .

[19] C. Komo , C. Beierle , Nonmonotonic inferences with qualitative conditionals based on preferred structures on worlds , in: U. Schmid , F. Klügl , D. Wolter (Eds.), KI 2020: Advances in Artificial Intelligence - 43rd German Conference on AI , Bamberg, Germany, September 21-25 , 2020 , Proceedings, volume 12325 of LNCS , Springer, 2020 , pp. 102 - 115 . doi: 10 .1007/ 978-3- 030 -58285- 2 _ 8 .

[20] J. Pearl , System Z : A natural ordering of defaults with tractable applications to nonmonotonic reasoning , in: Proc. of the 3rd Conf. on Theoretical Aspects of Reasoning About Knowledge (TARK ' 1990 ), Morgan Kaufmann Publ. Inc., San Francisco, CA, USA, 1990 , pp. 121 - 135 .

[21] C. Beierle , C. Eichhorn , G. Kern-Isberner , Skeptical inference based on c-representations and its characterization as a constraint satisfaction problem , in: M. Gyssens , G. Simari (Eds.), Foundations of Information and Knowledge Systems - 9th International Symposium, FoIKS 2016 , Linz, Austria, March 7- 11 , 2016 . Proceedings, volume 9616 of LNCS , Springer, 2016 , pp. 65 - 82 . doi: 10 .1007/978-3- 319 -30024- 5 _ 4 .

[22] J. Haldimann , C. Beierle , Properties of system W and its relationships to other inductive inference operators , in: I. Varzinczak (Ed.), Foundations of Information and Knowledge Systems - 12th International Symposium, FoIKS 2022 , Helsinki, Finland, June 20-23, 2022 , Proceedings, volume 13388 of LNCS , Springer, 2022 , pp. 206 - 225 . doi: 10 .1007/978-3- 031 -11321-5_ 12 .

[23] J. Haldimann , C. Beierle , Characterizing multipreference closure with system W , in: F. D. de Saint-Cyr, M. Öztürk-Escofier , N. Potyka (Eds.), Scalable Uncertainty Management - 15th International Conference, SUM 2022 , Paris, France, October 17-19 , 2022 , Proceedings, volume 13562 of LNCS , Springer, 2022 , pp. 79 - 91 . doi: 10 .1007/978-3- 031 -18843- 5 _ 6 .

[24] J. Haldimann , C. Beierle , Approximations of system W for inference from strongly and weakly consistent belief bases , Int. J. Approx. Reason . 175 ( 2024 ) 109295 . doi: 10 .1016/j.ijar. 2024 . 109295 .

[25] J. Larrosa , E. Rollon, Towards a better understanding of (partial weighted) MaxSAT proof systems , in: L. Pulina , M. Seidl (Eds.), Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3 - 10 , 2020 , Proceedings, volume 12178 of LNCS , Springer, 2020 , pp. 218 - 232 . URL: https://doi.org/10.1007/978-3- 030 -51825-7_ 16 .

[26] D. Lehmann , What does a conditional knowledge base entail? , in: R. J. Brachman , H. J. Levesque , R. Reiter (Eds.), Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR'89) . Toronto, Canada, May 15 -18 1989 , Morgan Kaufmann, 1989 , pp. 212 - 222 .

[27] M. Goldszmidt , J. Pearl , On the relation between rational closure and system-z , in: Proceedings of the Third International Workshop on Nonmonotonic Reasoning , May 31 - June 3, 1990 , pp. 130 - 140 .

[28] N. Bjørner , L. de Moura, L. Nachmanson, C. M. Wintersteiger , Programming Z3 , Engineering Trustworthy Software Systems: 4th International School, SETSS 2018 , Chongqing, China, April 7- 12 , 2018 , Tutorial Lectures 4 ( 2019 ) 148 - 201 .

[29] M. Gario , A. Micheli , Pysmt: a solver-agnostic library for fast prototyping of smt- based algorithms , in: SMT Workshop 2015 , 2015 .

[30] N. S. Bjørner , A. Phan , L. Fleckenstein, z - an optimizing SMT solver , in: C. Baier , C. Tinelli (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software , ETAPS 2015 , London, UK, April 11 - 18 , 2015 . Proceedings, volume 9035 of LNCS , Springer, 2015 , pp. 194 - 199 . doi: 10 .1007/978-3- 662 -46681-0_ 14 .

[31] S. Kutsch , C. Beierle, InfOCF-Web : An online tool for nonmonotonic reasoning with conditionals and ranking functions , in: Z. Zhou (Ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021 , ijcai .org, 2021 , pp. 4996 - 4999 . doi: 10 .24963/ijcai. 2021 /711.

[32] M. von Berg , A. Sanin , C. Beierle , An implementation of nonmonotonic reasoning with c-representations using an SMT solver , Int. J. Approx. Reason . 175 ( 2024 ) 109285 . doi: 10 .1016/j.ijar. 2024 . 109285 .

[33] J. Haldimann , C. Beierle , G. Kern-Isberner , T. Meyer, Conditionals, infeasible worlds, and reasoning with system W, The International FLAIRS Conference Proceedings 36 ( 2023 ). doi: 10 .32473/flairs.36. 133268.

[34] J. P. Haldimann , T. Meyer, G. Kern-Isberner , C. Beierle , Rational closure extension in spo representable inductive inference operators , in: S. Gaggl, M. V. Martinez , M. Ortiz (Eds.), Logics in Artificial Intelligence 18th European Conference, JELIA 2023 , Dresden, Germany, September 20-22 , 2023 , Proceedings, volume 12678 of LNCS , Springer, 2023 , pp. 561 - 576 . doi: 10 .1007/978-3- 031 -43619-2_ 38 .

[35] C. Beierle , J. Haldimann , L. Schwarzer, CLKR - Conditional Logic and Knowledge Representation , KI - Künstliche Intelligenz ( 2024 ). URL: https://doi.org/10. 1007/s13218-024-00842-z.

[36] M. Thimm , Tweety: A comprehensive collection of java libraries for logical aspects of artificial intelligence and knowledge representation , in: C. Baral, G. D. Giacomo , T. Eiter (Eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014 , Vienna, Austria, July 20-24 , 2014 , AAAI Press, 2014 , pp. 528 - 537 . URL: http://www.aaai.org/ocs/index.php/KR/ KR14/paper/view/7811.

[37] C. Beierle , C. Eichhorn , S. Kutsch , A practical comparison of qualitative inferences with preferred ranking models , KI - Künstliche Intelligenz 31 ( 2017 ) 41 - 52 . 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 .