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:

- a
*syntax*, which is used to define the well-formed formulae; - a
*proof theory*, which allows for saying when a formula follows from another one; and - a
*model-theoretic semantics*, which establishes when a model satisfies a formula.

The syntax is defined from a finite alphabet of propositional symbols , possibly with subscripts, and the usual set of propositional connectives , , .

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 , then the fact holds. We can thus say that the formula is part of the knowledge represented by .

In some cases, we want knowledge bases to represent models
rather than sets of formulas. An * interpretation* for
an alphabet of propositional variables is a mapping from
in
. The * model-theoretic
semantics* of the propositional calculus is the usual way
of extending an interpretation for 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 for denoting default rules, while logic programming has a special unary connective , and so on. A knowledge base of a formalism 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 is a binary relation on the set of knowledge bases and formulae. Intuitively, means that is a consequence of the knowledge base , according to the rules of the formalism . As a result, the set of formulae that are implied by a knowledge base is exactly the knowledge represented by .

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 , we assume that is a knowledge base in the syntax of , while is a propositional formula.

This allows for saying that two knowledge bases and , expressed in two different formalisms and , represent the same piece of knowledge: this is true when, for any propositional formula it holds if and only if .

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

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:

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 is the set of formulae such that , and the size of is at most the size of . This is done for two reasons: first, formulas that are larger than are likely to contain large parts that are actually independent from ; second, we can give technicals result in a very simple way by using the compilability classes introduced in the next section.

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, if and only if and . The assumption on the size of is not restrictive in this case, if is a CNF formula.