Space Efficiency of Propositional Knowledge Representation Formalisms

M. Cadoli, F. M. Donini, P. Liberatore and M. Schaerf

Volume 13, 2000

Links to Full Text:

Abstract:
We investigate the space efficiency of a Propositional Knowledge Representation (PKR) formalism. Intuitively, the space efficiency of a formalism F in representing a certain piece of knowledge A, is the size of the shortest formula of F that represents A. In this paper we assume that knowledge is either a set of propositional interpretations (models) or a set of propositional formulae (theorems). We provide a formal way of talking about the relative ability of PKR formalisms to compactly represent a set of models or a set of theorems. We introduce two new compactness measures, the corresponding classes, and show that the relative space efficiency of a PKR formalism in representing models/theorems is directly related to such classes. In particular, we consider formalisms for nonmonotonic reasoning, such as circumscription and default logic, as well as belief revision operators and the stable model semantics for logic programs with negation. One interesting result is that formalisms with the same time complexity do not necessarily belong to the same space efficiency class.

Extracted Text


Journal of Artificial Intelligence Research 13 (2000) 1-31 Submitted 8/99;
published 8/00

Space Efficiency of Propositional Knowledge Representation

Formalisms

Marco Cadoli cadoli@dis.uniroma1.itDipartimento di Informatica e Sistemistica
Universit`a di Roma "La Sapienza"Via Salaria 113, I-00198, Roma, Italy

Francesco M. Donini donini@dis.uniroma1.itPolitecnico di Bari Dipartimento
di di Elettrotecnica ed ElettronicaVia Orabona 4, I-70125, Bari, Italy

Paolo Liberatore liberato@dis.uniroma1.it Marco Schaerf schaerf@dis.uniroma1.it
Dipartimento di Informatica e Sistemistica Universit`a di Roma "La Sapienza"
Via Salaria 113, I-00198, Roma, Italy

Abstract We investigate the space efficiency of a Propositional Knowledge
Representation (PKR)formalism. Intuitively, the space efficiency of a formalism

F in representing a certain pieceof knowledge ff, is the size of the shortest
formula of F that represents ff. In this paper weassume that knowledge is
either a set of propositional interpretations (models) or a set of

propositional formulae (theorems). We provide a formal way of talking about
the relativeability of PKR formalisms to compactly represent a set of models
or a set of theorems. We introduce two new compactness measures, the corresponding
classes, and show that therelative space efficiency of a PKR formalism in
representing models/theorems is directly related to such classes. In particular,
we consider formalisms for nonmonotonic reasoning,such as circumscription
and default logic, as well as belief revision operators and the stable model
semantics for logic programs with negation. One interesting result is that
formalismswith the same time complexity do not necessarily belong to the
same space efficiency class.

1. Introduction During the last years a large number of formalisms for knowledge
representation (KR) have been proposed in the literature. Such formalisms
have been studied from several perspectives, including semantical properties,
and computational complexity. Here we investigate space efficiency, a property
that has to do with the minimal size needed to represent a certain piece
of knowledge in a given formalism. This study is motivated by the fact that
the same piece of knowledge can be represented by two formalisms using a
different amount of space. Therefore, all else remaining the same, a formalism
could be preferred over another one because it needs less space to store
information.

The definition of space efficiency, however, is not simple. Indeed, a formalism
may allow several different ways to represent the same piece of knowledge.
For example, let us assume that we want to represent the piece of knowledge
"today is Monday". In Propositional

cfl2000 AI Access Foundation and Morgan Kaufmann Publishers. All rights reserved.

Cadoli, Donini, Liberatore, & Schaerf Logic we may decide to use a single
propositional variable monday. The fact that today is Monday can be represented
by the formula monday, but also by the formula ~~monday, as well as monday
^ (rain . ~rain), because all formulae of the Propositional Logic that are
logically equivalent to monday represent exactly the same information.

In Propositional Logic, we should consider the shortest of the equivalent
formulae used to represent the information we have. The same principle can
be applied to a generic formalism: if it allows several formulae to represent
the same information, then we only take into account the shortest one. Therefore,
we say that the space efficiency of a formalism F in representing a certain
piece of knowledge ff is the size of the shortest formula of F that represents
ff. Space efficiency --also called succinctness or compactness-- of a formalism
is a measure of its ability in representing knowledge in a small amount of
space.

In this paper we focus on propositional KR (PKR) formalisms. We do not give
a formal definition of which formalisms are propositional and which one are
not: intuitively, in a propositional formalism, quantifications are not allowed,
and thus the formulae are syntactically bounded to be formed only using propositional
connectives, plus some other kind of nonclassical connectives (for instance,
negation in logic programs, etc.).

So far, we have not discussed what knowledge represents. A possible way to
think of a piece of knowledge is that it represents all facts that can be
inferred from it. In other words, knowing something is the same as knowing
everything that can be logically implied. The second way -- which is in some
cases more natural -- is to think of a piece of knowledge as the set of states
of the world that we consider possible.

In a more formal way, we say that knowledge is represented either by a set
of propositional interpretations (those describing states of the world we
consider plausible) or a set of formulae (those implied from what we know).
Consequently, we focus on both reasoning problems of model checking and theorem
proving. The following example shows that we can really think of knowledge
in both ways.

Example 1 We want to eat in a fast food, and want to have either a sandwich
or a salad (but not both), and either water or coke (but not both).

In Propositional Logic, each choice can be represented as a model, and the
following models represent all possible choices (models are represented by
writing down only the letters mapped to true).

A = {{sandwich, water}, {sandwich, coke}, {salad, water}, {salad, coke}}
For representing the set of choices we can use formulae instead of models.
In this case, we write down a set of formulae whose models represent exactly
the allowed choices, as follows.

C = (sandwich . salad) ^ (~sandwich . ~salad) ^ (sandwich ! ~salad) ^

(water . coke) ^ (~water . ~coke) ^ (~coke ! water)

Actually, we can get rid of redundancies, and end up with the following formula.

F = (sandwich . salad) ^ (~sandwich . ~salad) ^ (water . coke) ^ (~water
. ~coke)

2

Space Efficiency of Propositional Knowledge Representation Formalisms More
formally, F represents the set of models A, because for each interpretation
I, I 2 A holds if and only if I |= F . The formula F also represents the
set of formulae C, because Cn(F ) = Cn(C), where Cn(.) is the function that
gives the set of all conclusions that can be drawn from a propositional formula.

1.1 State of the Art A question that has been deeply investigated, and is
related to space efficiency, is the possibility of translating a formula
expressed in one formalism into a formula expressed in another formalism
(under the assumption, of course, that these formulae represent the same
knowledge).

In most cases, the analysis is about the possibility of translating formulae
from different formalisms to Propositional Logic (PL). For example, Ben-Eliyahu
and Dechter (1991, 1994) proposed a translation from default logic to PL,
and a translation from disjunctive logic programs to PL, while Winslett (1989)
introduced a translation from revised knowledge bases to PL, and Gelfond,
Przymusinska, and Przymusinskyi (1989) defined a translation from circumscription
to PL.

All the above translations, as well as many other ones in the literature,
lead to an exponential increase of the size of the formula, in the worst
case. When the best known translation yields a formula in the target formalism
which has exponential size w.r.t. the formula in the source formalism, a
natural question arising is whether such exponential blow up is due to the
specific translation, or is intrinsic of the problem. For example, although
all proposed translations from default logic to PL lead to the exponential
blow up, we cannot conclude that all possible translations suffer from this
problem: it could be that a polynomial translation exists, but it has not
discovered so far.

Some works have focussed on the question of whether this kind of exponential
increase in the size is intrinsic or not. Cadoli, Donini, and Schaerf (1996)
have shown that many interesting fragments of default logic and circumscription
cannot be expressed by polynomialtime fragments of PL without super-polynomially
increasing the size of formulae. It has been proved that such a super-polynomial
increase of size is necessary when translating unrestricted propositional
circumscription (Cadoli, Donini, Schaerf, & Silvestri, 1997) and most operators
for belief revision into PL (Cadoli, Donini, Liberatore, & Schaerf, 1999;
Liberatore, 1995).

Gogic and collegues (1995) analyzed the relative succinctness of several
PKR formalisms in representing sets of models. Among other results, they
showed that skeptical default logic can represent sets of models more succinctly
than circumscription.

Kautz, Kearns, and Selman (1995) and Khardon and Roth (1996, 1997) considered
representations of knowledge bases based on the notion of characteristic
model, comparing them to other representations, e.g., based on clauses. They
showed that the representation of knowledge bases with their characteristic
models is sometimes exponentially more compact than other ones, and that
the converse is true in other cases.

However, all the above results are based on specific proofs, tailored to
a specific reduction, and do not help us to define equivalence classes for
the space efficiency of KR formalisms. In a recent paper (Cadoli, Donini,
Liberatore, & Schaerf, 1996b), a new complexity measure for decision problems,
called compilability, has been introduced. In the

3

Cadoli, Donini, Liberatore, & Schaerf present paper we show how this new
measure can be directly used to characterize the space efficiency of PKR
formalisms. We emphasize methodological aspects, expressing in a more general
context many of the results presented before.

1.2 Goal The notion of polynomial time complexity has a great importance
in KR (as well as many other fields of computer science), as problems that
can be solved in polynomial time are to be considered easy, from a computational
point of view.

The notion of polynomial many-one reducibility also has a very intuitive
meaning when applied to KR: if there exists a polynomial many-one reduction
from one formalism to another one, then the time complexity of reasoning
in the two formalisms is comparable. This allows to say, e.g., that inference
in PL is coNP-complete, i.e. it is one of the hardest problems among those
in the complexity class coNP.

As a result, we have a formal tool for comparing the difficulty of reasoning
in two formalisms. What is missing is a way for saying that one formalism
is able to represent the same information in less space.

Example 2 We consider again the lunch scenario of the previous example. We
show that we can reduce the size of the representation using circumscription
instead of Propositional Logic. In PL, the knowledge of the previous example
was represented by the formula F :

F = (sandwich . salad) ^ (~sandwich . ~salad) ^ (water . coke) ^ (~water
. ~coke) The set of models of this formula is A, and the models of A are
exactly the minimal models of the formula Fc defined as follows.

Fc = (sandwich . salad) ^ (water . coke) By the definition of circumscription
(McCarthy, 1980) it holds that F is equivalent to CIRC(Fc; {sandwich, salad,
water, coke}, ;, ;). Note that Fc is shorter than F . If this result can
be proved to hold for arbitrary sets of models, we may conclude that circumscription
is more space efficient than Propositional Logic in representing knowledge
expressed as sets of models.

Our goal is to provide a formal way of talking about the relative ability
of PKR formalisms to compactly represent information, where the information
is either a set of models or a set of theorems. In particular, we would like
to be able to say that a specific PKR formalism provides "one of the most
compact ways to represent models/theorems" among the PKR formalisms of a
specific class.

1.3 Results We introduce two new compactness measures (model and theorem
compactness) and the corresponding classes (model-C and thm-C, where C is
a complexity class like P, NP, coNP, etc.). Such classes form two hierarchies
that are isomorphic to the polynomial-time hierarchy (Stockmeyer, 1976).
We show that the relative space efficiency of a PKR formalism is

4

Space Efficiency of Propositional Knowledge Representation Formalisms directly
related to such classes. In particular, the ability of a PKR formalism to
compactly represent sets of models/theorems is directly related to the class
of the model/theorem hierarchy it belongs to. Problems higher up in the model/theorem
hierarchy can represent sets of models/theorems more compactly than formalisms
that are in lower classes.

This classification is obtained through a general framework and not by making
direct comparisons and specific translations between the various PKR formalisms.
Furthermore, our approach also allows for a simple and intuitive notion of
completeness for both model and theorem hierarchies. This notion precisely
characterizes both the relation between formalisms at different levels, and
the relations between formalisms at the same level. An interesting result
is that two PKR formalisms in which model checking or inference belong to
the same time complexity class may belong to different compactness classes.
This may suggest a criterion for choosing between two PKR formalisms in which
reasoning has the same time complexity--namely, choose the more compact one.
Also, two PKR formalisms may belong to the same theorem compactness class,
yet to different model compactness classes. This stresses the importance
of clarifying whether one wants to represent models or theorems when choosing
a PKR formalism.

1.4 Outline In the next section we introduce the notation and the assumptions
that we adopt in this work. In Section 3 (Compilability) we briefly recall
some notions on non-uniform computation that are important for what follows
and we recall the basic definitions of compilability classes (Cadoli et al.,
1996b). In Section 4 (Reductions) we describe the constraints we impose on
reductions, while in Section 5 (Space Efficiency) we introduce our compactness
classes. In Section 6 (Applications) we actually compare many known PKR formalisms
using our framework. Finally, in Section 7 (Related Work and Conclusions)
we compare our work with other proposals presented in the literature and
draw some conclusions.

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

5

Cadoli, Donini, Liberatore, & Schaerf 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 OE means that OE is a consequence of the knowledge base KB, according
to the rules of the formalism F . As a result, the set of formulae OE 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 OE, we assume that KB is a knowledge base
in the syntax of F , while OE 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 OE it holds KB1 `F1 OE if
and only if KB2 `F2 OE.

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 OE iff 8I . I |= KB implies I |= OE 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 OE such that KB `F OE, and the size of OE is at most the
size of KB. This is done for two reasons: first, formulas that are larger
than KB are likely to

6

Space Efficiency of Propositional Knowledge Representation Formalisms 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 `F OE ^ u if and only if KB `F OE and KB `F u. The
assumption on the size of OE is not restrictive in this case, if OE is a
CNF formula.

3. Compilability Classes We assume the reader is familiar with basic complexity
classes, such as P, NP and (uniform) classes of the polynomial hierarchy
(Stockmeyer, 1976; Garey & Johnson, 1979). Here we just briefly introduce
non-uniform classes (Johnson, 1990). In the sequel, C, C0, etc. denote arbitrary
classes of the polynomial hierarchy.

We assume that the input instances of problems are strings built over an
alphabet Sigma . We denote with ffl the empty string and assume that the
alphabet Sigma  contains a special symbol # to denote blanks. The length
of a string x 2 Sigma * is denoted by |x|.

Definition 1 An advice A is a function that takes an integer and returns
a string.

Advices are important in complexity theory because definitions and results
are often based on special Turing machines that can determine the result
of an oracle "for free", that is, in constant time.

Definition 2 An advice-taking Turing machine is a Turing machine enhanced
with the possibility to determine A(|x|) in constant time, where x is the
input string.

Of course, the fact that A(|x|) can be determined in constant time (while
A can be an intractable or even undecidable function) makes all definitions
based on advice-taking Turing machine different from the same ones based
on regular Turing machine. For example, an advice-taking Turing machine can
calculate in polynomial time many functions that a regular Turing machine
cannot (including some untractable ones).

Note that the advice is only a function of the size of the input, not of
the input itself. Hence, advice-taking Turing machines are closely related
to non-uniform families of circuits (Boppana & Sipser, 1990). Clearly, if
the advice were allowed to access the whole instance, it would be able to
determine the solution of any problem in constant time.

Definition 3 An advice-taking Turing machine uses polynomial advice if there
exists a polynomial p such that the advice oracle A satisfies |A(n)| <= p(n)
for any nonnegative integers n.

The non-uniform complexity classes are based on advice-taking Turing machines.
In this paper we consider a simplified definition, based on classes of the
polynomial hierarchy.

7

Cadoli, Donini, Liberatore, & Schaerf Definition 4 If C is a class of the
polynomial hierarchy, then C/poly is the class of languages defined by Turing
machines with the same time bounds as C, augmented by polynomial advice.

Any class C/poly is also known as non-uniform C, where non-uniformity is
due to the presence of the advice. Non-uniform and uniform complexity classes
are related: Karp and Lipton (1980) proved that if NP ` P/poly then Pi p2
= Sigma p2 = PH, i.e., the polynomial hierarchy collapses at the second
level, while Yap (1983) generalized their results, in particular by showing
that if NP ` coNP/poly then Pi p3 = Sigma p3 = PH, i.e., the polynomial
hierarchy collapses at the third level. An inprovement of this results has
been given by K"obler and Watanabe (1998): they proved that Pi pk ` Sigma
pk/poly implies that the polynomial hierarchy collapses to ZPP(Sigma pk+1).
The collapse of the polynomial hierarchy is considered very unlikely by most
researchers in structural complexity.

We now summarize some definitions and results proposed to formalize the compilability
of problems (Cadoli et al., 1996b), adapting them to the context and terminology
of PKR formalisms. We remark that it is not the aim of this paper to give
a formalization of compilability of problems, or to analyze problems from
this point of view. Rather, we show how to use the compilability classes
as a technical tool for proving results on the relative efficiency of formalisms
in representing knowledge in little space.

Several papers in the literature focus on the problem of reducing the complexity
of problems via a preprocessing phase (Kautz & Selman, 1992; Kautz et al.,
1995; Khardon & Roth, 1997). This motivates the introduction of a measure
of complexity of problems assuming that such preprocessing is allowed. Following
the intuition that a knowledge base is known well before questions are posed
to it, we divide a reasoning problem into two parts: one part is fixed or
accessible off-line (the knowledge base), and the second one is varying,
or accessible on-line (the interpretation/formula). Compilability aims at
capturing the on-line complexity of solving a problem composed of such inputs,
i.e., complexity with respect to the second input when the first one can
be preprocessed in an arbitrary way. In the next section we show the close
connection between compilability and the space efficiency of PKR formalisms.

A function f is called poly-size if there exists a polynomial p such that
for all strings x it holds |f (x)| <= p(|x|). An exception to this definition
is when x represents a number: in this case, we impose |f (x)| <= p(x). As
a result, we can say that the function A used in advice-taking turing machine
is a polysize function.

A function g is called poly-time if there exists a polynomial q such that
for all x, g(x) can be computed in time less than or equal to q(|x|). These
definitions easily extend to binary functions as usual.

We define a language of pairs S as a subset of Sigma * * Sigma *. This
is necessary to represent the two inputs to a PKR reasoning problem, i.e.,
the knowledge base (KB), and the formula or interpretation. As an example,
the problem of Inference in Propositional Logic (pli) is defined as follows.

pli = {hx, yi | x is a set of propositional formulae (the KB), y is a formula,
and x ` y}

It is well known that pli is coNP-complete, i.e., it is one of the "hardest"
problems among those belonging to coNP. Our goal is to prove that pli is
the "hardest" theorem8

Space Efficiency of Propositional Knowledge Representation Formalisms proving
problem among those in coNP that can be solved by preprocessing the first
input in an arbitrary way, i.e., the KB. To this end, we introduce a new
hierarchy of classes, the non-uniform compilability classes, denoted as k;C,
where C is a generic uniform complexity class, such as P, NP, coNP, or Sigma
p2.

Definition 5 (k;C classes) A language of pairs S ` Sigma * * Sigma * belongs
to k;C iff there exists a binary poly-size function f and a language of pairs
S0 2 C such that for all hx, yi 2 S it holds:

hf (x, |y|), yi 2 S0 iff hx, yi 2 S Notice that the poly-size function f
takes as input both x (the KB) and the size of y (either the formula or the
interpretation). This is done for technical reason, that is, such assumption
allows obtaining results that are impossible to prove if the function f only
takes x as input (Cadoli et al., 1996b). Such assuption is useful for proving
negative results, that is, theorems of impossibility of compilation: indeed,
if it is impossible to reduce the complexity of a problem using a function
that takes both x and |y| as input, then such reduction is also impossible
using a function taking x only as its argument.

Theorem 1 (Cadoli, Donini, Liberatore, & Schaerf, 1997, Theorem 6) Let C
be a class in the polynomial hierarchy and S ` Sigma * * Sigma *. A problem
S belongs to k;C if and only if there exists a poly-size function f and a
language of pairs S0, such that for allh

x, yi 2 Sigma * * Sigma * it holds that:

1. for all y such that |y| <= k, hf (x, k), yi 2 S0 if and only if hx, yi
2 S; 2. S0 2 C.

Clearly, any problem whose time complexity is in C is also in k;C: just take
f (x, |y|) = x and S0 = S. What is interesting is that some problem in C
may belong to k;C0 with C0 ae C, e.g.,, some problems in NP are in k;P. This
is true for example for some problems in belief revision (Cadoli et al.,
1999). In the rest of this paper, however, we mainly focus on "complete"
problems, defined below. A pictorial representation of the class k;C is in
Figure 1, where we assume that S0 2 C.

For the problem pli no method proving that it belongs to k;P is known. In
order to show that it (probably) does not belong to k;P, we define a notion
of reduction and completeness.

Definition 6 (Non-uniform comp-reducibility) Given two problems A and B,
A is non-uniformly comp-reducible to B (denoted as A <=nu-comp B) iff there
exist two poly-size binary functions f1 and f2, and a polynomial-time binary
function g such that for every pair hx, yi it holds that hx, yi 2 A if and
only if hf1(x, |y|), g(f2(x, |y|), y)i 2 B.

The <=nu-comp reductions can be represented as depicted in Figure 2. Such
reductions satisfy all important properties of a reduction.

Theorem 2 (Cadoli et al., 1996b, Theorem 5) The reductions <=nu-comp satisfy
transitivity and are compatible (Johnson, 1990) with the class k;C for every
complexity class C.

9

Cadoli, Donini, Liberatore, & Schaerf

|y|!!!1

- | | y -

hx, yi 2 Sx S0 f --

6 Figure 1: A representation of k;C.

|y|

- -

6 | |

y0?

- f

2

y -

x0x g f1 -

-

-

Figure 2: The nu-comp-C reductions. Therefore, it is possible to define the
notions of hardness and completeness for k;C for every complexity class C.

Definition 7 (k;C-completeness) Let S be a language of pairs and C a complexity
class. S is k;C-hard iff for all problems A 2 k;C we have that A <=nu-comp
S. Moreover, S isk

;C-complete if S is in k;C and is k;C-hard.

We now have the right complexity class to completely characterize the problem
pli. In fact pli is k;coNP-complete (Cadoli et al., 1996b, Theorem 7). Furthermore,
the hierarchy formed by the compilability classes is proper if and only if
the polynomial hierarchy is proper (Cadoli et al., 1996b; Karp & Lipton,
1980; Yap, 1983) -- a fact widely conjectured to be true.

Informally, we may say that k;NP-hard problems are "not compilable to P",
as from the above considerations we know that if there exists a preprocessing
of their fixed part that makes them on-line solvable in polynomial time,
then the polynomial hierarchy collapses. The same holds for k;coNP-hard problems.
In general, a problem which is k;C-complete for a class C can be regarded
as the "toughest" problem in C, even after arbitrary preprocessing of the
fixed part. On the other hand, a problem in k;C is a problem that, after
preprocessing of the fixed part, becomes a problem in C (i.e., it is "compilable
to C").

We close the section by giving another example of use of the compilability
classes through the well-known formalism of Circumscription (McCarthy, 1980).
Let x be any propositional formula. The minimal models of x are the truth
assignments satisfying x having as few positive values as possible (w.r.t.
set containment). The problem we consider is: check whether a given model
is a minimal model of a propositional formula. This problem, called Minimal
Model checking (mmc), can be reformulated as the problem of model checking
in Circumscription, which is known to be co-NP-complete (Cadoli, 1992).

10

Space Efficiency of Propositional Knowledge Representation Formalisms If
we consider the knowledge base x as given off-line, and the truth assignment
y as given on-line, we obtain the following definition:

mmc = {hx, yi | y is a minimal model of x } This problem can be shown to
be k;coNP-complete (Cadoli et al., 1996b, Theorem 13). Hence, it is very
unlikely that it can be in k;P; that is, it is very unlikely that there exists
some off-line processing of the knowledge base, yielding (say) some data
structure x0, such that given y, it can now checked in polynomial time whether
y is a minimal model of x. This, of course, unless x0 has exponential size.
This observation applies also when x0 is a knowledge base in Propositional
Logic, and led to the interpretation that Circumscription is more compact,
or succint, than PL (Cadoli, Donini, & Schaerf, 1995; Gogic et al., 1995).
Our framework allows to generalize these results for all PKR formalisms,
as shown in the sequel.

4. 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 F1 and F2 be two PKR formalisms. There exists a poly-size reduction from
F1 to F2, denoted as f : F1 7! F2, if f is a poly-size function such that
for any given knowledge base KB in F1, f (KB) is a knowledge base in F2.
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 (1995) is that the models of
the two knowledge bases must be exactly the same. In other words, if a knowledge
base KB of the formalism F1 is translated into a knowledge base KB0 of the
formalism F2, then M |=F1 KB if and only if M |=F2 KB0. This approach can
be summarized by: a reduction between formalisms F1 and F2 is a way to translate
knowledge bases of F1 into knowledge bases of F2, 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 x1 ^ F , where F is a regular formula over the variables x2,
. . .. 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 = ~x1. Indeed,
the only model of KB is ;, while any model of any consistent knowledge base
of the modified propositional calculus contains x1.

We propose a more general approach that can deal also with functions f that
change the language of the KB. To this end, we allow for a translation gKB
from models of KB to models of f (KB). We stress that, to be as general as
possible, the translation may depend on KB -- i.e., different knowledge bases
may have different translations of their models. We want this translation
easy to compute, since otherwise the computation of gKB could hide the complexity
of reasoning in the formalism. However, observe that to this end, it is

11

Cadoli, Donini, Liberatore, & Schaerf not sufficient to impose that gKB is
computable in polynomial time. In fact, once KB is fixed, its models could
be trivially translated to models of f (KB) 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 gKB is a circuit of polynomial-size
wrt KB. We still use a functional notation gKB(M ) to denote the result of
applying a model M to the circuit gKB. A formal definition follows.

Definition 8 (Model Preservation) A poly-size reduction f : F1 7! F2 satisfies
modelpreservation if there exists a polynomial p such that, for each knowledge
base KB in F1 there exists a circuit gKB whose size is bounded by p(|KB|),
and such that for every interpretation M of the variables of KB it holds
that M |=F1 KB iff gKB(M ) |=F2 f (KB).

The rationale of model-preserving reduction is that the knowledge base KB
of the first formalism F1 can be converted into a knowledge base f (KB) in
the second one F2, and this reduction should be such that each model M in
F1 can be easily translated into a model gKB(M ) in F2.

We require g to depend on KB, because the transformation f , in general,
could take the actual form of KB into account. This happens in the following
example of a modelpreserving translation.

Example 3 We reduce a fragment of skeptical default logic (Kautz & Selman,
1991) to circumscription with varying letters, using the transformation introduced
by Etherington (1987). Let hD, W i be a prerequisite-free normal (PFN) default
theory, i.e., all defaults are of the form :flfl , where fl is a generic
formula. Let Z be the set of letters occurring inh

D, W i. Define PD as the set of letters {afl | :flfl 2 D}. The function f
can be defined in the following way: f (hD, W i) = CIRC(T ; PD; Z), where
T = W [ {afl j ~fl|afl 2 PD}, PD are the letters to be minimized, and Z (the
set of letters occurring in hD, W i) are varying letters. We show that f
is a model-preserving poly-size reduction. In fact, given a set of PFN defaults
D let gD be a function such that for each interpretation M for Z, gD(M )
= M [ {afl 2 PD|M |= ~fl}. Clearly, f is poly-size, gD can be realized by
a circuit whose size is polynomial in |D|, and M is a model of at least one
extension of hD, W i iff gD(M ) |= CIRC(T ; PD; Z). The dependence of g only
on D stresses the fact that, in this case, the circuit g does not depend
on the whole knowledge base hD, W i, but just on D.

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 KB to be translated by a "simple"
circuit gKB to theorems of KB.

Definition 9 (Theorem Preservation) A poly-size reduction f : F1 7! F2 satisfies
theorempreservation if there exists a polynomial p such that, for each knowledge
base KB in F1, there exists a circuit gKB whose size is bounded by p(|KB|),
and such that for every formula ' on the variables of KB, it holds that KB
`F1 ' iff f (KB) `F2 gKB(').

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 KB is translated into another knowledge
base f (KB) which can

12

Space Efficiency of Propositional Knowledge Representation Formalisms 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 ff in F1 can be reduced, via a poly-size reduction, to
a knowledge base fi 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 classk

;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-Sigma
p2,etc.) and the theorem hierarchy (thm-P,thm-NP,thm-Sigma p2,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.

13

Cadoli, Donini, Liberatore, & Schaerf Theorem 3 PL is in model-P and it is
thm-coNP-complete.

We can now formally establish the connection between succinctness of representations
and compilability classes. In the following theorems, the complexity classes
C, C1, C2 belong to the polynomial hierarchy (Stockmeyer, 1976). In Theorems
5 and 7 we assume that the polynomial hierarchy does not collapse.

We start by showing that the existence of model-preserving reductions from
a formalism to another one can be easily obtained if their levels in the
model hierarchy satisfy a simple condition.

Theorem 4 Let F1 and F2 be two PKR formalisms. If F1 is in model-C and F2
is modelC-hard, then there exists a poly-size reduction f : F1 7! F2 satisfying
model preservation.

Proof. Recall that since F1 is in model-C, model checking in F1 is in k;C,
and since F2 is model-C-hard, model checking in F1 is non-uniformly comp-reducible
to model checking in F2. That is, (adapting Def. 6) there exist two poly-size
binary functions f1 and f2, and a polynomial-time binary function g such
that for every pair hKB, M i it holds that

M |=F1 KB if and only if g(f2(KB, |M |), M ) |=F2 f1(KB, |M |) (note that
g is the poly-time function appearing in Def. 6, different from gKB which
is the poly-size circuit appearing in Def. 8).

Now observe that |M | can be computed from KB by simply counting the letters
appearing in KB; let f3 be such a counting function, i.e., |M | = f3(KB).
Clearly, f3 is poly-size. Define the reduction f as f (KB) = f1(KB, f3(KB)).
Since poly-size functions are closed under composition, f is poly-size. Now
we show that f is a model-preserving reduction. By Definition 8, we need
to prove that there exists a polynomial p such that for each knowledge base
KB in F1, there exists a poly-size circuit gKB such that for every interpretation
M of the variables of KB it holds that M |=F1 KB iff gKB(M ) |=F2 f (KB).

We proceed as follows: Given a KB in F1, we compute z = f2(KB, |M |) = f2(KB,
f3(KB)). Since f2 and f3 are poly-size, z has size polynomial with respect
to |KB|. Define the circuit gKB(M ) as the one computing g(z, M ) = g(f2(KB,
f3(KB)), M ). Since g is a poly-time function over both inputs, and z is
poly-size in KB, there exists a representation of g(z, M ) as a circuit gKB
whose size is polynomial wrt KB. From this construction, M |=F1 KB iff gKB(M
) |=F2 f (KB). Hence, the thesis follows.

The following theorem, instead, gives a simple method to prove that there
is no modelpreserving reduction from one formalism to another one.

Theorem 5 Let F1 and F2 be two PKR formalisms. If the polynomial hierarchy
does not collapse, F1 is model-C1-hard, F2 is in model-C2, and C2 ae C1,
then there is no poly-size reduction f : F1 7! F2 satisfying model preservation.

Proof. We show that if such a reduction exists, then C1/poly ` C2/poly which
implies that the polynomial hierarchy collapses at some level (Yap, 1983).
Let A be a complete problem for class C1 -- e.g., if C1 is Sigma p3 then
A may be validity of 989-quantified boolean formulae (Stockmeyer, 1976).
Define the problem fflA as follows.

fflA = {hx, yi | x = ffl (the empty string) and y 2 A}

14

Space Efficiency of Propositional Knowledge Representation Formalisms We
already proved (Cadoli et al., 1996b, Thm. 6) that fflA is k;C1-complete.
Since model checking in F1 is model-C1-hard, fflA is non-uniformly comp-reducible
to model checking in F1. That is, (adapting Def. 6) there exist two poly-size
binary functions f1 and f2, and a polynomial-time binary function g such
that for every pair hffl, yi, it holds hffl, yi 2 fflA if and only if g(f2(ffl,
|y|), y) |=F1 f1(ffl, |y|). Let |y| = n. Clearly, the knowledge base f1(ffl,
|y|) depends only on n, i.e., there is exactly one knowledge base for each
integer. Call it KBn. Moreover, f2(ffl, |y|) = f2(ffl, n) also depends on
n only: call it On (for Oracle). Observe that both KBn and On have polynomial
size with respect to n.

If there exists a poly-size reduction f : F1 7! F2 satisfying model preservation,
then given the knowledge base KBn there exists a poly-size circuit hn such
that g(On, y) |=F1 KBn if and only if hn(g(On, y)) |=F2 f (KBn).

Therefore, the k;C1-complete problem fflA can be non-uniformly reduced to
a problem in k;C2 as follows: Given y, from its size |y| = n one obtains
(with a preprocessing) f (KBn) and On. Then one checks whether the interpretation
hn(g(On, y)) (computable in polynomial time given n, y and On) is a model
in F2 for f (KBn). From the fact that model checking in F2 is in k;C2, we
have that k;C1 ` k;C2. We proved in a previous paper that such result implies
that C1/poly ` C2/poly (Cadoli et al., 1996b, Thm. 9), which in turns implies
that the polynomial hierarchy collapses (Yap, 1983).

The above theorems show that the hierarchy of classes model-C exactly characterizes
the space efficiency of a formalism in representing sets of models. In fact,
two formalisms at the same level in the model hierarchy can be reduced into
each other via a poly-size reduction (Theorem 4), while there is no poly-size
reduction from a formalism (F1) higher up in the hierarchy into one (F2)
in a lower class (Theorem 5). In the latter case we say that F1 is more space-efficient
than F2.

Analogous results (with similar proofs) hold for poly-size reductions preserving
theorems. Namely, the next theorem shows how to infer the existence of theorem-preserving
reductions, while the other one gives a way to prove that there is no theorem-preserving
reduction from one formalism to another one.

Theorem 6 Let F1 and F2 be two PKR formalisms. If F1 is in thm-C and F2 is
thm-Chard, then there exists a poly-size reduction f : F1 7! F2 satisfying
theorem preservation.

Proof. Recall that since F1 is in thm-C, inference in F1 is in k;C, and since
F2 is thm-Chard, inference in F1 is non-uniformly comp-reducible to inference
in F2. That is, (adapting Def. 6) there exist two poly-size binary functions
f1 and f2, and a polynomial-time binary function g1 such that for every pair
hKB, 'i it holds that

KB `F1 ' if and only if f1(KB, |'|) `F2 g(f2(KB, |'|), ') (here we distinguish
the poly-time function g appearing in Def. 6 and the poly-size circuit gKB
appearing in Def. 9).

Using Theorem 1 we can replace |'| with an upper bound in the above formula.
From Assumption 1, we know that the size of ' is less than or equal to the
size of KB; therefore we replace |'| with |KB|. The above formula now becomes

KB `F1 ' if and only if f1(KB, |KB|) `F2 g(f2(KB, |KB|), ')

15

Cadoli, Donini, Liberatore, & Schaerf Define the reduction f as f (KB) =
f1(KB, f3(KB)), where f3 is the poly-size function that computes the size
of its input. Since poly-size functions are closed under composition, f is
poly-size.

Now, we show that f is a theorem-preserving reduction, i.e.,f satisfies Def.
9. This amounts to proving that for each knowledge base KB in F1 there exists
a circuit gKB, whose size is poynomial wrt KB, such that for every formula
' on the variables of KB it holds that KB `F1 ' iff f (KB) `F2 gKB(').

We proceed as in the proof of Theorem 4: Given a KB in F1, let z = f2(KB,
f3(KB)). Since f2 and f3 are poly-size, z has polynomial size with respect
to |KB|. Define gKB(') = g(z, ') = g(f2(KB, f3(KB)), '). Clearly, gKB can
be represented by a circuit of polynomial size wrt KB. From this construction,
KB `F1 ' iff f (KB) `F2 gKB('). Hence, the claim follows.

Theorem 7 Let F1 and F2 be two PKR formalisms. If the polynomial hierarchy
does not collapse, F1 is thm-C1-hard, F2 is in thm-C2, and C2 ae C1, then
there is no poly-size reduction f : F1 7! F2 satisfying theorem preservation.

Proof. We show that if such a reduction exists, then C1/poly ` C2/poly and
the polynomial hierarchy collapses at some level (Yap, 1983). Let A be a
complete problem for class C1. Define the problem fflA as in the proof of
Theorem 5: this problem is k;C1-complete (Cadoli et al., 1996b, Thm. 6).
Since inference in F1 is thm-C1-hard, fflA is non-uniformly compreducible
to inference in F1. That is, (adapting Def. 6) there exist two poly-size
binary functions f1 and f2, and a polynomial-time binary function g such
that for every pair hffl, yi,h

ffl, yi 2 fflA if and only if f1(ffl, |y|) `F1 g(f2(ffl, |y|), y). Let |y|
= n. Clearly, the knowledge base f1(ffl, |y|) depends just on n, i.e., there
is one knowledge base for each integer. Call it KBn. Moreover, also f2(ffl,
|y|) = f2(ffl, n) depends just on n: call it On (for Oracle). Observe that
both KBn and On have polynomial size with respect to n.

If there exists a poly-size reduction f : F1 7! F2 satisfying theorem preservation,
then given the knowledge base KBn there exists a poly-time function hn such
that KBn `F1 g(On, y) if and only if f (KBn) `F2 hn(g(On, y)).

Therefore, the k;C1-complete problem fflA can be non-uniformly reduced to
a problem ink ;C2 as follows: Given y, from its size |y| = n one obtains
(with an arbitrary preprocessing) f (KBn) and On. Then one checks whether
the formula hn(g(On, y)) (computable in polytime given y and On) is a theorem
in F2 of f (KBn). From the fact that inference in F2 is in k;C2, we have
that k;C1 ` k;C2. It follows that C1/poly ` C2/poly (Cadoli et al., 1996b,
Thm. 9), which implies that the polynomial hierarchy collapses (Yap, 1983).

Theorems 4-7 show that compilability classes characterize very precisely
the relative capability of PKR formalisms to represent sets of models or
sets of theorems. For example, as a consequence of Theorems 3 and 7 there
is no poly-size reduction from PL to the syntactic restriction of PL allowing
only Horn clauses that preserves the theorems, unless the polynomial hierarchy
collapses. Kautz and Selman (1992) proved non-existence of such a reduction
for a problem strictly related to pli using a specific proof.

16

Space Efficiency of Propositional Knowledge Representation Formalisms 6.
Applications This section is devoted to the application of the theorems presented
in the previous section. Using Theorems 4-7 and results previously known
from the literature, we are able to asses model- and theorem-compactness
of some PKR formalisms.

We assume that definitions of Propositional Logic, default logic (Reiter,
1980), and circumscription (McCarthy, 1980) are known. Definitions of WIDTIO,
SBR, GCWA, and stable model semantics are in the appropriate subsections.

In the following proofs we refer to the problem 983QBF, that is, the problem
of verifying whether a quantified Boolean formula 9X8Y.~F is valid, where
X and Y are disjoint sets of variables, and F is a set of clauses on the
alphabet X [ Y , each composed of three literals. As an example, a simple
formula belonging to this class is: 9x1, x28y1, y2 ~((x1 . y2) ^ (~x1 . ~x2
. ~y1) ^ (~y1 . ~x2 . ~y2) ^ (~x1 . ~x2)).

The problem of deciding validity of a 983QBF is complete for the class Sigma
p2. As a consequence, the corresponding problem *983QBF, that is deciding
whether an input composed of any string (*) as the fixed part and a quantified
Boolean formula 9X8Y.~F as the varying one, is complete for the class k;Sigma
p2 (Liberatore, 1998). Notice that in most of the hardness proofs we show
in the sequel we use problems without any meaningful fixed part.

6.1 Stable Model Semantics Stable model semantics (SM) was introduced by
Gelfond and Lifschitz (1988) as a tool to provide a semantics for logic programs
with negation. their original proposal is now one of the standard semantics
for logic programs. We now recall the definition of propositional stable
model.

Let P be a propositional, general logic program. Let M be a subset (i.e.,
an interpretation) of the atoms of P . Let P M be the program obtained from
P in the following way: if a clause C of P contains in its body a negated
atom ~A such that A 2 M then C is deleted; if a body of a clause contains
a negated atom ~A such that A 62 M then ~A is deleted from the body of the
clause. If M is a least Herbrand model of P M then M is a stable model of
P .

For the formalism sm, we consider the program P as the knowledge base. We
write P |=sm Q to denote that query Q is implied by a logic program P under
Stable Model semantics.

In order to prove our result, we need to define the kernel of a graph.

Definition 12 (Kernel) Let G = (V, E) be a graph. A kernel of G is a set
K ` V such that, denoting H = V - K, it holds:

1. H is a vertex cover of G 2. for all j 2 H, there exists an i 2 K such
that (i, j) 2 E. We can now state the theorem on the compilability class
of inference in the stable model semantics, and the corresponding theorem
compactness class.

Theorem 8 The problem of inference for the Stable Model semantics is k;coNP-complete,
thus Stable Model Semantics is thm-coNPcomplete.

17

Cadoli, Donini, Liberatore, & Schaerf Proof. Membership in the class follows
from the fact that the problem is coNP-complete (Marek & Truszczy'nski, 1991).
For the hardness, we adapt the proof of Marek and Truszczy'nski (1991) showing
that deciding whether a query is true in all stable models is coNP-hard.

Let fflkernel be the language {ffl, G} such that G is a graph with at least
one kernel. Let |G| = n, and observe that G cannot have more vertices than
its size n.

We show that for each n, there exists a logic program Pn such that for every
graph G with at most n vertices, there exists a query QG such that G has
a kernel iff Pn 6|=sm QG.

Let the alphabet of Pn be composed by the following 2n2 + n propositional
letters:{ ai|i 2 {1..n} } [ {rij, sij|i, j 2 {1..n} }.

The program Pn is defined as:

aj :- ~ai, rij sij :- ~rij

rij :- ~sij 9?=?;

for i, j 2 {1..n}

Given a graph G = (V, E), the query QG is defined as

QG = ( .

(i,j)2E ~

rij) . ( .

(i,j)62E

rij)

The reduction from fflkernel to sm is defined as: f1(x, n) = Pn, i.e., f1
depends only on its second argument, f2(x, n) = ffl, i.e., f2 is a constant
function, and g = Qy, i.e., given a graph G, the circuit g computes the query
QG.

As a result, this is a k; reduction. We now show that this reduction is correct,
i.e.,h ffl, Gi 2 fflkernel (G has a kernel) iff Pn 6|=SM QG.

If-part. Suppose Pn 6|=SM QG. Then, there exists a stable model M of Pn such
that M |= ~QG. Observe that ~QG is equivalent to the conjunction of all rij
such that (i, j) 2 E, and all ~rij such that (i, j) 62 E. Simplifying Pn
with ~QG we obtain the clauses:

aj :- ~ai, for (i, j) 2 E (1) Observe that M contains all sij such that (i,
j) 62 E, and in order to be stable, -- i.e., to support atoms rij such that
(i, j) 2 E -- M contains no atom sij such that (i, j) 2 E.

Let H = {j|aj 2 M }, K = {i|ai 62 M }. Now H is a vertex cover of G, since
for each edge (i, j) 2 E, M should satisfy the corresponding clause (1) aj
: - ~ai, hence either ai 2 M , or aj 2 M . Moreover, for each j in H, the
atom aj is in M , and since M is a stable model, there exists a clause aj
:- ~ai such that ai 62 M , that is, i 2 K. Therefore, K is a kernel of G.

Only-if part. Suppose G = (V, E) has a kernel K, and let H = V - K. Let M
be the interpretation

M = {rij|(i, j) 2 E} [ {sij|(i, j) 62 E} [ {aj|j 2 H}

Obviously, M 6|= QG. We now show that M is a stable model of Pn, i.e., M
is a least Herbrand model of P Mn . In fact, P Mn contains the following
clauses:

sij for (i, j) 62 E (2)

rij for (i, j) 2 E (3)

aj :- rij for i 2 K (4)

18

Space Efficiency of Propositional Knowledge Representation Formalisms Clauses
in the last line are obtained from clauses in Pn of the form aj :- ~ai, rij,
where the clauses such that i 2 H (hence ai 2 M ) are deleted, while in the
other clauses the negated atom ~ai is deleted, since i 2 K, hence ai 62 M
. Now for each aj 2 M , the vertex j is in H, hence there is an edge (i,
j) 2 E, and i 2 K. Hence clauses (4) and (3) are in P Mn , hence in the least
Herbrand model of P Mn there are exactly all aj such that j 2 H.

6.2 Minimal Model Reasoning One of the most successful form of non-monotonic
reasoning is based on the selection of minimal models. Among the various
formalisms based on minimal model semantics we consider here Circumscription
(McCarthy, 1980) and the Generalized Closed World Assumption (GCWA) (Minker,
1982), which is a formalism to represent knowledge in a closed world.

We assume that the reader is familiar with Circumscription, we briefly present
the definition of GCWA. The model semantics for GCWA is defined as (a is
a letter):

M |=GCW A KB iff M |= KB[{~a | for any positive clause fl, if KB 6` fl then
KB 6` fl . a}

We can now present the results for these two formalisms. Theorem 9 The problem
of model checking for Circumscription is k;coNP-complete, thus Circumscription
is model-coNP-complete.

This result is a trivial corollary of a theorem already proved (Cadoli et
al., 1997, Theorem 6). In fact, that proof implicitly shows that model checking
for circumscription isk

;coNP-complete.

Theorem 10 The problem of model checking for GCWA is in k;P, thus GCWA is
in model-P.

Proof. As already pointed out (Cadoli et al., 1997), it is possible to rewrite
GCW A(T ) into a propositional formula F such that, for any given model M
, M |= GCW A(T ) if and only if M |= F . Moreover, the size of F is polynomially
bounded by the size of T . As a consequence, the model compactness for GCWA
is in the same class of PL. By Theorem 3 the thesis follows.

Theorem 11 The problem of inference for Circumscription is k;Pi p2-complete,
thus Circumscription is thm-Pi p2-complete.

This result is a trivial corollary of a theorem published in a previous paper
(Cadoli et al., 1997, Theorem 7) which implicitly shows that inference for
circumscription is k;Pi p2- complete.

Theorem 12 The problem of inference for GCWA is k;coNP-complete, thus GCWA
is thm-coNP-complete.

Proof. As already pointed out in the proof of Theorem 10, it is possible
to rewrite GCW A(T ) into a formula F that is equivalent to it. As a consequence,
a formula ff is a theorem of GCW A(T ) if and only if it is a theorem of
F . Thus, GCWA has at most the theorem compexity of PL. Since GCWA is a generalization
of PL, it follows that GCWA is in the same theorem compactness class of PL.
Hence, GCWA is thm-coNP-complete.

19

Cadoli, Donini, Liberatore, & Schaerf 6.3 Default Logic In this subsection
we present the results for default logic, in its two variants (credulous
and skeptical). For more details on these two main variants of default logic,
we refer the reader to the paper by Kautz and Selman (1991). Notice that
model-compactness is only applicable to skeptical default logic.

Theorem 13 The problem of model checking for skeptical default logic is k;Sigma
p2 complete, thus skeptical default logic is model-Sigma p2 complete.

Proof. The proof of membership is straightforward: since model checking for
skeptical default logic is in Sigma p2 (Liberatore & Schaerf, 1998), it
follows that it is also in k;Sigma p2.

The proof of k;Sigma p2-hardness is similar to the proof of Sigma p2-hardness
(Liberatore & Schaerf, 1998). The reduction is from the problem *983QBF.
Let hff, fii be an instance of *983QBF, where fi = 9X8Y.~F represents a valid
983QBF formula, and ff is any string.

Let n be the size of the formula F . This implies that the variables in the
formula are at most n. Let Gamma  = {fl1, . . . , flk} be the set of all
the clauses of three literals over this alphabet. The number of clauses of
three literals over an alphabet of n variables is less than O(n3), thus bounded
by a polynomial in n.

We prove that 9X8Y.~F is valid if and only if M is a model of some extension
of hW, Di, where

W = ;

D = [

fli2Gamma  ae

: ci ci ,

: ~ci~

ci oe [ [xi2X ae

: w ^ (w ! xi)

w ! xi ,

: w ^ (w ! ~xi)

w ! ~xi oe [ (

: w ^ Vfli2Gamma  ci ! fli

w )

M = {ci | fli 2 F }

The set {ci | 1 <= i <= k} is a set of new variables, one-to-one with the
elements of Gamma . Note that W and D only depends on the size n of F ,
while M depends on F . As a result, this is a <=nu-comp reduction.

We now prove that the formula is valid if and only if M is a model of some
extension of the default theory hW, Di. This is similar to an already published
proof (Liberatore & Schaerf, 1998). Consider an evaluation C1 of the variables
{ci} and an evaluation X1 of the variables X. Let D0 be the following set
of defaults.

D0 = [

ci2C1 ae

: ci ci oe [c

i62C1 ae

: ~ci~

ci oe [ [x

i2X1 ae

: w ^ (w ! xi)

w ! xi oe [x

i~2X1 ae

: w ^ (w ! ~xi)

w ! ~xi oe

This set of defaults has been chosen so that the set R of its consequences
corresponds to the sets C1 and X1. Namely, we have:

ci 2 C1 iff R |= ci ci 62 C1 iff R |= ~ci xi 2 X1 iff R |= w ! xi xi 62 X1
iff R |= w ! ~xi

20

Space Efficiency of Propositional Knowledge Representation Formalisms Now,
we prove that the consequences of this set of defaults are an extension of
the default theory if and only if the QBF formula is valid. Since all defaults
are semi-normal, we have to prove that:

1. the set of consequences of D0 is consistent; and 2. no other default is
applicable, that is, there is no other default whose precondition is

consistent with R.

Consistency of R follows by construction: assigning ci to true for each ci
2 C1, etc., we obtain a model of R.

We have then to prove that no other default is applicable. If ci 2 C1, the
default :~ci~ci is not applicable, and vice versa, if ~ci 2 C1, then :cici
is not applicable. Moreover, none

of the defaults :w^(w!xi)w!xi , is applicable if xi 62 X1, because in this
case w ! ~xi 2 R, thus~

w would follow (while w is a justification of the default). A similar statement
holds for :w^(w!~xi)

w!~xi if xi 2 X1.

As a result, the only applicable default may be the last one,

:w^Vfli2Gamma  ci!fli

w (recall thatF is negated). This default is applicable if and only if, for
the given evaluation of the c

i'sand xi's, the set of clauses is satisfiable. This amount to say: "there
is an extension in

which the last default is not applicable if and only if the QBF formula is
valid". Now, if the last default is applicable, then M is not a model of
the extension because w is the consequence of the last default while w 6|=
M . The converse also holds: if the last default is not applicable then M
is a model of the default theory.

As a result, the QBF is valid if and only if M is a model of the given default
theory.

Theorem 14 The inference problem for skeptical default logic is k;Pi p2
complete, thus skeptical default logic is thm-Pi p2 complete.

Proof. Since inference in skeptical default logic is in Pi p2, it is also
in k;Pi p2. k;Pi p2-hardness comes from a simple reduction from circumscription.
Indeed, the circumscription of a formula T is equivalent to the conjunction
of the extensions of the default theory hT, Di, where (Etherington, 1987):

D = [ ae : ~xi~x

i oe

As a result, CIRC(T ) |= Q if and only if Q is implied by hT, Di under skeptical
semantics. Since hT, Di only depends on T (and not on Q) this is a <=nu-comp
reduction. Since inference for circumscription is k;Pi p2-complete (see
Theorem 11), it follows that skeptical default logic is k;Pi p2-hard.

Theorem 15 The inference problem for credulous default logic is k;Sigma
p2 complete, thus credulous default logic is thm-Sigma p2 complete.

21

Cadoli, Donini, Liberatore, & Schaerf Proof. The proof is very similar to
the proof for model checking of skeptical default logic. Indeed, both problems
are k;Sigma p2 complete. Since the problem is in Sigma p2, as proved by
Gottlob (1992), it is also in k;Sigma p2. Thus, what we have to prove is
that is hard for that class.

We prove that the *983QBF problem can be reduced to the problem of verifying
whether a formula is implied by some extensions of a default theory (that
is, inference in credulous default logic).

Namely, a formula 8X9Y.~F is valid if and only if Q is derived by some extension
of the default theory hD, W i, where W and D are defined as follows (Gamma
is the set of all the clauses of three literals over the alphabet of F ,
and C is a set of new variables, one-to-one with Gamma ).

W = ;

D = [

ci2C ae

: ci ci ,

: ~ci~

ci oe [ [xi2X ae

: xi xi ,

: ~xi~

xi oe [ ( ~

(Vci2C ci ! fli) :

w )

Q = ^

fli2F

ci ^ ^

fli62F ~

ci ^ w

Informally, the proof goes as follows: for each truth evaluation of the variables
in C and X there is a set of defaults which are both justified and consistent.
A simple necessary and sufficient condition for the consequences of this
set of defaults to be an extension is the following. If, in this evaluation,
the formula

~ ^

ci=true

fli

is valid, then the last default is applicable, thus the extension also contains
w. The converse also holds: if the formula is not valid in the evaluation,
then the variable w is not in the extension.

As a result, there exists an extension in which Q holds if and only if there
exists an extension in which each ci is true if and only if fli 2 F , and
such that w also holds. When the variables ci have the given value, the above
formula is equivalent to ~F . As a result, such an extension exists if and
only if there exists a truth evaluation of the variables X in which ~F is
valid.

6.4 Belief Revision Many formalisms for belief revision have been proposed
in the literature, here we focus on two of them: WIDTIO (When In Doubt Throw
it Out) and SBR (Skeptical Belief Revision). Let K be a set of propositional
formulae, representing an agent's knowledge about the world. When a new formula
A is added to K, the problem of the possible inconsistency between K and
A arises. The first step is to define the set of sets of formulae W (K, A)
in the following way:

W (K, A) = {K0 K0 is a maximal consistent subset of K [ {A} containing A
}

22

Space Efficiency of Propositional Knowledge Representation Formalisms Any
set of formulae K0 2 W (K, A) is a maximal choice of formulae in K that are
consistent with A and, therefore, we may retain when incorporating A. The
definition of this set leads to two different revision operators: SBR and
WIDTIO.

SBR Skeptical Belief Revision (Fagin, Ullman, & Vardi, 1983; Ginsberg, 1986).
The revised

theory is defined as a set of theories: K * A .= {K0 | K0 2 W (K, A)}. Inference
in the revised theory is defined as inference in each of the theories:

K * A `SBR Q iff for all K0 2 W (K, A) , we have that K0 ` Q The model semantics
is defined as:

M |=SBR K * A iff there exists a K0 2 W (K, A) such that M |= K0

WIDTIO When In Doubt Throw It Out (Winslett, 1990). A simpler (but somewhat

drastical) approach is the so-called WIDTIO, where we retain only the formulae
of K that belong to all sets of W (K, A). Thus, inference is defined as:

K * A `W IDT IO Q iff T W (K, A) ` Q

The model semantics of this formalism is defined as:

M |=W IDT IO K * A iff M |= " W (K, A)

The results on model compactness have been shown by Liberatore and Schaerf
(2000). Here we recall them.

Theorem 16 (Liberatore & Schaerf, 2000, Theorem 11) The problem of model
checking for WIDTIO is in k;P, thus WIDTIO is in model-P.

Theorem 17 (Liberatore & Schaerf, 2000, Theorem 5) The problem of model checking
for Skeptical Belief Revision is k;coNP-complete, thus Skeptical Belief Revision
is model-coNP-complete.

The results on theorem compactness are quite simple and we provide here the
proofs. Theorem 18 The problem of inference for WIDTIO is k;coNP-complete,
thus WIDTIO is thm-coNP-complete.

Proof. Membership in the class thm-coNP immediately follows from the definition.
In fact, we can rewrite K * A into a propositional formula by computing the
set W (K, A) and then constructing their intersection. By construction their
intersection has size less than or equal to the size of K [ A. As a consequence,
after preprocessing, deciding whether a formula Q follows from K * A is a
problem in coNP. Hardness follows from the obvious fact that PL can be reduced
to WIDTIO and PL is thm-coNP-complete (see Theorem 3).

Theorem 19 The problem of inference for Skeptical Belief Revision is k;Pi
p2-complete, thus Skeptical Belief Revision is thm-Pi p2-complete.

23

Cadoli, Donini, Liberatore, & Schaerf

Time Complexity Space Efficiency Propositional P model-PLogic

- - WIDTIO Sigma p2-complete model-P(Liberatore & Schaerf, 1996) Th. 16

Skeptical coNP-complete model-coNP-completeBelief Revision (Liberatore &
Schaerf, 1996) Th. 17 Circumscription coNP-complete model-coNP-complete(Cadoli,
1992) Th. 9

GCWA coNP-hard, model-Pin Delta 

p 2[log n] Th. 10(Eiter & Gottlob, 1993)

Skeptical Sigma p2-complete model-Sigma p2-completeDefault Reasoning (Liberatore
& Schaerf, 1998) Th. 13

Credulous N/A N/ADefault Reasoning Stable Model P model-PSemantics

- -

Table 1: Complexity of model checking and Space Efficiency of Model Representations
Proof. Membership follows from the complexity results of Eiter and Gottlob
(1992), where they show that deciding whether K * A `SBR Q is a Pi p2-complete
problem. Hardness follows easily from Theorem 17. In fact, M |=SBR K * A
iff K * A 6`SBR ~f orm(M ), where f orm(M ) is the formula that represents
the model M . As a consequence, model checking can be reduced to the complement
of inference. Thus inference is k;Pi p2-complete.

6.5 Discussion Tables 1 and 2 summarize the results on space efficiency of
PKR formalisms and where they were proved (a dash "-" denotes a folklore
result).

First of all, notice that space efficiency is not always related to time
complexity. As an example, we compare in detail WIDTIO and circumscription.
From the table it follows that model checking is harder for WIDTIO than for
circumscription, and that inference has the same complexity in both cases.
Nevertheless, since circumscription is thm-Sigma p2-complete and WIDTIO
is thm-coNP-complete (and thus in thm-Sigma p2), there exists a poly-size
reduction from WIDTIO to circumscription satisfying theorem preservation.
The converse does not hold: since circumscription is thm-Sigma p2-complete
and WIDTIO is thm-coNP, unless the Polynomial Hierarchy does not collapse
there is no theorem-preserving poly-size reduction from the former formalism
to the latter. Hence, circumscription is a more compact formalism than WIDTIO
to represent theorems. Analogous considerations can be done for models. Intuitively,
this is due to the fact that for WIDTIO both model checking and inference
require a lot of work on the revised knowledge base alone--computing the
intersection of

24

Space Efficiency of Propositional Knowledge Representation Formalisms

Time Complexity Space Efficiency Propositional coNP-complete thm-coNP-completeLogic
(Cook, 1971) (Cadoli et al., 1996)

WIDTIO Pi p2-complete thm-coNP-complete(Eiter & Gottlob, 1992) & (Nebel,
1998) Th. 18

Skeptical Pi p2-complete thm-Pi p2-completeBelief Revision (Eiter & Gottlob,
1992) Th. 19 Circumscription Pi p2-complete thm-Pi p2-complete(Eiter &
Gottlob, 1993) Th. 11

GCWA Pi p2-complete thm-coNP-complete(Eiter & Gottlob, 1993) & (Nebel, 1998)
Th. 12 Skeptical Pi p2-complete thm-Pi p2-completeDefault Reasoning (Gottlob,
1992) Th. 14 Credulous Sigma p2-complete thm-Sigma p2-completeDefault Reasoning
(Gottlob, 1992) Th. 15 Stable Model coNP-complete thm-coNP-completeSemantics
(Marek & Truszczy'nski, 1991) Th. 8

Table 2: Complexity of inference and Space Efficiency of Theorem Representations
all elements of W (K, A). Once this is done, one is left with model checking
and inference in PL. Hence, WIDTIO has the same space efficiency as PL, which
is below circumscription.

Figures 3 and 4 contain the same information of Tables 1 and 2, but highlight
existing reductions. Each figure contains two diagrams, the left one showing
the existence of polynomial-time reductions among formalisms, the right one
showing the existence of polysize reductions. An arrow from a formalism to
another denotes that the former can be reduced to the latter one. We use
a bidirectional arrow to denote arrows in both directions and a dashed box
to enclose formalisms that can be reduced one into another. Note that some
formalisms are more appropriate in representing sets of models, while others
perform better on sets of formulae. An interesting relation exists between
skeptical default reasoning and circumscription. While there is no model-preserving
poly-size reduction from circumscription to skeptical default reasoning (Gogic
et al., 1995), a theorem-preserving poly-size reduction exists, as shown
by Theorem 14.

7. Related Work and Conclusions The idea of comparing the compactness of
KR formalisms in representing information is not novel in AI. It is well
known that first-order circumscription can be represented in secondorder
logic (Schlipf, 1987). Kolaitis and Papadimitriou (1990) discuss several
computational aspects of circumscription. Among many interesting results
they show a reduction from a restricted form of first-order circumscription
into first-order logic. The proposed reduction will increase the size of
the original formula by an exponential factor. It is left as an open problem
to show whether this increase is intrinsic, because of the different compactness
properties of the two formalisms, or there exists a more space-efficient
reduction. When a

25

Cadoli, Donini, Liberatore, & Schaerf

StableModel 6 6 oe -

6 oe -

.6

6 oe -

oe - oe -oe -

oe -WIDTIO GCWA

CircumscriptionSBR

PL Stable Model

SBR Circumscription

Skeptical Default

PL WIDTIO GCWA a. Time Complexity b. Space Efficiency

SkepticalDefault

Figure 3: Complexity of Model Checking vs. Space Efficiency of Model Representation

AAK oe - oe -

SSo Delta Delta 

Delta *

oe-

Delta Delta 

Delta *

oe- oe-oe-oe-

6?

oe -

oe-Circum SkepticalDefaultSBR DefaultCredulous SBR Circum SkepticalDefault
CredulousDefault

Model StablePL GCWAWIDTIOPL Stable Model

WIDTIO GCWA

b. Space efficiencya. Time complexity Figure 4: Complexity of Inference vs.
Space Efficiency of Theorem Representation

26

Space Efficiency of Propositional Knowledge Representation Formalisms first-order
language is used, more results on compactness and existence of reductions
are reported by Schlipf (1995).

Khardon and Roth (1996, 1997), and Kautz, Kearns and Selman (1995) propose
modelbased representations of a KB in Propositional Logic, and compare it
with formula-based representations. Although their results are significant
for comparing representations within PL, they refer only to this formalism,
hence they are not applicable to our comparison between different PKR formalisms.
The same comment applies also to the idea of representing a KB with an efficient
basis by Moses and Tennenholz (1996), since it refers only to one PKR formalism,
namely, PL.

An active area of research studies the connections of the various non-monotonic
logics. In particular, there are several papers discussing the existence
of translations that are polynomial in time and satisfy other intuitive requirements
such as modularity and faithfulness. Janhunen (1998), improving on results
of Imielinski (1987) and Gottlob (1995), shows that default logic is the
most expressive, among the non-monotonic logics examined, since both circumscription
and autoepistemic logic can be modularly and faithfully embedded in default
logic, but not the other way around. While these results are of interest
and help to fully understand the relation among many knowledge representation
formalisms, they are not directly related to ours. In fact, we allow for
translations that are more general than polynomial time, while in all of
the above papers they only consider translations that use polynomial time
and also satisfy additional requirements.

The first result on compactness of representations for a propositional language
is presented, to the best of our knowledge, by Kautz and Selman (1992). They
show that, unless there is a collapse in the polynomial hierarchy, the size
of the smallest representation of the least Horn upper bound of a propositional
theory is superpolynomial in the size of the original theory. These results
are also presented in a different form in the more comprehensive paper (Selman
& Kautz, 1996). The technique used in the proof has been then used by us
and other researchers to prove several other results on the relative complexity
of propositional knowledge representation formalisms (Cadoli et al., 1996,
1997, 1999; Gogic et al., 1995).

In a recent paper (Cadoli et al., 1996b) we introduced a new complexity measure,
i.e., compilability. In this paper we have shown how this measure is inherently
related to the succinctness of PKR formalisms. We analyzed PKR formalisms
with respect to two succinctness measures: succinctness in representing sets
of models and succinctness in representing sets of theorems.

The main advantage of our framework is the machinery necessary for a formal
way of talking about the relative ability of PKR formalisms to compactly
represent information. In particular, we were able to formalize the intuition
that a specific PKR formalism provides "one of the most compact ways to represent
models/theorems" among the PKR formalisms of a specific class.

In our opinion, the proposed framework improves over the state of the art
in two different aspects:

1. All the proofs presented in the previous papers only compare pairs of
PKR formalisms, for example propositional circumscription and Propositional
Logic (Cadoli et al., 1997). These results do not allow for a precise classification
of the level of

27

Cadoli, Donini, Liberatore, & Schaerf compactness of the considered formalisms.
Rephrasing and adapting these results in our framework allows us to infer
that circumscription is model-coNP-complete and thm-Pi p2-complete. As a
consequence, we also have that it is more space-efficient of the WIDTIO belief
revision formalism in representing sets of models or sets of theorems.

2. Using the proposed framework it is now possible to find criteria for adapting
existent

polynomial reductions showing C-hardness into reductions that show model-C
or thmC-hardness, where C is a class in the polynomial hierarchy (Liberatore,
1998).

Acknowledgments This paper is an extended and revised version of a paper
by the same authors appeared in the proceedings of the fifth international
conference on the principles of knowledge representation and reasoning (KR'96)
(Cadoli, Donini, Liberatore, & Schaerf, 1996a). Partial supported has been
given by ASI (Italian Space Agency) and CNR (National Research Council of
Italy).

References Ben-Eliyahu, R., & Dechter, R. (1991). Default logic, propositional
logic and constraints.

In Proceedings of the Ninth National Conference on Artificial Intelligence
(AAAI'91), pp. 379-385.

Ben-Eliyahu, R., & Dechter, R. (1994). Propositional semantics for disjunctive
logic programs. Annals of Mathematics and Artificial Intelligence, 12, 53-87.

Boppana, R., & Sipser, M. (1990). The complexity of finite functions. In
van Leeuwen,

J. (Ed.), Handbook of Theoretical Computer Science, Vol. A, chap. 14, pp.
757-804. Elsevier Science Publishers (North-Holland), Amsterdam.

Cadoli, M. (1992). The complexity of model checking for circumscriptive formulae.
Information Processing Letters, 44, 113-118.

Cadoli, M., Donini, F., Liberatore, P., & Schaerf, M. (1996a). Comparing
space efficiency

of propositional knowledge representation formalisms. In Proceedings of the
Fifth International Conference on the Principles of Knowledge Representation
and Reasoning (KR'96), pp. 364-373.

Cadoli, M., Donini, F. M., Liberatore, P., & Schaerf, M. (1996b). Feasibility
and unfeasibility of off-line processing. In Proceedings of the Fourth Israeli
Symposium on Theory of Computing and Systems (ISTCS'96), pp. 100-109. IEEE
Computer Society Press. url = ftp://ftp.dis.uniroma1.it/PUB/AI/papers/cado-etal-96.ps.gz.

Cadoli, M., Donini, F. M., Liberatore, P., & Schaerf, M. (1997). Preprocessing
of intractable problems. Tech. rep. DIS 24-97, Dipartimento di Informatica
e Sistemistica, Universit`a di Roma "La Sapienza". url = http://ftp.dis.uniroma1.it/PUB/AI/papers/cado-etal-97-d-REVISED.ps.gz.

28

Space Efficiency of Propositional Knowledge Representation Formalisms Cadoli,
M., Donini, F. M., Liberatore, P., & Schaerf, M. (1999). The size of a revised

knowledge base. Artificial Intelligence, 115 (1), 25-64.

Cadoli, M., Donini, F. M., & Schaerf, M. (1995). On compact representations
of propositional circumscription. In Proceedings of the Twelfth Symposium
on Theoretical Aspects of Computer Science (STACS'95), pp. 205-216. Extended
version as RAP.14.95 DIS, Univ. of Roma "La Sapienza", July 1995.

Cadoli, M., Donini, F. M., & Schaerf, M. (1996). Is intractability of non-monotonic
reasoning

a real drawback?. Artificial Intelligence, 88 (1-2), 215-251.

Cadoli, M., Donini, F. M., Schaerf, M., & Silvestri, R. (1997). On compact
representations

of propositional circumscription. Theoretical Computer Science, 182, 183-202.

Cook, S. A. (1971). The complexity of theorem-proving procedures. In Proceedings
of the

Third ACM Symposium on Theory of Computing (STOC'71), pp. 151-158.

Eiter, T., & Gottlob, G. (1992). On the complexity of propositional knowledge
base revision,

updates and counterfactuals. Artificial Intelligence, 57, 227-270.

Eiter, T., & Gottlob, G. (1993). Propositional circumscription and extended
closed world

reasoning are Pi p2-complete. Theoretical Computer Science, 114, 231-245.

Etherington, D. V. (1987). Reasoning with incomplete information. Morgan
Kaufmann,

Los Altos, Los Altos, CA.

Fagin, R., Ullman, J. D., & Vardi, M. Y. (1983). On the semantics of updates
in databases.

In Proceedings of the Second ACM SIGACT SIGMOD Symposium on Principles of
Database Systems (PODS'83), pp. 352-365.

Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability: A Guide
to the

Theory of NP-Completeness. W.H. Freeman and Company, San Francisco, Ca.

Gelfond, M., & Lifschitz, V. (1988). The stable model semantics for logic
programming.

In Proceedings of the Fifth Logic Programming Symposium, pp. 1070-1080. The
MIT Press.

Gelfond, M., Przymusinska, H., & Przymusinsky, T. (1989). On the relationship
between

circumscription and negation as failure. Artificial Intelligence, 38, 49-73.

Ginsberg, M. L. (1986). Conterfactuals. Artificial Intelligence, 30, 35-79.
Gogic, G., Kautz, H. A., Papadimitriou, C., & Selman, B. (1995). The comparative
linguistics of knowledge representation. In Proceedings of the Fourteenth
International Joint Conference on Artificial Intelligence (IJCAI'95), pp.
862-869.

Gottlob, G. (1992). Complexity results for nonmonotonic logics. Journal of
Logic and

Computation, 2, 397-425.

Gottlob, G. (1995). Translating default logic into standard autoepistemic
logic. Journal of

the ACM, 42, 711-740.

29

Cadoli, Donini, Liberatore, & Schaerf Imielinski, T. (1987). Results on translating
defaults to circumscription. Artificial Intelligence, 32, 131-146.

Janhunen, T. (1998). On the intertranslatability of autoepistemic, default
and priority

logics, and parallel circumscription. In Proceedings of the Sixth European
Workshop on Logics in Artificial Intelligence (JELIA'98), No. 1489 in Lecture
Notes in Artificial Intelligence, pp. 216-232. Springer-Verlag.

Johnson, D. S. (1990). A catalog of complexity classes. In van Leeuwen, J.
(Ed.), Handbook of Theoretical Computer Science, Vol. A, chap. 2, pp. 67-161.
Elsevier Science Publishers (North-Holland), Amsterdam.

Karp, R. M., & Lipton, R. J. (1980). Some connections between non-uniform
and uniform

complexity classes. In Proceedings of the Twelfth ACM Symposium on Theory
of Computing (STOC'80), pp. 302-309.

Kautz, H. A., Kearns, M. J., & Selman, B. (1995). Horn approximations of
empirical data.

Artificial Intelligence, 74, 129-145.

Kautz, H. A., & Selman, B. (1991). Hard problems for simple default logics.
Artificial

Intelligence, 49, 243-279.

Kautz, H. A., & Selman, B. (1992). Forming concepts for fast inference. In
Proceedings of

the Tenth National Conference on Artificial Intelligence (AAAI'92), pp. 786-793.

Khardon, R., & Roth, D. (1996). Reasoning with models. Artificial Intelligence,
87, 187-

213.

Khardon, R., & Roth, D. (1997). Defaults and relevance in model-based reasoning.
Artificial

Intelligence, 97, 169-193.

K"obler, J., & Watanabe, O. (1998). New collapse consequences of NP having
small circuits.

SIAM Journal on Computing, 28 (1), 311-324.

Kolaitis, P. G., & Papadimitriou, C. H. (1990). Some computational aspects
of circumscription. Journal of the ACM, 37 (1), 1-14.

Liberatore, P. (1995). Compact representation of revision of Horn clauses.
In Yao, X. (Ed.),

Proceedings of the Eighth Australian Joint Artificial Intelligence Conference
(AI'95), pp. 347-354. World Scientific.

Liberatore, P. (1998). Compilation of intractable problems and its application
to Artificial

Intelligence. Ph.D. thesis, Dipartimento di Informatica e Sistemistica, Universit`a
di Roma "La Sapienza". URL = ftp://ftp.dis.uniroma1.it/pub/AI/papers/libe-98-c.ps.gz.

Liberatore, P., & Schaerf, M. (1996). The complexity of model checking for
belief revision and update. In Proceedings of the Thirteenth National Conference
on Artificial Intelligence (AAAI'96), pp. 556-561.

30

Space Efficiency of Propositional Knowledge Representation Formalisms Liberatore,
P., & Schaerf, M. (1998). The complexity of model checking for propositional

default logics. In Proceedings of the Thirteenth European Conference on Artificial
Intelligence (ECAI'98), pp. 18-22.

Liberatore, P., & Schaerf, M. (2000). The compactness of belief revision
and update operators. Tech. rep., Dipartimento di Informatica e Sistemistica,
Universit`a di Roma "La Sapienza".

Marek, W., & Truszczy'nski, M. (1991). Autoepistemic logic. Journal of the
ACM, 38 (3),

588-619.

McCarthy, J. (1980). Circumscription - A form of non-monotonic reasoning.
Artificial

Intelligence, 13, 27-39.

Minker, J. (1982). On indefinite databases and the closed world assumption.
In Proceedings

of the Sixth International Conference on Automated Deduction (CADE'82), pp.
292- 308.

Moses, Y., & Tennenholtz, M. (1996). Off-line reasoning for on-line efficiency:
knowledge

bases. Artificial Intelligence, 83, 229-239.

Nebel, B. (1998). How hard is it to revise a belief base?. In Dubois, D.,
& Prade, H. (Eds.),

Belief Change - Handbook of Defeasible Reasoning and Uncertainty Management
Systems, Vol. 3. Kluwer Academic.

Reiter, R. (1980). A logic for default reasoning. Artificial Intelligence,
13, 81-132. Schlipf, J. S. (1987). Decidability and definability with circumscription.
Annals of Pure

and Applied Logic, 35, 173-191.

Schlipf, J. S. (1995). A survey of complexity and undecidability results
for logic programming. Annals of Mathematics and Artificial Intelligence,
15, 257-288.

Selman, B., & Kautz, H. A. (1996). Knowledge compilation and theory approximation.

Journal of the ACM, 43, 193-224.

Stockmeyer, L. J. (1976). The polynomial-time hierarchy. Theoretical Computer
Science,

3, 1-22.

Winslett, M. (1989). Sometimes updates are circumscription. In Proceedings
of the Eleventh

International Joint Conference on Artificial Intelligence (IJCAI'89), pp.
859-863.

Winslett, M. (1990). Updating Logical Databases. Cambridge University Press.
Yap, C. K. (1983). Some consequences of non-uniform conditions on uniform
classes. Theoretical Computer Science, 26, 287-300.

31