Reductions among KR Formalisms

We now define the forms of reduction between PKR formalisms that we analyze in the following sections. A formula can always be represented as a string over an alphabet $\Sigma$ , hence from now on we consider translations as functions transforming strings.

Let

and

be two PKR formalisms. There exists a poly-size reduction from

, denoted as $f:F_1 \mapsto F_2$ , if

is a poly-size function such that for any given knowledge base

is a knowledge base in

. Clearly, reductions should be restricted to produce a meaningful output. In particular, we now discuss reductions that preserve the models of the original theory.

The semantic approach by Gogic and collegues [21] is that the models of the two knowledge bases must be exactly the same. In other words, if a knowledge base

of the formalism

is translated into a knowledge base

of the formalism

, then $M \models_{F_1} KB$ if and only if $M \models_{F_2} KB'$ . This approach can be summarized by: a reduction between formalisms $F_{1}$ and $F_{2}$ is a way to translate knowledge bases of $F_{1}$ into knowledge bases of $F_{2}$ , preserving their sets of models. While this semantics is intuitively grounded, it is very easy to show examples in which two formalisms that we consider equally space-efficient cannot be translated to each other. Let us consider for instance a variant of the propositional calculus in which the syntax is that formulas must be of the form $x_1 \wedge F$ , where

is a regular formula over the variables $x_2, \ldots$ . Clearly, this formalism is able to represent knowledge in the same space than the propositional calculus (apart a polynomial factor). However, according to the definition, this formalism cannot be translated to propositional calculus: there is no knowledge base that is equivalent to $KB=\neg x_1$ . Indeed, the only model of

is $\emptyset$ , while any model of any consistent knowledge base of the modified propositional calculus contains

We propose a more general approach that can deal also with functions

that change the language of the

. To this end, we allow for a translation $g_{KB}$ from models of

to models of

. We stress that, to be as general as possible, the translation may depend on

-- i.e., different knowledge bases may have different translations of their models. We want this translation easy to compute, since otherwise the computation of $g_{KB}$ could hide the complexity of reasoning in the formalism. However, observe that to this end, it is not sufficient to impose that $g_{KB}$ is computable in polynomial time. In fact, once

is fixed, its models could be trivially translated to models of

in constant time, using a lookup table. This table would be exponentially large, though; and this is what we want to forbid. Hence, we impose that $g_{KB}$ is a circuit of polynomial-size wrt

. We still use a functional notation $g_{KB}(M)$ to denote the result of applying a model

to the circuit $g_{KB}$ . A formal definition follows.

Definition 8 (Model Preservation) A poly-size reduction $f:F_1 \mapsto F_2$ satisfies model-preservation if there exists a polynomial

such that, for each knowledge base

there exists a circuit $g_{KB}$ whose size is bounded by $p(\vert KB\vert)$ , and such that for every interpretation

of the variables of

it holds that $M \models_{F_1} KB$ iff $g_{KB}(M) \models_{F_2} f(KB)$ .

The rationale of model-preserving reduction is that the knowledge base

of the first formalism

can be converted into a knowledge base

in the second one

, and this reduction should be such that each model

can be easily translated into a model $g_{KB}(M)$ in

We require

to depend on

, because the transformation

, in general, could take the actual form of

into account. This happens in the following example of a model-preserving translation.

Example 3

We reduce a fragment of skeptical default logic [29] to circumscription with varying letters, using the transformation introduced by Etherington [15]. Let $\langle D, W \rangle$ be a prerequisite-free normal (PFN) default theory, i.e., all defaults are of the form $\frac{~:\gamma}{\gamma}$ , where $\gamma$ is a generic formula. Let be the set of letters occurring in $\langle D, W \rangle$ . Define as the set of letters $\{a_\gamma \vert \frac{~:\gamma}{\gamma} \in D\}$ . The function can be defined in the following way: $f(\langle D, W \rangle ) = CIRC(T;P_D;Z)$ , where $T = W \cup \{ a_\gamma \equiv \neg \gamma \vert a_\gamma \in P_D\}$ , are the letters to be minimized, and (the set of letters occurring in $\langle D, W \rangle$ ) are varying letters. We show that is a model-preserving poly-size reduction. In fact, given a set of PFN defaults let $g_{D}$ be a function such that for each interpretation for , $g_{D}(M) = M \cup \{a_\gamma \in P_D \vert M\models \neg\gamma\}$ . Clearly, is poly-size, $g_{D}$ can be realized by a circuit whose size is polynomial in $\vert D\vert$ , and is a model of at least one extension of $\langle D, W \rangle$ iff $g_{D}(M) \models CIRC(T;P_D;Z)$ . The dependence of only on stresses the fact that, in this case, the circuit does not depend on the whole knowledge base $\langle D, W \rangle$ , but just on .

Clearly, when models are preserved, theorems are preserved as well. A weaker form of reduction is the following one, where only theorems are preserved. Also in this case we allow theorems of

to be translated by a ``simple" circuit $g_{KB}$ to theorems of

Definition 9 (Theorem Preservation)

A poly-size reduction $f:F_1 \mapsto F_2$ satisfies theorem-preservation if there exists a polynomial such that, for each knowledge base in , there exists a circuit $g_{KB}$ whose size is bounded by $p(\vert KB\vert)$ , and such that for every formula $\varphi$ on the variables of , it holds that $KB \vdash_{F_1} \varphi$ iff $f(KB) \vdash_{F_2} g_{KB}(\varphi)$ .

The theorem-preserving reduction has a property similar to that of the model-preserving reduction, when the knowledge bases are used to represent theorems rather than models. Namely, a knowledge base

is translated into another knowledge base

which can be used to represent the same set of theorems. More precisely, we have that each theorem $\varphi$ of

is represented by a theorem $g_{KB}(\varphi)$ of

Winslett [50] 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

, both before and after the update (plus the reduction). Also the reduction shown in the previous Example 3 is theorem-preserving, this time

being the identity circuit.

We remark that our definitions of reduction are more general than those proposed by Gogic and collegues [21]. In fact, these authors consider only a notion analogous to Definition 8. and only for the case when

is the identity -- i.e., models in the two formalisms should be identical. By allowing a simple translation

between models Definition 8 covers more general forms of reductions preserving models, like the one of Example 3.