1 Introduction

Defeasible Conditionals “If A then usually B” and conditional knowledge bases consisting of finite sets of such conditionals play a major role in nonmonotonic reasoning, as they are used to formalize the background knowledge of intelligent agents. A short, compact and straightforward normal form of these knowledge bases is desirable, not only to allow us to compare the knowledge of different agents, but also to store this knowledge in a form that is easily understandable and to compare different approaches of nonmonotonic reasoning. Additionally, the number of conditionals in a knowledge base is an important factor in the computational complexity of approaches that generate an epistemic state inductively on top of conditional knowledge bases. Thus, knowledge bases which contain no unnecessary conditionals may lead to significantly reduced computational efforts required when dealing with knowledge bases in these approaches.

This article extends the work presented in the short paper [2] in several directions and is organized as follows: After briefly recalling the required background in Sect. 2, we propose to use the notion of elementwise equivalence or model equivalence for conditional knowledge bases (Sect. 3) to enable the replacement of a knowledge base \(\mathcal R\) by a simpler, but equivalent knowledge base \(\mathcal R'\). In Sect. 4 we present a set of naturally arising transformation rules on conditional knowledge bases, develop a terminating and confluent transformation system for elementwise equivalence, yielding a unique normal form for every conditional knowledge base, and prove that two knowledge bases are elementwise equivalent iff they have the same conditional normal form. In Sect. 5, we show that an extended version of this transformation system takes model equivalence into account. We prove that both transformation systems yield normal forms that are minimal with respect to the corresponding notion of equivalence and subset inclusion. Section 6 concludes the paper and points out future work.

2 Background: Conditionals and OCFs

Let \(\varSigma =\{V_1,...,V_m\}\) be a propositional alphabet. A literal is the positive (\(v_i\)) or negated (\(\overline{v}_i\)) form of a propositional variable \(V_i\). From these we obtain the propositional language \(\mathfrak {L}\) as the set of formulas of \(\varSigma \) closed under negation \(\lnot \), conjunction \(\wedge \), and disjunction \(\vee \), as usual; for formulas A, \(B\in \mathfrak {L}\), \(A\Rightarrow B\) denotes the material implication and stands for \(\lnot A\vee B\). For shorter formulas, we abbreviate conjunction by juxtaposition (i.e., AB stands for \(A\wedge B\)), and negation by overlining (i.e., \(\overline{A}\) is equivalent to \(\lnot A\)). Let \(\varOmega \) denote the set of possible worlds over \(\mathfrak {L}\); \(\varOmega \) will be taken here simply as the set of all propositional interpretations over \(\mathfrak {L}\) and can be identified with the set of all complete conjunctions over \(\varSigma \). For \(\omega \in \varOmega \), \(\omega \,\models \,A\) means that the propositional formula \(A \in \mathfrak {L}\) holds in the possible world \(\omega \).

A conditional (B|A) with \(A,B\in \mathfrak {L}\) encodes the defeasible rule “if A then usually B” and is a trivalent logical entity with the evaluation [4, 6]:

$$\begin{aligned}{}[\![(B|A)]\!]_\omega&=\left\{ \begin{array}{l@{\quad }l@{\quad }l} true &{}\text {iff}\quad \omega \,\models \,AB&{}\text {(verification)}\\ false &{}\text {iff}\quad \omega \,\models \,A\overline{B}&{}\text {(falsification)}\\ undefined &{}\text {iff}\quad \omega \,\models \,\overline{A}&{}\text {(not applicable)} \end{array}\right. \end{aligned}$$

A knowledge base \(\mathcal R=\{(B_1|A_1),...,(B_n|A_n)\}\) is a finite set of such conditionals.

An Ordinal Conditional Function (OCF, ranking function) [9] is a function \(\kappa :\varOmega \rightarrow \mathbb {N}_0\cup \{\infty \}\) that assigns to each world \(\omega \in \varOmega \) an implausibility rank \(\kappa (\omega )\), that is, the higher \(\kappa (\omega )\), the more surprising \(\omega \) is. OCFs have to satisfy the normalization condition that there has to be a world that is maximally plausible, i.e., the preimage of 0 cannot be empty, formally \(\kappa ^{-1}(0)\ne \emptyset \). The rank of a formula A is defined by \(\kappa (A)=\min \{\kappa (\omega ) \mid \omega \,\models \,A\}\).

An OCF \(\kappa \) accepts a conditional \((B|A)\) (denoted by \(\kappa \models (B|A)\)) iff the verification of the conditional is less surprising than its falsification, i.e., iff \(\kappa (AB) < \kappa (A\overline{B})\). This can also be understood as a nonmonotonic inference relation between the premise A and the conclusion B: We say that A \(\kappa \) -entails B (written ) if and only if \(\kappa \) accepts the conditional \((B|A)\), formally

(1)

The acceptance relation in (1) is extended as usual to a set \(\mathcal R\) of conditionals by defining \(\kappa \models \mathcal R\) iff \(\kappa \models (B|A)\) for all \((B|A) \in \mathcal R\). This is synonymous to saying that \(\mathcal R\) is admissible with respect to \(\mathcal R\) [5]. A knowledge base \(\mathcal R\) is consistent iff there exists an OCF \(\kappa \) such that \(\kappa \models \mathcal R\).

Example 1

\(( {\mathcal R_{ car }} ). \) Let \(\varSigma =\{C,E,F\}\) be an alphabet where C indicates whether something is a car (c), or not (\(\overline{c})\), E indicates whether something is an e-car (e), or not (\(\overline{e})\), and F indicates whether something needs fossil fuel (f), or not (\(\overline{f})\).

Let \({\mathcal R_{ car }} = \{r_1, r_2, r_3, r_4, r_5, r_6, r_7\}\) be a knowledge base using \(\varSigma \) with:

  • \(\varvec{r_{1}:}\) \((f|c)\)Usually cars need fossil fuel.

  • \(\varvec{r_{2}:}\) \((\overline{f}|e)\)Usually e-cars do not need fossil fuel.

  • \(\varvec{r_{3}:}\) \((c|e)\)E-cars usually are cars.

  • \(\varvec{r_{4}:}\) \((e| e\overline{f} )\)E-cars that do not need fossil fuel usually are e-cars.

  • \(\varvec{r_{5}:}\) \((e\overline{f}|e)\)E-cars usually are e-cars that do not need fossil fuel.

  • \(\varvec{r_{6}:}\) \((\overline{e}|\top )\)Usually things are no e-cars.

  • \(\varvec{r_{8}:}\) \(( cf \vee \overline{c}f | ce \vee c\overline{e} )\)Things that are cars and e-cars or cars but not e-cars are cars that need fossil fuel or are no cars but need fossil fuel.

This knowledge base is consistent: For instance, a ranking model \(\kappa \) for \({\mathcal R_{ car }} \) is

figure a

with, e.g., \(\kappa \,\models \,(\overline{f}|e)\) because \(\kappa (e\overline{f})=1<2=\kappa (ef)\) and \(\kappa \,\models \,(\overline{e}|\top )\) because \(\kappa (\overline{e})=0<1=\kappa (\overline{e})\).

3 Model Based Equivalences

With the acceptance relation between ranking functions and knowledge bases, we now can define the set of ranking models of a knowledge base.

Definition 1 (ranking models)

Let \(\mathcal R=\{(B_1|A_1),\ldots ,(B_n|A_n)\}\) be a finite conditional knowledge base. The set of ranking models of \(\mathcal R\) is the set of OCFs that are admissible with respect to \(\mathcal R\), formally \({ Mod}\,(\mathcal R)=\{\kappa |\kappa \,\models \,\mathcal R\}\).

The notion of inconsistency gives us a possibility to determine whether every ranking model of a knowledge base accepts a given conditional:

Proposition 1

([5]). Let \(\mathcal R=\{(B_1|A_1),\ldots ,(B_n|A_n)\}\) be a finite conditional knowledge base. A conditional \((B|A)\) with \(AB \not \equiv \bot \) is accepted by every ranking model \(\kappa \in { Mod}\,(\mathcal R)\) if and only if \(\mathcal R\cup \{(\overline{B}|A)\}\) is inconsistent.

Definition 2 (model equivalence)

Let \(\mathcal R\), \(\mathcal R'\) be knowledge bases. \(\mathcal R\) and \(\mathcal R'\) are model equivalent, denoted \( \mathcal R\equiv _{mod}\mathcal R'\), iff \( Mod (\mathcal R) = Mod (\mathcal R') \).

By definition, the model set of an inconsistent knowledge base is empty, so all inconsistent knowledge bases are equivalent. We introduce the special knowledge base \(\diamond \) that is inconsistent by definition; thus \(\diamond \equiv _{mod}\mathcal R\) for every \(\mathcal R\) with \({ Mod}\,(\mathcal R)=\emptyset \); for instance, \(\{(\bot |\top )\} \equiv _{mod}\diamond \). The idea of elementwise equivalence is that each piece of knowledge (i.e. conditional) in one knowledge base directly corresponds to a piece of knowledge in the other knowledge base.

Definition 3 (elementwise equivalence)

Let \(\mathcal R\), \(\mathcal R'\) be knowledge bases.

  • \(\mathcal R\) is an elementwise equivalent sub-knowledge base of \(\mathcal R'\), denoted by \( \mathcal R\ll _{ee}\mathcal R'\), iff for every conditional \((B'|A') \in \mathcal R'\) that is not self-fulfilling (i.e. \(A' \not \models B'\)) there is a conditional \((B|A) \in \mathcal R\) such that \( Mod (\{(B|A)\}) = Mod (\{(B'|A')\}) \).

  • \(\mathcal R\) and \(\mathcal R'\) are strictly elementwise equivalent iff \( \mathcal R\ll _{ee}\mathcal R'\) and \( \mathcal R'\ll _{ee}\mathcal R\).

  • \(\mathcal R\) and \(\mathcal R'\) are elementwise equivalent, denoted by \( \mathcal R\equiv _{ee}\mathcal R'\), iff either both \(\mathcal R\) and \(\mathcal R'\) are inconsistent, or both \(\mathcal R\) and \(\mathcal R'\) are consistent and strictly elementwise equivalent.

Thus, two inconsistent knowledge bases are also elementwise equivalent according to Definition 3, e.g. \(\{(B|A),(\overline{B}|A)\} \equiv _{ee}\{\{(B'|A'),(\bot |\top )\} \), enabling us to avoid cumbersome case distinctions when dealing with sets of consistent and inconsistent knowledge bases. We illustrate model equivalence and elementwise equivalence with the following excerpts of Example 1:

Example 2

Let \(\mathcal R'_{ car } =\{r_1,r_2,r_3,r_7\}\) and \(\mathcal R''_{ car } =\{r_1,r_2,r_3\}\) be knowledge bases with conditionals from Example 1. Since \(f\equiv ef\vee \overline{c}f\) and \(c\equiv ce\vee c\overline{e}\), for every OCF \(\kappa \) we have \(\kappa (cf)=\kappa \left( \left( ce\vee c\overline{e}\right) \wedge \left( ef\vee \overline{c}f\right) \right) \) and likewise \(\kappa (c\overline{f})=\kappa \left( \left( ce\vee c\overline{e}\right) \wedge \lnot \left( ef\vee \overline{c}f\right) \right) \) and hence \(\kappa \,\models \,r_3\) if and only if \(\kappa \,\models \,r_7\). Therefore, for every \(\kappa \,\models \,\mathcal R''_{ car } \) we also have \(\kappa \,\models \,\mathcal R'_{ car } \), and vice versa, which gives us \(\mathcal R'_{ car } \equiv _{mod}\mathcal R''_{ car } \). For the same reason we have \({ Mod}\,(\{r_3\})={ Mod}\,(\{r_7\})\) (and, trivially, \({ Mod}\,(\{r_i\})={ Mod}\,(\{r_i\})\) for all \(i\in \{1,2,3,7\}\)), which gives us \(\mathcal R'_{ car } \ll _{ee}\mathcal R''_{ car } \) and \(\mathcal R''_{ car } \ll _{ee}\mathcal R'_{ car } \) and hence \(\mathcal R'_{ car } \equiv _{ee}\mathcal R''_{ car } \). So \(\mathcal R'_{ car } \) and \(\mathcal R''_{ car } \) are both model equivalent and also elementwise equivalent.

4 Normal Forms for Elementwise Equivalence

Similar to formulas in propositional logic, it is often advantageous to consider only conditional knowledge bases that are in a standardized normal form. In the following, we will develop rules for transforming a knowledge base toward a normal form. For this, we will use a function \(\varPi \) that assigns to a knowledge base \(\mathcal R\) an ordered partition \(\varPi (\mathcal R)=(\mathcal R_0,\ldots ,\mathcal R_m)\) such that all conditionals in \(\mathcal R_i\), \(1\leqslant i\leqslant m\), are tolerated by the set \(\bigcup _{j=i}^m\mathcal R_j\) [8]; if no such partition exists, we extend \(\varPi \) by defining \(\varPi (\mathcal R)={\diamond }\). Thus, \(\mathcal R\) is consistent iff \(\varPi (\mathcal R)\ne {\diamond }\) [8].

For propositional formulas over a propositional alphabet \(\varSigma \), there are various ways of defining a normal form such that precisely semantically equivalent formulas are mapped to the same normal form, using e.g. disjunctions of worlds or selected shortest formulas. In order to abstract from a particular choice, for the rest of this paper we assume a function \(\nu \) that maps a propositional formula \(A\) to a unique normal form \(\nu (A)\) such that \( A \equiv A' \) iff \( \nu (A) = \nu (A') \).

Using \(\varPi \) and \(\nu \), the transformation system \(\mathcal {T}\) is given in Fig. 1:

Fig. 1.
figure 1

Transformation rules \(\mathcal {T}\) for conditional knowledge bases

 

(\( SF \)):

removes a conditional \((B|A)\) if \(A\,\models \,B\) since such a conditional is self-fulfilling because it can not be falsified by any world.

(\( DP \)):

removes a conditional \((B'|A')\) which is a duplicate of a conditional \((B|A)\) under propositional equivalences of \(A\) and \(A'\) and of \(B\) and \(B'\).

(\( CE \)):

removes a conditional that is conditionally equivalent to another one.

(\( PN \)):

propositionally normalizes antecedent and consequent of a conditional.

(\( CN \)):

transforms a conditional \((B|A)\) to its conditional normal form by sharpening its consequent to the conjunction with its antecedent.

(\( CC \)):

transforms a knowledge base containing both a conditional \((B|A)\) and its counter conditional \((\overline{B}|A)\) into the inconsistent knowledge base \(\diamond \).

(\( SC \)):

transforms a knowledge base containing a conditional that can not be verified by any world into the inconsistent knowledge base \(\diamond \).

(\( IC \)):

transforms an inconsistent knowledge base into \(\diamond \).

 

We illustrate \(\mathcal {T}\) transforming the knowledge base in the running example to a reduced, more compact form.

Example 3

\(( \mathcal {T} ({\mathcal R_{ car }})). \) Consider the knowledge base \({\mathcal R_{ car }} \) from Example 1.  

(\( SF \)):

In \({\mathcal R_{ car }} \), \(r_4\) is self-fulfilling since \(ef\,\models \,e\), hence the application of (\( SF \)) yields \({\mathcal R_{ car }^{( SF )}} ={\mathcal R_{ car }} \setminus \{r_4\}\).

(\( DP \)):

The conditionals \(r_1\) and \(r_7\) are duplicates since \(c\equiv ce \vee c\overline{e} \) and \(f\equiv ( cf \vee \overline{c}f )\). So applying (\( DP \)) to \({\mathcal R_{ car }} \) gives us \({\mathcal R_{ car }^{( DP )}} ={\mathcal R_{ car }} \setminus \{r_7\}\).

(\( CE \)):

We have \( e\overline{f} \equiv ee\overline{f} \) and \( ef \equiv e\wedge (\overline{e}\vee f) \), therefore \(r_2\) and \(r_5\) are conditionally equivalent; applying (\( CE \)) to \({\mathcal R_{ car }} \) yields \({\mathcal R_{ car }^{( CE )}} ={\mathcal R_{ car }} \setminus \{r_5\}\).

(\( PN \)):

The conditional \(r_1\) is equivalent to \(r_7\) but shorter, so let us assume the shorter formula as propositional normal form. With \(\nu \) being a function that converts a propositional formula to this normal form, applying (\( PN \)) to \({\mathcal R_{ car }} \) gives us the same results as (\( DP \)), that is, \({\mathcal R_{ car }^{( PN )}} ={\mathcal R_{ car }} \setminus \{r_7\}\).

(\( SC \)):

The knowledge base \({\mathcal R_{ car }} \) contains no self-contradictory conditional; hence, (\( SC \)) can not be applied to \({\mathcal R_{ car }} \).

 

Applying \(\mathcal {T} \) exhaustively and in arbitrary sequence to \({\mathcal R_{ car }} \) gives us the knowledge base \({\mathcal R_{ car }^{\mathcal {T}}} = \mathcal {T} ({\mathcal R_{ car }}) = \{r_1,r_2,r_3,r_6\}\).

Note that \(\mathcal {T}\) is not a minimal set of transformation rules. For instance, (\( DP \)) is redundant since the effect of removing a conditional \((B'|A')\) as a duplicate of \((B|A)\) could also be achieved by applying (\( PN \)) to both conditionals, thereby mapping them both to the same normalized conditional in the resulting knowledge base. Similarly, (\( CC \)) and (\( SC \)) are redundant since these cases are also covered by the more general transformation rule (\( IC \)). However, our objective here is not to present a minimal set of rules, but a set of more or less naturally arising transformation rules.

Proposition 2

\(\mathcal {T}\) is terminating.

Proof

The rules (\( SF \)), (\( DP \)), (\( CE \)), and (\( IC \)) all remove at least one conditional, (\( PN \)) and (\( CN \)) can be applied at most once to any conditional, and also (\( CC \)), (\( SC \)), and (\( IC \)) all remove at least one conditional. Hence, \(\mathcal {T}\) is terminating.    \(\square \)

Proposition 3

( \(\mathcal {T} \) correct). Let \(\mathcal {T} (\mathcal R)\) be the knowledge base obtained from \(\mathcal R\) by exhaustively applying \(\mathcal {T}\) to \(\mathcal R\). Then \( \mathcal R\equiv _{mod}\mathcal {T} (\mathcal R) \).

Proof

We prove the proposition by showing that each single rule is correct.

  • (\( SF \)) is correct since \((B|A)\) with \(A\,\models \,B\) is verified by every OCF.

  • (\( DP \)) is correct since \(A \equiv A', \, B \equiv B'\) implies that \(\kappa \,\models \,(B|A)\) iff \(\kappa \,\models \,(B'|A')\) for every OCF \(\kappa \).

  • (\( CE \)) is correct since \(AB \equiv A'B', \, A\overline{B} \equiv A\overline{B'}\) implies that \(\kappa \,\models \,(B|A)\) iff \(\kappa \,\models \,(B'|A')\) for every OCF \(\kappa \).

  • (\( PN \)) is correct since for every OCF \(\kappa \), we have \(\kappa \,\models \,(B|A)\) iff \(\kappa \,\models \,(\nu (B)|\nu (A))\).

  • (\( CN \) is correct since for every OCF \(\kappa \), we have \(\kappa \,\models \,(B|A)\) iff \(\kappa \,\models \,(AB|A)\).

  • (\( CC \)) is correct since there is no OCF \(\kappa \) accepting both a conditional \((B|A)\) and its counter conditional \((\overline{B}|A)\).

  • (\( SC \)) is correct since there is no OCF \(\kappa \) with \(\kappa \,\models \,(B|A)\) if \(AB \equiv \bot \).

  • (\( IC \)) is correct since \(\varPi \) is a consistency test for any knowledge base \(\mathcal R\).    \(\square \)

While Proposition 3 states that \(\mathcal {T}\) is correct with respect to model equivalence of knowledge bases, the following proposition shows that this is also the case with respect to the stricter notion of elementwise equivalence.

Proposition 4

( \(\mathcal {T} \) correct w.r.t. elementwise equivalence). Let \(\mathcal {T} (\mathcal R)\) be the knowledge base obtained from \(\mathcal R\) by exhaustively applying \(\mathcal {T}\) to \(\mathcal R\). Then \( \mathcal R\equiv _{ee}\mathcal {T} (\mathcal R) \).

Proof

According to the proof of Proposition 3, \(\mathcal R\) is inconsistent iff \(\mathcal {T} (\mathcal R) = \diamond \); thus, if \(\mathcal R\) is inconsistent then \(\mathcal R\equiv _{ee}\mathcal {T} (\mathcal R)\). So let \(\mathcal R\) be consistent. Then \(\mathcal {T} (\mathcal R)\) has been obtained from \(\mathcal R\) by a finite number of applications of (\( SF \)), (\( DP \)), (\( CE \)), (\( PN \)), and (\( CN \)). For these applications we observe:

  • (\( SF \)) preserves elementwise equivalence since for self-fulfilling conditionals no counterpart in the other knowledge base is required.

  • (\( DP \)) and (\( CE \)) preserve elementwise equivalence since in both cases, we obviously have \( Mod (\{(B|A)\}) = Mod (\{(B'|A')\}) \) and thus \(\{(B|A),\, (B'|A')\} \equiv _{ee}\{(B|A)\}\).

  • (\( DP \)) and (\( CN \)) preserve elementwise equivalence since \( Mod (\{(B|A)\}) = Mod (\{(\nu (B)|\nu (A))\}) \) and since \( Mod (\{(B|A)\}) = Mod (\{(AB|A)\}) \).    \(\square \)

\(\mathcal {T}\) is an extended version of the transformation system \( NF \) presented in [2]. While \( NF \) is not confluent [1, 2, 7], the next proposition proves that \(\mathcal {T}\) is confluent.

Proposition 5

\(\mathcal {T}\) is confluent.

Proof

Since \(\mathcal {T}\) is terminating, local confluence of \(\mathcal {T}\) implies confluence of \(\mathcal {T}\); local confluence of \(\mathcal {T}\) in turn can be shown by ensuring that for every critical pair obtained form superpositioning two left hand sides of rules in \(\mathcal {T}\) reduces to the same knowledge base [1, 7]:

Any critical pair obtained from (\( CC \)), (\( SC \)), or (\( IC \)) and a rule in \(\mathcal {T}\) reduces to \(\diamond \) since all rules preserve the consistency status af a knowledge base.

Any critical pair obtained from (\( SF \)) with \(\mathcal {T} \setminus \{( CC ), ( SC ),( IC )\}\) reduces to the same knowledge base since a self-fulfilling conditional replaced by a transformation rule in \(\{( DP ), ( CE ), ( PN ), ( CN )\}\) is still self-fulfilling. Furthermore, any critical pair involving (\( PN \)) can obviously be reduced to the same knowledge base; this observation also holds for (\( CN \)).

Thus, we are left with critical pairs obtained from (\( DP \)) and (\( CE \)). Consider

$$\begin{aligned} \mathcal R_0 = \mathcal R\cup \{(B|A), (B'|A'), (B''|A'')\}. \end{aligned}$$

If (\( DP \)) can be applied to \(\mathcal R_0\) at \( \{(B|A), (B'|A')\} \) we get \( \mathcal R_1 = \mathcal R\cup \{(B|A), (B''|A'')\} \), and if (\( CE \)) can be applied to \(\mathcal R_0\) at \( \{(B'|A'), (B''|A'')\} \) we get \( \mathcal R_2 = \mathcal R\cup \{(B|A), (B'|A')\} \). The used applicability of (\( DP \)) to \(\mathcal R_0\) ensures \(A \equiv A', B \equiv B'\); hence (\( DP \)) can be applied to \(\mathcal R_2\), yielding \( \mathcal R_3 = \mathcal R\cup \{(B|A)\} \). The used applicability of (\( CE \)) to \(\mathcal R_0\) ensures \(A'B' \equiv A''B'', A'\overline{B'} \equiv A''\overline{B''}\); thus, we also have \(AB \equiv A''B'', A\overline{B} \equiv A''\overline{B''}\) so that (\( CE \)) can be applied to \(\mathcal R_1\), yielding \( \mathcal R\cup \{(B|A)\} = \mathcal R_3 \). Hence, \(\mathcal {T}\) reduces both \(\mathcal R_1\) and \(\mathcal R_2\) to \(\mathcal R_3\). Similarly, the other critical pairs obtained from (\( DP \)) and (\( CE \)) can be shown to be reducible to the same knowledge base.    \(\square \)

\(\mathcal {T}\) is not only confluent, but it also yields a knowledge base that is minimal when taking elementwise equivalence into account.

Proposition 6

( \(\mathcal {T} \) minimizing w.r.t. elementwise equivalence). For all knowledge bases \(\mathcal R\) we have \( \mathcal {T} (\mathcal R) = \diamond \) iff \(\mathcal R\) is inconsistent, and if \(\mathcal R\) is consistent, then for all knowledge bases \(\mathcal R'\) it holds that:

$$\begin{aligned} \mathcal R'\subsetneqq \mathcal {T} (\mathcal R)&\text {\,\,\,\,\,implies\,\,\,\,\,} \mathcal R'\not \equiv _{ee}\mathcal R\end{aligned}$$
(2)

Proof

For inconsistent \(\mathcal R\), the proof follows from Proposition 4, so let \(\mathcal R\) be consistent and \(\mathcal R'\subsetneqq \mathcal {T} (\mathcal R)\). Proposition 4 implies \(\mathcal R\equiv _{ee}\mathcal {T} (\mathcal R)\); hence, it suffices to show \(\mathcal R' \not \equiv _{ee}\mathcal {T} (\mathcal R)\). If we assume the contrary, \(\mathcal R' \equiv _{ee}\mathcal {T} (\mathcal R)\), then \( \mathcal R'\subsetneqq \mathcal {T} (\mathcal R)\) implies that there must be two different conditionals \((B_1|A_1), (B_2|A_2) \in \mathcal {T} (\mathcal R)\) and a conditional \((B|A) \in \mathcal R'\) such that \( Mod (\{(B_1|A_1)\}) = Mod (\{(B|A)\}) \) and \( Mod (\{(B_1|A_1)\}) = Mod (\{(B|A)\}) \) and hence \( Mod (\{(B_1|A_1)\}) = Mod (\{(B_2|A_2)\}) \). This requires \(A_1\equiv A_2\), \(A_1B_1 \equiv A_2B_2\), and \(A_1\overline{B_1} \equiv A_2\overline{B_2}\), implying that (\( CE \)) could be applied to \((B_1|A_1), (B_2|A_2)\), a contradiction to our assumptions. Thus, \(\mathcal R'\not \equiv _{ee}\mathcal R\).    \(\square \)

Propositions 26 ensure that applying \(\mathcal {T}\) to a knowledge base \(\mathcal R\) always yields the unique normal form \(\mathcal {T} (\mathcal R)\) that is elementwise equivalent to \(\mathcal R\) and minimal with respect to set inclusion.

Definition 4 (conditional normal form)

A knowledge base \(\mathcal R\) is in conditional normal form iff \(\mathcal R= \mathcal {T} (\mathcal R)\).

Thus, for every knowledge base \(\mathcal R\), its conditional normal form is uniquely determined. Moreover, \(\mathcal {T}\) provides a convenient test for the elementwise equivalence of knowledge bases.

Proposition 7 (elementwise equivalence)

Two knowledge bases \(\mathcal R, \mathcal R'\) are elementwise equivalent iff the have the same conditional normal form, i.e.:

$$\begin{aligned} \mathcal R\equiv _{ee}\mathcal R'\text {\,\,\,\,\,iff\,\,\,\,\,} \mathcal {T} (\mathcal R) = \mathcal {T} (\mathcal R') \end{aligned}$$
(3)

5 Normal Forms for Model Equivalence

While \(\mathcal {T}\) is correct with respect to both model equivalence and elementwise equivalence, it is minimizing for elementwise equivalence (Proposition 4), but it is not minimizing when taking model equivalence into account.

Example 4

\(( \mathcal {T} ~not~minimizing~for~model~equivalence). \) We illustrate that \(\mathcal {T} \) is not minimizing with respect to model equivalence using the running example with the knowledge bases \({\mathcal R_{ car }} \) and \({\mathcal R_{ car }^{\mathcal {T}}} \). We already illustrated that \({\mathcal R_{ car }^{\mathcal {T}}} \) can be obtained from \({\mathcal R_{ car }} \) by exhaustive application of the rules of \(\mathcal {T} \) in Example 3, i.e. \(\mathcal {T} ({\mathcal R_{ car }}) = {\mathcal R_{ car }^{\mathcal {T}}} \). But \({\mathcal R_{ car }^{\mathcal {T}}} \) is not minimal with respect to set inclusion when taking model equivalence into account: Consider the knowledge base \( \mathcal R'_{ car } \) \( =\{r_1,r_2,r_3\}\subsetneqq {\mathcal R_{ car }^{\mathcal {T}}} = \{r_1,r_2,r_3,r_6\} \). We have \(\mathcal R'_{ car } \cup \{(e|\top )\} \equiv _{mod}\diamond \) and thus Proposition 1 gives us \(\kappa \,\models \,(\overline{e}|\top )\) for all \(\kappa \,\models \,\mathcal R'_{ car } \). Therefore, since \(r_6 = (\overline{e}|\top )\), every ranking model of \(\mathcal R'_{ car } \) is also a ranking model of \({\mathcal R_{ car }^{\mathcal {T}}} \), thus \(\mathcal R'_{ car } \equiv _{mod}{\mathcal R_{ car }^{\mathcal {T}}} \).

This example motivates the following extension of \(\mathcal {T}\):

Definition 5

( \(\mathcal {T}_2 \) ). \(\mathcal {T}_2\) is the transformation system \(\mathcal {T}\) extended by the rule:

Since (\( RC \)) removes a conditional \((B|A)\) from a knowledge base \(\mathcal R\cup \{(B|A)\}\) if every model of \(\mathcal R\) accepts \((B|A)\), we immediately have \(\mathcal R\cup \{(B|A)\} \equiv _{mod}\mathcal R\). Together with the properties for \(\mathcal {T}\) shown above, we get:

Proposition 8

( \(\mathcal {T}_2 \) terminating and correct w.r.t. model equivalence). \(\mathcal {T}_2\) is terminating, and for all knowledge bases \(\mathcal R\), we have \( \mathcal R\equiv _{mod}\mathcal {T}_2 (\mathcal R) \).

In contrast to \(\mathcal {T} \), \(\mathcal {T}_2 \) is not confluent as the choice of where the transformation rule (\( RC \)) is applied may influence the result as illustrated by the following example.

Example 5

\({ (}\mathcal {T}_2 ~{ not~confluent).}\) Consider the knowledge base \( \mathcal R= \{r_1, r_2, r_3, r_4\} \) with \(r_1 = (f|c)\), \(r_2 = (c|e)\), \(r_3 = (\overline{f}|e)\), and \(r_4 = (\overline{f}|ce)\). Let \(\overline{r_3} = (f|e)\) and \(\overline{r_4} = (f|ce)\). Then \(\varPi (\{r_1, r_2, r_3\} \cup \{\overline{r_4}\}) = {\diamond }\), and hence applying (\( RC \)) to \(\mathcal R\) at \(r_4\) yields \(\mathcal R_1 = \{r_1, r_2, r_3\}\). Furthermore, \(\varPi (\{r_1, r_2, r_4\} \cup \{\overline{r_3}\}) = {\diamond }\), and hence applying (\( RC \)) to \(\mathcal R\) at \(r_3\) yields \(\mathcal R_2 = \{r_1, r_2, r_4\}\). Applying \(\mathcal {T}_2\) yields

$$\begin{aligned} R'_1&= \mathcal {T}_2 (R_1) = \{(\nu (cf)|\nu (c)), (\nu (ce)|\nu (e)), (\nu (e\overline{f})|\nu (e))\} \end{aligned}$$
(4)
$$\begin{aligned} R'_2&= \mathcal {T}_2 (R_2) = \{(\nu (cf)|\nu (c)), (\nu (ce)|\nu (e)), (\nu (ce\overline{f})|\nu (ce))\} \end{aligned}$$
(5)

and since \(\mathcal R'_1 \not = \mathcal R'_2\), these two knowledge bases are two different normal forms for \(\mathcal R\) under \(\mathcal {T}_2\).

On the other hand, \(\mathcal {T}_2\) is minimizing when taking model equivalence into account.

Proposition 9

( \(\mathcal {T}_2 \) minimizing w.r.t. model equivalence). For all knowledge bases \(\mathcal R\) we have \( \mathcal {T}_2 (\mathcal R) = \diamond \) iff \(\mathcal R\) is inconsistent, and if \(\mathcal R\) is consistent, then for all knowledge bases \(\mathcal R'\) it holds that:

$$\begin{aligned} \mathcal R'\subsetneqq \mathcal {T}_2 (\mathcal R)&\text {\,\,\,\,\,implies\,\,\,\,\,} \mathcal R'\not \equiv _{mod}\mathcal R\end{aligned}$$
(6)

Proof

As in Proposition 6, we are left to prove the case for a consistent \(\mathcal R\). So let \(\mathcal R\) be consistent and \(\mathcal R'\subsetneqq \mathcal {T}_2 (\mathcal R)\). Proposition 8 implies \(\mathcal R\equiv _{mod}\mathcal {T}_2 (\mathcal R)\); hence, it suffices to show \(\mathcal R' \not \equiv _{mod}\mathcal {T}_2 (\mathcal R)\). If we assume the contrary, \(\mathcal R' \equiv _{mod}\mathcal {T}_2 (\mathcal R)\), then \( \mathcal R'\subsetneqq \mathcal {T}_2 (\mathcal R)\) implies that there must be conditionals \((B_1|A_1), \ldots , (B_n|A_n) \in \mathcal {T}_2 (\mathcal R)\), \(n \geqslant 1\), such that \( \mathcal R' \cup \{(B_1|A_1), \ldots , (B_n|A_n)\} = \mathcal {T}_2 (\mathcal R) \) with \( Mod (\{\mathcal R' \cup \{(B_1|A_1), \ldots , (B_n|A_n)\}) = Mod (\{\mathcal {T}_2 (\mathcal R)\}) \). This implies that (\( RC \)) could be applied to \(\mathcal {T}_2 (\mathcal R)\) at \((B_1|A_1)\), contradicting our assumptions. Thus, \(\mathcal R'\not \equiv _{mod}\mathcal R\).    \(\square \)

6 Conclusions and Future Work

In this paper we proposed notions of elementwise and model equivalence for conditional knowledge bases, enabling the replacement of a knowledge base \(\mathcal R\) by an equivalent knowledge base \(\mathcal R'\). Based on these notions, we presented the terminating and confluent transformation system \(\mathcal {T}\) that for every knowledge base yields a minimal and unique conditional normal form with respect to elementwise equivalence, providing a straightforward test for elementwise equivalence of knowledge bases. We extended this system to the transformation system \(\mathcal {T}_2\) that takes model equivalence into account. Both systems yield set-inclusion minimal knowledge bases with respect to the corresponding notion of equivalence. Note that we used OCFs as an exemplary model for knowledge bases. Both \(\mathcal {T}\) and \(\mathcal {T}_2\) should also apply to probabilistic or possibilistic [3] settings, it remains to show that the resulting knowledge bases respect the given semantics.

In our ongoing work, we are studying the practical consequences that result from using normalized knowledge bases instead of their non-normalized versions. Both transformation systems \(\mathcal {T}\) and \(\mathcal {T}_2\) are model preserving, so the normal forms obtained by these system can be used for all inference relations that take all or a single model into account. We are currently investigating to which extent this also applies to inference relations that are defined upon a set of preferred models.