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
{true, 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 :**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 wellformed 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 ⊢F on the set of knowledge bases and formulae. Intuitively, F B ⊢F φ **means**
that φ is a consequence of the knowledge base KB**, according to the rules of the formalism**
F. As a result, the set of formulae φ 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 ⊢F φ, we assume that KB is a knowledge base in the syntax of F**, while**
φ **is a propositional formula.**
This allows for saying that two knowledge bases KB1 and KB2, expressed in two different formalisms F1 and F2**, represent the same piece of knowledge: this is true when, for**
any propositional formula φ it holds KB1 ⊢F1 φ **if and only if** KB2 ⊢F2 φ.

The model-theoreric semantics of a formalism is a relation |=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 |=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 (Reiter, 1980), 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 ⊢F Φ Iff ∀I . I |= Kb **Implies** I |= Φ

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 φ such that KB ⊢F φ, and the size of φ **is at most the size**
of KB. This is done for two reasons: first, formulas that are larger than KB **are likely to**