On the Antecedent Normal Form of Conditional Knowledge Bases

Abstract

Desirable properties of a normal form for conditional knowledge are, for instance, simplicity, minimality, uniqueness, and the respecting of adequate equivalences. In this paper, we propose the notion of antecedentwise equivalence of knowledge bases. It identifies more knowledge bases as being equivalent and allows for a simpler and more compact normal form than previous proposals. We develop a set of transformation rules mapping every knowledge base into an equivalent knowledge base that is in antecedent normal form (ANF). Furthermore, we present an algorithm for systematically generating conditional knowledge bases in ANF over a given signature. The approach is complete in the sense that, taking renamings and equivalences into account, every consistent knowledge base is generated. Moreover, it is also minimal in the sense that no two knowledge bases are generated that are antecedentwise equivalent or that are isomorphic to antecedentwise equivalent knowledge bases.

1 Introduction

A core question in knowledge representation and reasoning is what a knowledge base consisting of a set of conditionals like “If A then usually B”, formally denoted by $(B|A)$, entails [20]. For investigating this question and corresponding properties of a knowledge base, for comparing the inference relations induced by different knowledge bases, for implementing systems realizing reasoning with conditional knowledge bases, and for many related tasks a notion of normal form for knowledge bases is advantageous. Desirable properties of a normal form for conditional knowledge bases are, for instance, simplicity, minimality, uniqueness, and the respecting of adequate equivalences of knowledge bases. Normal forms of conditional knowledge bases have been investigated in e.g. [3, 4]. In this paper, we propose the new notion of antecedentwise equivalence of conditional knowledge bases and the concept of antecedent normal form (ANF) of a knowledge base. Antecedentwise equivalence identifies more knowledge bases as being equivalent and allows for a simpler and more compact normal form than previous proposals. As an effective way of transforming every knowledge base $\mathcal R$ into an equivalent knowledge base being in ANF, we develop a set of transformation rules $\varTheta$ achieving this goal. Furthermore, we present an algorithm $KB_{ gen }^{ae}$ enumerating conditional knowledge bases over a given signature. The algorithm is complete in the sense that every consistent knowledge base is generated when taking renamings and antecedentwise equivalences into account. Moreover, $KB_{ gen }^{ae}$ is also minimal: It will not generate any two different knowledge bases $\mathcal R$, $\mathcal R'$ such that $\mathcal R$ and $\mathcal R'$ or any isomorphic images of $\mathcal R$ and $\mathcal R'$ are antecedentwise equivalent. This algorithm is a major improvement over the approach given in [9] because it generates significantly fewer knowledge bases, while still being complete and minimal. Systematic generation of knowledge bases as achieved by $KB_{ gen }^{ae}$ is fruitful for various purposes, for instance for the empirical comparison and evaluation of different nonmonotonic inference relations induced by a knowledge base (e.g. [5, 17, 20, 22]) with the help of implemented reasoning systems like InfOCF [6].

For illustrating purposes, we will use ranking functions, also called ordinal conditional functions (OCF) [23, 24], as semantics for conditionals. However, it should be noted that all notions and concepts developed in this paper are independent of the semantics of ranking functions we use in this paper. They also apply to every semantics satisfying system P [1, 17], e.g., Lewis’ system of spheres [21], conditional objects evaluated using Boolean intervals [12], possibility distributions [10], or special classes of ranking functions like c-representations [15]. A common feature of these semantics is that a conditional $(B|A)$ is accepted if its verification $A \wedge B$ is considered more plausible, more possible, less surprising, etc. than its falsification $A \wedge \lnot B$.

After recalling required basics in Sect. 2, antecedentwise equivalence and ANF is introduced in Sect. 3. The system $\varTheta$ transforming a knowledge base into ANF is presented in Sect. 4. Orderings and renamings developed in Sect. 5 are exploited in knowledge base generation by $KB_{ gen }^{ae}$ in Sect. 6, before concluding in Sect. 7.

2 Background: Conditional Logic

Let $\mathcal L$ be a propositional language over a finite signature $\varSigma$ of atoms $a,b,c, \ldots$. The formulas of $\mathcal L$ will be denoted by letters $A,B,C, \ldots$. We write AB for $A \wedge B$ and $\overline{A}$ for $\lnot A$. We identify the set of all complete conjunctions over $\varSigma$ with the set $\varOmega$ of possible worlds over $\mathcal L$. For $\omega \in \varOmega$, $\omega \models A$ means that $A \in \mathcal L$ holds in $\omega$, and the set of worlds satisfying A is $\varOmega _A = \{\omega \mid \omega \models A\}$. By introducing a new binary operator |, we obtain the set $(\mathcal L\mid \mathcal L)= \{ (B|A) \mid A,B \in \mathcal L\}$ of conditionals over $\mathcal L$. For a conditional $r = (B|A)$, $ant (r) = A$ is the antecedent of r, and $cons (r) = B$ is its consequent. The counter conditional of $r = (B|A)$ is $\overline{r} = (\overline{B}|A)$. As semantics for conditionals, we use ordinal conditional functions (OCF) [24]. An OCF is a function expressing degrees of plausibility of possible worlds where a lower degree denotes “less surprising”. At least one world must be regarded as being normal; therefore, $\kappa (\omega ) = 0$ for at least one $\omega \in \varOmega$. Each $\kappa$ uniquely extends to a function mapping sentences to given by $\kappa (A) = \min \{\kappa (\omega ) \mid \omega \models A\}$ where $\min \emptyset = \infty$. An OCF $\kappa$ accepts a conditional $(B|A)$, written $\kappa \models (B|A)$, if the verification of the conditional is less surprising than its falsification, i.e., if $\kappa (AB) < \kappa (A\overline{B})$; equivalently, $\kappa \models (B|A)$ iff for every $\omega ' \in \varOmega _{A\overline{B}}$ there is $\omega \in \varOmega _{AB}$ with $\kappa (\omega ) < \kappa (\omega ')$. A conditional $(B|A)$ is trivial if it is self-fulfilling ($A \models B$) or contradictory ($A \models \overline{B}$); a set of conditionals is self-fulfilling if every conditional in it is self-fulfilling. A finite set $\mathcal R\subseteq (\mathcal L|\mathcal L)$ of conditionals is called a knowledge base. An OCF $\kappa$ accepts $\mathcal R$ if $\kappa$ accepts all conditionals in $\mathcal R$, and $\mathcal R$ is consistent if an OCF accepting $\mathcal R$ exists [14]. We use $\diamond$ to denote an inconsistent knowledge base. $Mod (\mathcal R)$ denotes the set of all OCFs $\kappa$ accepting $\mathcal R$. Two knowledge bases $\mathcal R, \mathcal R'$ are model equivalent, denoted by $\mathcal R\equiv _{mod}\mathcal R'$, if $Mod (\mathcal R) = Mod (\mathcal R')$. We say $(B|A) \equiv (B'|A')$ if $A \equiv A'$ and $AB \equiv A'B'$. Example 1 presents a knowledge base we will use for illustration.

Example 1

($\mathcal {R}_{car}$ [4]). Let ${\varSigma _{ car }} =\{c,e,f\}$ where c indicates whether something is a car, e indicates whether something is an e-car, and f indicates whether something needs fossil fuel. The knowledge base ${\mathcal R_{ car }}$ contains seven conditionals:

3 Antecedentwise Equivalence of Knowledge Bases

For comparing or generating knowledge bases, it is useful to abstract from merely syntactic variants. In particular, it is desirable to have minimal versions and normal forms of knowledge bases at hand. The following notion of equivalence presented in [4] employs the idea that each piece of knowledge in one knowledge base directly corresponds to a piece of knowledge in the other knowledge base.

Definition 1

(equivalence $\equiv _{ee}$ [4]). 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'$, if for every conditional $(B|A) \in \mathcal R$ that is not self-fulfilling there is a conditional $(B'|A') \in \mathcal R'$ such that $(B|A) \equiv (B'|A')$.

• $\mathcal R$ and $\mathcal R'$ are strictly elementwise equivalent if $\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'$, if either both are inconsistent, or both are consistent and strictly elementwise equivalent.

Elementwise equivalence is a stricter notion than model equivalence. In [3], as a simple example the knowledge bases $\mathcal R_1 = \{(a|\top ), (b|\top ), (ab|\top )\}$ and $\mathcal R_2 = \{(a|\top ), (b|\top )\}$ are given which are model equivalent, but not elementwise equivalent since for $(ab|\top ) \in \mathcal R_1$ there is no corresponding conditional in $\mathcal R_2$. The idea of the notion of antecedentwise equivalence we will introduce here is to take into account the set of conditionals having the same (or propositionally equivalent) antecedent when comparing to knowledge bases.

Definition 2

($Ant (\mathcal R)$, $\mathcal R_{|A}$, ANF). Let $\mathcal R$ be a knowledge base.

• $Ant (\mathcal R) = \{A \mid (B|A) \in \mathcal R\}$ is the set of antecedents of $\mathcal R$.

• For $A \in Ant (\mathcal R)$, the set $\mathcal R_{|A} = \{(B'|A') \mid (B'|A') \in \mathcal R\text { and } A \equiv A'\}$ is the set of A-conditionals in $\mathcal R$.

• $\mathcal R$ is in antecedent normal form (ANF) if either $\mathcal R$ is inconsistent and $\mathcal R= \diamond$, or $\mathcal R$ is consistent, does not contain any self-fulfilling conditional, contains only conditionals of the form $(AB|A)$, and $\left| {\mathcal R_{|A}}\right| = 1$ for all $A \in Ant (\mathcal R)$.

Definition 3

(${\ll _{ae}}$, equivalence $\equiv _{ae}$). Let $\mathcal R$, $\mathcal R'$ be knowledge bases.

• $\mathcal R$ is an antecedentwise equivalent sub-knowledge base of $\mathcal R'$, denoted by $\mathcal R\ll _{ae}\mathcal R'$, if for every $A \in Ant (\mathcal R)$ such that $\mathcal R_{|A}$ is not self-fulfilling there is an $A' \in Ant (\mathcal R')$ with $\mathcal R_{|A} \equiv _{mod}\mathcal R'_{|A'}$.

• $\mathcal R$ and $\mathcal R'$ are strictly antecedentwise equivalent if $\mathcal R\ll _{ae}\mathcal R'$ and $\mathcal R'\ll _{ae}\mathcal R$.

• $\mathcal R$ and $\mathcal R'$ are antecedentwise equivalent, denoted by $\mathcal R\equiv _{ae}\mathcal R'$, if either both are inconsistent, or both are consistent and strictly antecedentwise equivalent.

Note that any two inconsistent knowledge bases are also antecedentwise equivalent according to Definition 3, e.g., $\{(b|a),(\overline{b}|b)\} \equiv _{ae}\{(b|b),(a\overline{a}|\top )\}$, enabling us to avoid cumbersome case distinctions when dealing with consistent and inconsistent knowledge bases. In general, we have:

Proposition 1

${\varvec{(}}{\equiv _{ ae }}$). Let $\mathcal R, \mathcal R'$ be consistent knowledge bases.

• 1. If $\mathcal R\ll _{ae}\mathcal R'$ then $Mod (\mathcal R') \subseteq Mod (\mathcal R)$.

• 2. If $\mathcal R\equiv _{ae}\mathcal R'$ then $\mathcal R\equiv _{mod}\mathcal R'$.

• 3. If $\mathcal R\ll _{ee}\mathcal R'$ then $\mathcal R\ll _{ae}\mathcal R'$.

• 4. If $\mathcal R\equiv _{ee}\mathcal R'$ then $\mathcal R\equiv _{ae}\mathcal R'$.

• 5. None of the implications (1.)–(4.) holds in general in the reverse direction.

Proof

(1.) If $\mathcal R\ll _{ae}\mathcal R'$, Definition 3 implies that there is a function $f:\, Ant (\mathcal R) \rightarrow Ant (\mathcal R')$ with $\mathcal R_{|A} \equiv _{mod}\mathcal R'_{|f(A)}$ for each $A \in Ant (\mathcal R)$. Thus, $\mathcal R= \bigcup _{A \in Ant (\mathcal R)} \mathcal R_{|A} \equiv _{mod}\bigcup _{A \in Ant (\mathcal R)} \mathcal R'_{|f(A)} \subseteq \mathcal R'$ implies $Mod (\mathcal R') \subseteq Mod (R)$. Employing (1.) in both directions, we get (2.).

(3.) If $\mathcal R\ll _{ee}\mathcal R'$, Definition 1 ensures a function $f:\, \mathcal R \rightarrow \mathcal R'$ with $\{(B|A)\} \equiv _{mod}\{f((B|A))\}$ for each $(B|A) \in \mathcal R$. Hence, $A \equiv A'$ must hold if $(B'|A') = f((B|A))$. Thus, $\{(B|A) \mid (B|A) \in \mathcal R_{|A}\} \equiv _{mod}\{f((B|A)) \mid (B|A) \in \mathcal R_{|A}\}$ for each $A \in Ant (\mathcal R)$. Together with $\mathcal R= \bigcup _{A \in Ant (\mathcal R)} \mathcal R_{|A}$ and $\{f((B|A)) \mid (B|A) \in \mathcal R_{|A}\} \subseteq \mathcal R'$ this implies $\mathcal R\ll _{ae}\mathcal R'$. Employing (3.) in both directions yields (4.).

For proving (5.) w.r.t. both (1.) and (2.), consider $\mathcal R_3 = \{(c|a),(c|b)\}$ and $\mathcal R_4 = \{(c|a),(c|b),(c|a \vee b)\}$. Then $\mathcal R_3 \equiv _{mod}\mathcal R_4$ and $\mathcal R_3 \ll _{ae}\mathcal R_4$, but $\mathcal R_4 \not \ll _{ae}\mathcal R_3$ and therefore $\mathcal R_3 \not \equiv _{ae}\mathcal R_4$. For (5.) w.r.t. both (3.) and (4.), consider again $\mathcal R_1 = \{(a|\top ), (b|\top ), (ab|\top )\}$ and $\mathcal R_2 = \{(a|\top ), (b|\top )\}$. We have $\mathcal R_1 \equiv _{ae}\mathcal R_2$ because ${\mathcal R_{1}}_{|\top } \equiv _{mod}{\mathcal R_{2}}_{|\top }$, but $\mathcal R_1 \not \ll _{ee}\mathcal R_2$ and therefore $\mathcal R_1 \not \equiv _{ee}\mathcal R_2$.    $\square$

In the proof of Proposition 1 $\mathcal R_1 \not \equiv _{ee}\mathcal R_2$ and $\mathcal R_1 \equiv _{ae}\mathcal R_2$ holds, but also $\mathcal R_2 \ll _{ee}\mathcal R_1$. The following example shows that two knowledge bases may be antecedentwise equivalent even if they are not comparable with respect to $\ll _{ee}$.

Example 2

(${\equiv }_{ ae }$). Let $\mathcal R_5 = \{(bc|a),(cd|a)\}$ and $\mathcal R_6 = \{(bd|a),(bcd|a)\}$. Then $\mathcal R_5 \equiv _{ae}\mathcal R_6$, but $\mathcal R_5 \not \equiv _{ee}\mathcal R_6$, $\mathcal R_5 \not \ll _{ee}\mathcal R_6$, and $\mathcal R_6 \not \ll _{ee}\mathcal R_5$.

4 Transforming Knowledge Bases into ANF

In order to be able to deal with normal forms of formulas in $\mathcal L$ without having to select a specific representation, we assume a function $\nu$ mapping a propositional formula $A$ to a unique normal form $\nu (A)$ such that $A \equiv A'$ iff $\nu (A) = \nu (A')$. We also use a function $\varPi$ with $\varPi (\mathcal R) = \diamond$ iff $\mathcal R$ is inconsistent; $\varPi$ can easily be implemented by the tolerance test for conditional knowledge bases [14]. Using $\varPi$ and the propositional normalization function $\nu$, the system $\varTheta$ given in Fig. 1 contains four transformation rules:

Fig. 1.

Transformation rules $\varTheta$ and their applicability conditions for the normalization of knowledge bases respecting antecedence equivalence; $\varPi$ is a consistency test, e.g. the tolerance criterion [14], and $\nu$ a normalization function for propositional formulas.

• $( SF )$ removes a self-fulling conditional $(B|A)$ with $A \not \equiv \bot$.

• $( AE )$ merges two conditionals $(B|A)$ and $(B'|A')$ with propositionally equivalent antecedents to a conditional having this antecedent and the conjunction of the consequents.

• $( NO )$ transforms a conditional $(B|A)$ by sharpening its consequent to the conjunction with its antecedent and propositionally normalizes the antecedent and the resulting consequent.

• $( IC )$ transforms an inconsistent knowledge base into $\diamond$.

Example 3

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

• $( SF )$ As $ef\models e$, $q_4$ is self-fulfilling, and the application of $( SF )$ removes $q_4$.

• $( AE )$ Applying this rule to $q_3$ and $q_5$ yields $q_8: (ce\overline{f}|e)$.

• $( NO )$ Applying this rule to $q_1$ or to $q_7$ yields $\widetilde{q_1}: (\nu (cf)|\nu (c))$ in both cases, applying it to $q_2$ or to $q_5$ yields $\widetilde{q_2}: (\nu (e\overline{f})|\nu (e))$, applying it to $q_3$ yields $\widetilde{q_3}: (\nu (ce)|\nu (e))$, and applying it to $q_6$ yields $\widetilde{q_6}: (\nu (\overline{e})|\nu (\top ))$. Applying $( NO )$ to $q_8: (ce\overline{f}|e)$ yields $\widetilde{q_8}: (\nu (ce\overline{f})|\nu (e))$; note that first applying $( AE )$ to $\widetilde{q_2}$ and $\widetilde{q_3}$ and then $( NO )$ to the result also yields exactly $\widetilde{q_8}$.

• $( IC )$ As ${\mathcal R_{ car }}$ is consistent, $( IC )$ can not be applied to ${\mathcal R_{ car }}$.

Thus, applying $\varTheta$ exhaustively and in arbitrary sequence to ${\mathcal R_{ car }}$ gives us the knowledge base $\varTheta ({\mathcal R_{ car }}) = \{\widetilde{q_1}, \widetilde{q_6}, \widetilde{q_8}\}$. In contrast, the transformation system $\mathcal {T}$ given in [4] would yield $\mathcal {T} ({\mathcal R_{ car }}) = \{\widetilde{q_1}, \widetilde{q_2}, \widetilde{q_3}, \widetilde{q_6}\}$ containing more conditionals.

Proposition 2

(properties of $\varTheta$). Let $\mathcal R$ be a knowledge base.

Proof

(1.) $( SF )$, $( AE )$, and $( IC )$ remove at least one conditional, and $( NO )$ can be applied at most once to any conditional. Hence, $\varTheta$ is terminating.

(2.) Since $\varTheta$ is terminating, local confluence of $\varTheta$ implies confluence of $\varTheta$; local confluence of $\varTheta$ in turn can be shown by ensuring that for every critical pair obtained form superpositioning two left hand sides of rules in $\varTheta$ reduces to the same knowledge base [2, 16]: Any critical pair obtained from $( IC )$ and another rule in $\varTheta$ reduces to $\diamond$ since all rules preserve the consistency status of a knowledge base. Any critical pair obtained from $( SF )$ with $( NO )$ reduces to the same knowledge base since applying $( NO )$ to a self-fulfilling conditional yields again a self-fulfilling conditional. Regarding critical pairs with respect to $( NO )$, we observe that if $\mathcal R$ contains two distinct conditionals $(B|A)$ and $(B'|A')$ with $(\nu (AB)|\nu (A)) = (\nu (A'B')|\nu (A'))$, then applying $( NO )$ first to either of the conditionals and second to the other one yields the same result. Critical pairs between $( AE )$ and $( NO )$ reduce to the same result because propositional normalization commutes with $( AE )$. For a critical pair of $( SF )$ and $( AE )$ consider $\mathcal R_0 = \mathcal R\cup \{(B|A), (B'|A')\}$ with $A \equiv A'$ and $A' \models B'$. Applying $( SF )$ yields $\mathcal R_1 = \mathcal R\cup \{(B|A)\}$, and applying $( AE )$ yields $\mathcal R_2 = \mathcal R\cup \{(BB'|A)\}$. Applying $( NO )$ to both $\mathcal R_1$ and $\mathcal R_2$ yields the same result because $A \equiv A'$, $A' \models B'$ and therefore $AB \equiv ABB'$. Thus, we are left with critical pairs obtained from $( AE )$ which arise from $\mathcal R\cup \{(B|A), (B'|A'), (B''|A'')\}$ with $A \equiv A' \equiv A''$ so that $( AE )$ could be applied to $\{(B|A), (B'|A')\}$ and to $\{(B'|A'), (B''|A'')\}$. Applying $( AE )$ to the result followed by $( NO )$ yields $\mathcal R\cup \{(\nu (BB'B'')|\nu (A))\}$ in both cases.

(3.) By Proposition 1, (3.) will follow from the proof of (4.).

(4.) We will show that $\equiv _{ae}$-equivalence is preserved by every rule in $\varTheta$. $( IC )$ Since $\varPi$ is a consistency test, $\mathcal R\equiv _{ae}\diamond$ because all inconsistent knowledge bases are $\equiv _{ae}$-equivalent. Because all other rules preserve the consistency status of $\mathcal R$, we assume that $\mathcal R$ is consistent when dealing with the other rules in $\varTheta$. $( SF )$ By Definition 3 we get $\mathcal R\cup \{(B|A)\} \equiv _{ae}\mathcal R$. $( AE )$ This rule preserves $\equiv _{ae}$-equivalence because $A \equiv A'$ implies $\{(B|A), (B'|A')\} \subseteq (\mathcal R\cup \{(B|A), (B'|A')\})_{|A}$, $(BB'|A) \in (\mathcal R\cup \{(BB'|A)\})_{|A}$, and $Mod (\{(B|A), (B'|A')\}) = Mod (\{(BB'|A)\})$. $( NO )$ This rule preserves $\equiv _{ae}$-equivalence because $(B|A) \in (\mathcal R\cup \{(B|A)\})_{|A}$, $(\nu (AB)|\nu (A)) \in (\mathcal R\cup \{(\nu (AB)|\nu (A))\})_{|A}$, and $Mod (\{(B|A)\}) = Mod (\{(\nu (AB)|\nu (A))\})$.

(5.) The $\equiv _{ae}$-minimizing property will follow from the proof of (6.).

(6.) From (1.) and (2.) we conclude that $\varTheta (\mathcal R)$ is well defined. If $\varTheta (\mathcal R)$ was not in ANF then at least one of the rules in $\varTheta$ would be applicable to $\varTheta (\mathcal R)$, contradicting that $\varTheta$ has been applied exhaustively.    $\square$

Proposition 2 ensures that applying $\varTheta$ to a knowledge base $\mathcal R$ always yields the unique normal form $\varTheta (\mathcal R)$ that is in ANF. This provides a convenient decision procedure for antecedentwise equivalence and thus also for model equivalence.

Proposition 3

(antecedentwise equivalence). Let $\mathcal R$, $\mathcal R'$ be knowledge bases. Then $\mathcal R\equiv _{ae}\mathcal R'\text { iff } \varTheta (\mathcal R) = \varTheta (\mathcal R')$.

5 Orderings and Renamings for Conditionals

For developing a method for the systematic generation of knowledge bases in ANF, we will represent each formula $A \in \mathcal L$ uniquely by its set $\varOmega _A$ of satisfying worlds. The two conditions $B \subsetneqq A$ and $B \not = \emptyset$ then ensure the falsifiability and the verifiability of a conditional $(B|A)$, thereby excluding any trivial conditional [8]. This yields a propositional normalization function $\nu$, giving us:

Proposition 4

($NFC (\varSigma )$ [9]). For $NFC (\varSigma ) = \{(B|A) \mid A \subseteq \varOmega _{\varSigma }, \, B \subsetneqq A, \, B \not = \emptyset \},$ the set of normal form conditionals over a signature $\varSigma$, the following holds:

• (nontrivial) $NFC (\varSigma )$ does not contain any trivial conditional.

• (complete) For every nontrivial conditional over $\varSigma$ there is an equivalent conditional in $NFC (\varSigma )$.

• (minimal) All conditionals in $NFC (\varSigma )$ are pairwise non-equivalent.

For instance, for $\varSigma _{ab}= \{a,b\}$ we have where the latter is in $NFC (\varSigma _{ab})$. Out of the different 256 conditionals over $\varSigma _{ab}$ obtained when using sets of worlds as formulas, only 50 are in $NFC (\varSigma _{ab})$ [9].

For defining a linear order on $NFC (\varSigma )$, we use the following notation. For an ordering relation $\leqslant$ on a set M, its lexicographic extension to strings over M is denoted by $\leqslant _{ lex }$. For ordered sets $S, S' \subseteq M$ with $S = \{e_1, \ldots , e_n\}$ and $S' = \{e'_1, \ldots , e'_{n'}\}$ where $e_i \leqslant e_{i+1}$ and $e'_j \leqslant e'_{j+1}$ its extension $\leqslant _{ set }$ to sets is:

$$\begin{aligned} S \leqslant _{ set } S' \text { iff } n < n' \text {, or } n = n' \text { and } e_1 \ldots e_n \leqslant _{ lex } e'_1 \ldots e'_{n'} \end{aligned}$$

(1)

For $\varSigma$ with ordering $\lessdot$, $[\![\omega ]\!]_{\lessdot }$ is the usual interpretation of a world $\omega$ as a binary number; e.g., for $\varSigma _{ab}$ with $a \lessdot b$, $[\![ab]\!]_{\lessdot } = 3$, $[\![a\overline{b}]\!]_{\lessdot } = 2$, $[\![\overline{a}b]\!]_{\lessdot } = 1$, and $[\![\overline{a}\overline{b}]\!]_{\lessdot } = 0$.

Definition 4

(induced ordering on formulas and conditionals). Let $\varSigma$ be a signature with linear ordering $\lessdot$. The orderings induced by $\lessdot$ on worlds $\omega , \omega '$ and conditionals $(B|A),(B'|A')$ over $\varSigma$ are given by:

(2)

(3)

In order to ease our notation, we will omit the upper symbol in ${\mathop {\lessdot }\limits ^{w}}$ and ${\mathop {\lessdot }\limits ^{c}}$, and write just $\lessdot$ instead, and analogously for the non-strict variants. For instance, for $\varSigma _{ab}$ with $a \lessdot b$ we have for worlds, and $(ab|ab \vee a\overline{b}) \,\lessdot \, (ab|ab \vee \overline{a}\overline{b})$ and $(ab \vee \overline{a}\overline{b}|ab \vee a\overline{b} \vee \overline{a}\overline{b}) \,\lessdot \, (\overline{a}\overline{b}|ab \vee a\overline{b} \vee \overline{a}b \vee \overline{a}\overline{b})$ for conditionals.

Proposition 5

($NFC (\varSigma )$, $\lessdot$ [9]). For a linear ordering $\lessdot$ on a signature $\varSigma$, the induced ordering $\lessdot$ according to Definition 4 is a linear ordering on $NFC (\varSigma )$.

Given the ordering $\lessdot$ on $NFC (\varSigma )$ from Proposition 5, we will now define a new ordering $\prec \mathrel {}\mathrel {\cdot }$ on these conditionals that takes isomorphisms (or renamings) $\rho :\, \varSigma \rightarrow \varSigma$ into account and prioritizes the $\lessdot$-minimal elements in each isomorphism induced equivalence class. As usual, $\rho$ is extended canonically to worlds, formulas, conditionals, knowledge bases, and to sets thereof. We say that X and $X'$ are isomorphic, denoted by $X \simeq X'$, if there exists a renaming $\rho$ such that $\rho (X) = X'$. For a set M, $m \in M$, and an equivalence relation $\equiv$ on M, the set of equivalence classes induced by $\equiv$ is denoted by $[M]_{/\equiv }$, and the unique equivalence class containing m is denoted by $[m]_{\equiv }$. For instance, for $\varSigma _{ab}$ the only non-identity renaming is the function $\rho _{ab}$ with $\rho _{ab}(a)=b$ and $\rho _{ab}(b)=a$, $[\varOmega _{\varSigma _{ab}}]_{/\simeq } = \{[ab], [a\overline{b}, \overline{a}b], [\overline{a}\overline{b}]\}$ are the three equivalence classes of worlds over $\varSigma _{ab}$, and we have $[(ab|ab \vee a\overline{b})]_{\simeq } = [(ab|ab \vee \overline{a}b)]_{\simeq }$.

Definition 5

($cNFC (\varSigma )$, $\prec \mathrel {}\mathrel {\cdot }$ [9]). Given a signature $\varSigma$ with linear ordering $\lessdot$, let $[ NFC (\varSigma )]_{/\simeq } = \{[r_1]_{\simeq }, \ldots , [r_m]_{\simeq }\}$ be the equivalence classes of $NFC (\varSigma )$ induced by isomorphisms such that for each $i \in \{1,\ldots ,m\}$, the conditional $r_i$ is the minimal element in $[r_i]_{\simeq }$ with respect to $\lessdot$, and $r_1 \lessdot \ldots \lessdot r_m$. The canonical normal form conditionals over $\varSigma$ are $cNFC (\varSigma ) = \{r_1, \ldots , r_m\}$. The canonical ordering on $NFC (\varSigma )$, denoted by $\prec \mathrel {}\mathrel {\cdot }$, is given by the schema

$$ r_1 \prec \mathrel {}\mathrel {\cdot }\ldots \prec \mathrel {}\mathrel {\cdot }r_m \prec \mathrel {}\mathrel {\cdot }[r_1]_{\simeq } \setminus \{r_1\} \prec \mathrel {}\mathrel {\cdot }\ldots \prec \mathrel {}\mathrel {\cdot }[r_m]_{\simeq } \setminus \{r_m\} $$

where $r \prec \mathrel {}\mathrel {\cdot }r' \text { iff } r \lessdot r'$ for all $i \in \{1,\ldots ,m\}$ and all $r, r' \in [r_i]_{\simeq } \setminus \{r_i\}$.

Proposition 6

($NFC (\varSigma )$, $\prec \mathrel {}\mathrel {\cdot }$ [9]). For a linear ordering $\lessdot$ on a signature $\varSigma$, the induced ordering $\prec \mathrel {}\mathrel {\cdot }$ according to Definition 5 is a linear ordering on $NFC (\varSigma )$.

While $NFC (\varSigma _{ab})$ contains 50 conditionals, there are 31 equivalence classes in $[ NFC (\varSigma _{ab})]_{/\simeq }$; hence $cNFC (\varSigma _{ab})$ has 31 elements [9]. The three smallest elements in $NFC (\varSigma _{ab})$ w.r.t. $\prec \mathrel {}\mathrel {\cdot }$ are , , , and their corresponding equivalence classes are , , and .

6 Generating Knowledge Bases in ANF

The algorithm $KB_{ gen }^{ae}$ (Algorithm 1) generates all consistent knowledge bases up to antecedentwise equivalence and up to isomorphisms. It uses pairs $\langle \mathcal R,\, C\rangle$ where $\mathcal R$ is a knowledge base and C is a set of conditionals that are candidates for extending $\mathcal R$ to obtain a new knowledge base. For extending $\mathcal R$, conditionals are considered sequentially according to their $\prec \mathrel {}\mathrel {\cdot }$ ordering. Note that in Line 3, only the canonical conditionals (which are minimal with respect $\prec \mathrel {}\mathrel {\cdot }$) are used for initializing the set of one-element knowledge bases. In Line 3 (and in Line 11, respectively), a conditional r is selected for initializing (or extending, respectively) a knowledge base. In Lines 4–6 (and in lines 13–15, respectively), in the set D conditionals are collected that do not have to be considered as candidates for further extending the current knowledge base: $D_1$ contains all conditionals that are smaller than r w.r.t. $\prec \mathrel {}\mathrel {\cdot }$, $D_2$ contains all conditionals having the same antecedent as r (since R should be ANF), and $\overline{r}$ would make $\mathcal R$ inconsistent. The consistency test used in Line 12 can easily be implemented by the well-known tolerance test for conditional knowledge bases [14].

Proposition 7

$\varvec{(} KB_{ gen }^{ ae }$). Let $\varSigma$ be a signature with linear ordering $\lessdot$. Then applying $KB_{ gen }^{ae}$ to it terminates and returns $\mathcal {KB}$ for which the following holds:

Proof

The proof is obtained by formalizing the description of $KB_{ gen }^{ae}$ given above and the following observations. Note that $KB_{ gen }^{ae}$ exploits the fact that every subset of a consistent knowledge base is again a consistent knowledge base. Thus building up knowledge bases by systematically adding remaining conditionals according to their linear ordering $\prec \mathrel {}\mathrel {\cdot }$ ensures completeness; the removal of candidates in Lines 5 and 14 does not jeopardize completeness since Proposition 2 ensures that for each knowledge base an antecedentwise equivalent knowledge base exists that for any propositional formula A contains at most one conditional with antecedent A. Checking consistency when adding a new conditional ensures consistency of the resulting knowledge base. ANF is ensured because all conditionals in $NFC (\varSigma )$ are of the form $(AB|A)$. Because for all A, each generated $\mathcal R$ contains at most one conditional with antecedent A, $\equiv _{ae}$-minimality is guaranteed, and $\simeq$-minimality can be shown by induction on the number of conditionals in a knowledge base.    $\square$

Note that $KB_{ gen }^{ae}$ generates significantly fewer knowledge bases than the algorithm $GenKB$ given in [9]. For each formula A, each $\mathcal R\in GenKB (\varSigma )$ may contain up to half of all conditionals in $NFC (\varSigma )$ with antecedent A,¹ while $\mathcal R\in KB_{ gen }^{ae} (\varSigma )$ may contain at most one conditional with antecedent A.

For instance, $KB_{ gen }^{ae} (\varSigma _{ab})$ will generate the knowledge base but it will not generate the knowledge base which is antecedentwise equivalent to $\mathcal R_7$, i.e., $\mathcal R_8 \equiv _{ae}\mathcal R_7$. Furthermore, $KB_{ gen }^{ae} (\varSigma _{ab})$ will also not generate, e.g., the knowledge bases which are both antecedentwise equivalent to $\mathcal R_7$ when taking isomorphisms into account; specifically, we have $\rho _{ab}(\mathcal R_{10}) = \mathcal R_7$, and $\rho _{ab}(\mathcal R_9) = \mathcal R_8$ and hence also $\rho _{ab}(\mathcal R_9) \equiv _{ae}\mathcal R_7$.

7 Conclusions and Further Work

Aiming at a compact and unique normal form of conditional knowledge bases, we introduced the new notion of antecedentwise equivalence. We developed a system $\varTheta$ transforming every knowledge base into its unique antecedent normal form. The algorithm $KB_{ gen }^{ae}$ is complete in the sense that it generates, for any signature $\varSigma$, knowledge bases in ANF such that all knowledge bases over $\varSigma$ are covered up to isomorphisms and antecedentwise equivalence. Furthermore, the set of knowledge bases returned by $KB_{ gen }^{ae}$ is minimal because no two different knowledge bases are generated such that they or any isomorphic images of them are antecedentwise equivalent. Currently, we are working with $KB_{ gen }^{ae}$ and the reasoning system InfOCF [6] for empirically evaluating different nonmonotonic inference relations induced by a conditional knowledge base and for computing the full closures of such inference relations [18]. Another part of our future work is the investigation of inferential equivalence of ANF (for another normal form see [3, 7]) with respect to semantics that are not syntax independent like rational closure (cf. [11, 13]), but that are syntax dependent like lexicographic closure [19].