Notations and Assumptions

In this section we define what knowledge bases and formalisms are. Since we want to consider formalisms that are very different both in syntax and in semantics, we need very general definitions. Let us consider, as a base case, the formalism of propositional calculus. Formally, we can assume that it is composed of three parts:

1. a syntax, which is used to define the well-formed formulae;

2. a proof theory, which allows for saying when a formula follows from another one; and

3. a model-theoretic semantics, which establishes when a model satisfies a formula.

The syntax is defined from a finite alphabet of propositional symbols $L=\{a,b,c,\ldots\}$, possibly with subscripts, and the usual set of propositional connectives $\wedge$, $\vee$, $\neg$.

In terms of knowledge representation, the proof theory can be seen as a way for extracting knowledge from a knowledge base. For example, if our knowledge base is $a \wedge c$, then the fact $a \vee b$ holds. We can thus say that the formula $a \vee b$ is part of the knowledge represented by $a \wedge c$.

In some cases, we want knowledge bases to represent models rather than sets of formulas. An interpretation for an alphabet of propositional variables $L$ is a mapping from $L$ in $\{{\sf true}, {\sf false}\}$. The model-theoretic semantics of the propositional calculus is the usual way of extending an interpretation for $L$ to well-formed formulas.

Let us now extend such definition to generic formalisms: a formalism is composed of a syntax, a proof theory, and a model-theoretic semantics.

We remark that each formalism has its own syntax: for instance, default logic includes a ternary connective $\frac{~~:~~}{~~~}$ for denoting default rules, while logic programming has a special unary connective $not()$, and so on. A knowledge base of a formalism $F$ is simply a well-formed formula, according to the syntax of the formalism.

Each formalism has its own proof theory as well. The proof theory of a formalism $F$ is a binary relation $\vdash_F$ on the set of knowledge bases and formulae. Intuitively, $FB \vdash_F \phi$ means that $\phi$ is a consequence of the knowledge base $KB$, according to the rules of the formalism $F$. As a result, the set of formulae $\phi$ that are implied by a knowledge base $KB$ is exactly the knowledge represented by $KB$.

The base of a comparison between two different formalisms is a concept of equivalence, allowing for saying that two knowledge bases (of two different formalisms) represent the same piece of knowledge. Since the knowledge represented by a knowledge base is the set of formulas it implies, we have to assume that the syntax of these formulae is the same for all formalisms. Namely, we always assume that the formulae implied by a knowledge base are well-formed formulae of the propositional calculus. In other words, each formalism has a syntax for the knowledge bases: however, we assume that the proof theory relates knowledge bases (formulae in the syntax of the formalism) with propositional formulae. So, while writing $KB \vdash_F \phi$, we assume that $KB$ is a knowledge base in the syntax of $F$, while $\phi$ is a propositional formula.

This allows for saying that two knowledge bases $KB_1$ and $KB_2$, expressed in two different formalisms $F_1$ and $F_2$, represent the same piece of knowledge: this is true when, for any propositional formula $\phi$ it holds $KB_1 \vdash_{F_1} \phi$ if and only if $KB_2 \vdash_{F_2} \phi$.

The model-theoreric semantics of a formalism is a relation $\models_F$ between propositional models and knowledge bases. In this case, we assume a fixed alphabet $L$, thus the set of all interpretations is common to all formalisms. When a model $M$ and a knowledge base $KB$ are in the relation, we write $M \models_F KB$. Intuitively, this means that the model $M$ supports the piece of knowledge represented by $KB$.

We remark that some formalisms, e.g. credolous default logic [45], have a proof theory, but do not have a model-theoretic semantics. It is also possible to conceive formalisms with a model-theoretic semantics but no proof theory. When both of them are defined, we assume that they are related by the following formula:

$$KB \vdash_F \phi \mbox{ ~~ iff ~~ } \forall I ~.~ I \models KB \mbox{ implies } I \models \phi$$

Regarding the proof theory of formalisms, we only consider formulae that are shorter than the knowledge base, that is, we assume that the knowledge represented by a knowlegde base $KB$ is the set of formulae $\phi$ such that $KB \vdash_F \phi$, and the size of $\phi$ is at most the size of $KB$. This is done for two reasons: first, formulas that are larger than $KB$ are likely to contain large parts that are actually independent from $KB$; second, we can give technicals result in a very simple way by using the compilability classes introduced in the next section.

Assumption 1  

We consider only formulae whose size is less than or equal to that of the knowledge base.

All formalisms we consider satisfy the right-hand side distruibutivity of conjunction, that is, $KB \vdash_F \phi \wedge \mu$ if and only if $KB \vdash_F \phi$ and $KB \vdash_F \mu$. The assumption on the size of $\phi$ is not restrictive in this case, if $\phi$ is a CNF formula.