be used to represent the same set of theorems. More precisely, we have that each theorem ϕ of KB is represented by a theorem gKB(ϕ**) of** f(KB).

Winslett (1989) has shown an example of a reduction from updated knowledge bases to PL that is theorem-preserving but not model-preserving. Using Winslett's reduction, one could use the same machinery for propositional reasoning in the KB**, both before and after**
the update (plus the reduction). Also the reduction shown in **the previous Example 3 is** theorem-preserving, this time g **being the identity circuit.**
We remark that our definitions of reduction are more general than those proposed by Gogic and collegues (1995). In fact, these authors consider **only a notion analogous to** Definition 8. and only for the case when g **is the identity - i.e., models in the two formalisms** should be identical. By allowing a simple translation g **between models Definition 8 covers** more general forms of reductions preserving models, like the one of Example 3.

## 5. Comparing The Space Efficiency Of Pkr Formalisms

In this section we show how to use the compilability classes defined in Section 3 to compare the succinctness of PKR formalisms.

Let F1 and F2 be two formalisms representing sets of models. We prove that any knowledge base α in F1 **can be reduced, via a poly-size reduction, to a knowledge base** β in F2 **satisfying model-preservation if and only if the compilability class of the problem of**
model checking (first input: KB, second input: interpretation) in F2 **is higher than or equal**
to the compilability class of the problem of model checking in F1.

Similarly, we prove that theorem-preserving poly-size reductions exist if and only if the compilability class of the problem of inference **(first input: KB, second input: formula, cf.**
definition of the problem pli) in F1 **is higher than or equal to the compilability class of the**
problem of inference in F2.

In order to simplify the presentation and proof of the theorems we introduce some definitions.

Definition 10 (Model hardness/completeness) Let F **be a PKR formalism and** C be a complexity class. If the problem of model checking for F **belongs to the compilability class**
k❀C, where the model is the varying part of the instances, we say that F is in **model-C**.

Similarly, if model checking is k❀C-complete (hard), we say that F is model-C**-complete**
(hard). Definition 11 (Theorem hardness/completeness) Let F **be a PKR formalism and**
C be a complexity class. If the problem of inference for the formalism F **belongs to the**
compilability class k❀C, whenever the formula is the varying part of the instance, we say that F is in thm-C. Similarly, if inference is k❀C-complete (hard), we say that F is thmC**-complete (hard).**
These definitions implicitly define two hierarchies, which parallel the polynomial hierarchy (Stockmeyer, 1976): the model hierarchy (model-P,model-NP,model-Σp 2
,etc.) and the theorem hierarchy (thm-P,thm-NP,thm-Σp 2
,etc.). The higher a formalism is in the model hierarchy, the more its efficiency in representing models is - **and analogously for theorems.** As an example (Cadoli et al., 1996, Thm. 6), we characterize model and theorem classes of Propositional Logic.