%% Searched string: {}
%\documentstyle[11pt,proof,inputfiles]{article}
%\documentstyle[11pt]{article}
\documentstyle[theapa,11pt,jair]{article}

%\textwidth 6in
%\textheight 8.15in
%\oddsidemargin 0pt

\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{assumption}{Assumption}
\newtheorem{definition}{Definition}
\newtheorem{question}{Question}
\newtheorem{example}{Example}

\let\shortcite=\xxx

%%%%%%%%%%%%% macros %%%%%%%%%%%%%%
\def\nota#1{{\marginpar{\tiny #1}}}
\def\defn{\stackrel{\bf .}{=}}

%\expandafter\ifx\csname shortcite\endcsname\relax
%\let\shortcite=\cite
%\fi

\def\riga{\vskip 1\baselineskip \noindent}

\def\ie{i.e.,}

\def\wrt{w.r.t.\ }

\def\eg{e.g.,}

\def\cf{cf.\ }
\def\imply{\rightarrow}
\def\ginsberg{*_{G}}

%\def\eg{{\mbox{\rm e.g.\ }}}

\def\RE{{\mbox{\rm r.e.}}}

\def\piano-di-studi{{\mbox{\it curriculum\/}}}
\def\piani-di-studio{{\mbox{\it curricula\/}}}

\newcommand{\pUno}{{\tt Data\-Bases}}
\newcommand{\pDue}{{\tt Algebra}}
\newcommand{\pTre}{{\tt Non\-Mo\-no\-to\-nicRea\-so\-ning}}
\newcommand{\pQuattro}{{\tt Ma\-the\-ma\-ti\-cal\-Lo\-gic}}
\newcommand{\pCinque}{{\tt Com\-pu\-terArchi\-tectures}}
\newcommand{\zUno}{{\tt Reaso\-ning\-About\-Knowledge}}
\newcommand{\zDue}{{\tt Compu\-tational\-Comp\-lexity}}

%\newtheorem{theorem}{Theorem}


\newcommand{\nop}[1]{}

%%% example environment in standard style
%%

\newcounter{rmexample}

\newenvironment{rmexample}
{\addtocounter{rmexample}{1}
\medskip
\noindent{\bf Example~\thermexample}:}{\ifhmode\nobreak{\raisebox{-.2ex}{$\Diamond$}}\par\fi\smallskip}

\def\proof{\noindent {\sl Proof.\ \ }}
\def\proofsketch{\noindent {\sl Proof (sketch).\ \ }}

\def\qed{\hfill{\boxit{}}
  \ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi}
\long\def\boxit#1{\vbox{\hrule\hbox{\vrule\kern3pt
                  \vbox{\kern3pt#1\kern3pt}\kern3pt\vrule}\hrule}}

\def\ovl#1{\overline{#1}}


%%% Le macros servono o per accorciare il testo, o per riscrivere simboli che
%%% non ci piacciono... 

%%% Macros che definiscono classi di compplessita'

\def\P{{\rm P}}
\def\Pone{{\rm coNP}}
\def\Ptwo{$\Pi^p_2$}
\def\Pthree{$\Pi^p_3$}
\def\Sone{{\rm NP}}
\def\Stwo{$\Sigma^p_2$}
\def\Sthree{$\Sigma^p_3$}
\def\Dtwo{$\Delta^p_2$}
\def\Dthree{$\Delta^p_3$}
\def\NP{{\rm NP}}
\def\NC{\mbox{{\rm NC}$^1$}}
\def\coNP{{\rm coNP}}
\def\poly{{\rm poly}}
\def\PH{{\rm PH}}

%%% Macros che definiscono problemi

\def\unsat{{\sc unsat}}
\def\threesat{{\sc 3sat}}
\def\threeunsat{{\sc 3unsat}}
\def\threecnf{{\sc 3cnf}}
\def\PLI{{\sc pli}}

\def\FI{{\sc fi}}
\def\CI{{\sc ci}}
\def\LI{{\sc li}}
\def\kCI{{\sc $k$-ci}}
\def\CMI{{\sc cmi}}
\def\ConjI{{\sc conj-i}}
\def\CHR{{\sc chr}}
\def\GMC{{\sc gmc}}
\def\GI{{\sc gi}}
\def\csat{{\sc c-sat}}
\def\sat{{\sc sat}}
\def\constVC{{\sc c-vc}}
\def\mmc{{\sc mmc}}
\def\epssat{$\epsilon$\threesat}


\def\dd#1#2{#1_1,\ldots,#1_{#2}}
       %"\dd x n" makes "x_1,...,x_n"
\def\ddtre#1#2#3{#1_1#2 \cdots#2 #1_{#3}}
       %"\ddtre x \wedge n" makes "x_1 \wedge ... \wedge x_n"

\def\false{{\sf false}}            
\def\true{{\sf true}}            
\def\AEQBF{$\forall\exists$-QBF}
\def\M{{\cal M}}                     % set of models for...
\def\fixed{\Sigma}                   % fixed part (X-or formulae)
\def\ovl#1{\overline{#1}}
\def\ext{{\cal E}}                   % extension
\def\extone#1{{\cal E}_#1}           % extension with index

% Macros per le classi di compilabilit\'a

\def\C{{\rm C}}

\def\comp{\mbox{$\leadsto$}}
\def\cC{\comp{\rm C}}
\def\cP{\comp{\rm P}}
\def\cNP{\comp{\rm NP}}
\def\ccoNP{\comp{\rm coNP}}
\def\cS#1{\comp$\Sigma^p_{#1}$}
\def\cPi#1{\comp$\Pi^p_{#1}$}

\def\nucomp{\mbox{$\parallel\!\leadsto$}}
\def\nucC{\nucomp{\rm C}}
\def\nucP{\nucomp{\rm P}}
\def\nucNP{\nucomp{\rm NP}}
\def\nuccoNP{\nucomp{\rm coNP}}
\def\nucS#1{\nucomp$\Sigma^p_{#1}$}
\def\nucPi#1{\nucomp$\Pi^p_{#1}$}

\def\leqcomp{\leq_{comp}}
\def\leqnucomp{\leq_{nu-comp}}

\def\GCWA{{\sl GCWA}}
\def\HR{{\sl HR}}

% Macros di Francesco per la parte su non-compilabilita'

\newcommand{\pair}[2]{\langle #1, #2 \rangle}
\newcommand{\deftheory}[2]{\langle #1, #2 \rangle}
% Comando per un default PF normale
\def\defaultone#1{\frac{~:#1}{#1}}

% Comando per un default normale
\def\defaulttwo#1#2{\frac{#1:#2}{#2}}

% Comando per un default qualsiasi
\def\defaultthree#1#2#3{\frac{#1:#2}{#3}}

% Macros di Marco S. per l'articolo KR

\def\mC{{\rm model-C}}                 % Model checking e' C
\def\mP{{\rm model-P}}                 % Model checking e' P
\def\mNP{{\rm model-NP}}               % Model checking e' NP
\def\mcoNP{{\rm model-coNP}}           % Model checking e' coNP
\def\mS#1{{\rm model-}$\Sigma^p_{#1}$}
\def\mPi#1{{\rm model-}$\Pi^p_{#1}$}

\def\tC{{\rm thm-C}}                 % Inference e' C
\def\tP{{\rm thm-P}}                 % Inference e' P
\def\tNP{{\rm thm-NP}}               % Inference e' NP
\def\tcoNP{{\rm thm-coNP}}           % Inference e' coNP
\def\tS#1{{\rm thm-}$\Sigma^p_{#1}$}
\def\tPi#1{{\rm thm-}$\Pi^p_{#1}$}

\def\diventa{\mapsto}                % Simbolo del mapping tra formalismi

\def\PL{{\rm PL}}
%%%%%%%%%%%%%% altre macros

%\def\true{\mbox{true}}
%\def\false{\mbox{false}}
%\def\dd#1#2{#1_1,\ldots,#1_{#2}}                                                               %da da, makes x_1,...,x_n
\def\set#1{\{#1\}}
\def\Onlyif{{\em Only-if part.\/}}  %---> of iff-proof
\def\If{{\em If part.\/}}           %<--- of iff-proof

%%%%%%%%%%%%%%%%%


\def\SM{\textsc{sm}}
\def\kernel{\textsc{kernel}}
\def\prologif{~:\!\!-~}





% Local Variables: 
% mode: latex
% TeX-master: t
% End: 


\begin{document}

%%%%%%%%%%%%% title %%%%%%%%%%%%%%
\jairheading{13}{2000}{1-31}{8/99}{8/00}
\ShortHeadings{Space Efficiency of Propositional Knowledge Representation Formalisms}
{Cadoli, Donini, Liberatore, \& Schaerf}
\firstpageno{1}


\title{Space Efficiency of Propositional Knowledge Representation
Formalisms}


\author{%
\name Marco Cadoli \email cadoli@dis.uniroma1.it \\
\addr Dipartimento di Informatica e Sistemistica \\
      Universit{\`a} di Roma ``La Sapienza'' \\
      Via Salaria 113, I-00198, Roma, Italy
\AND
\name Francesco M.\  Donini \email donini@dis.uniroma1.it\\
\addr Politecnico di Bari \\
      Dipartimento di di Elettrotecnica ed Elettronica \\
      Via Orabona 4, I-70125, Bari, Italy
\AND
\name Paolo Liberatore \email liberato@dis.uniroma1.it \\
\name Marco Schaerf \email schaerf@dis.uniroma1.it \\
\addr Dipartimento di Informatica e Sistemistica \\ 
      Universit{\`a} di Roma ``La Sapienza'' \\
      Via Salaria 113, I-00198, Roma, Italy
}

\maketitle

\begin{abstract}
  
  We investigate the {\em space efficiency\/} of a Propositional
  Knowledge Representation (PKR) formalism. Intuitively, the space
  efficiency of a formalism $F$ in representing a certain piece of
  knowledge $\alpha$, is the size of the shortest formula of $F$ that
  represents $\alpha$. 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.

\end{abstract}

%\begin{center}
%{\bf Topic Area}\\
%Reasoning Techniques: Efficiency Measures and Complexity
%\end{center}

% Local Variables: 
% mode: latex
% TeX-master: "main"
% End: 


%\newpage
%\tableofcontents

%%%%%%%%%%%%% introduction %%%%%%%%%%%%%%
\section{Introduction}
\label{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 {\em 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 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 $\neg \neg monday$, as well as $monday \wedge (rain
\vee \neg 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 $\alpha$ is the size of the shortest formula of $F$ that
represents $\alpha$. Space efficiency ---also called {\em
 succinctness\/} or {\em 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.).

%We remark that PKR formalisms and Propositional Logic are not the
%same.  Indeed, Propositional Logic is a particular propositional
%formalism, but many other ones exist (for example, default logic,
%circumscription, logic programming, 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.

%and which one we assume unplausible. As a result, there are
%two possible way to see a given piece of knowledge. The first one is
%by assuming that it represents all possible facts we can infer from
%what is known. The second one is by assuming that it represents all
%possible states of the world that are consistent with the available
%information we have.

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.

\def\sandwich{\mbox{sandwich}}
\def\salad{\mbox{salad}}
\def\water{\mbox{water}}
\def\coke{\mbox{coke}}

\begin{example}
\label{first:example:intro}
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.

\begin{eqnarray*}
  C &=&
(\sandwich \vee \salad) \wedge (\neg \sandwich \vee \neg \salad)
\wedge (\sandwich \rightarrow \neg \salad)
  \wedge \\
&&(\water \vee \coke) \wedge (\neg \water \vee \neg \coke)
\wedge
(\neg \coke \rightarrow water)
\end{eqnarray*}

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

\[
  F = (\sandwich \vee \salad) \wedge (\neg \sandwich \vee \neg \salad)
  \wedge (\water \vee \coke) \wedge (\neg \water \vee \neg \coke)
\]

More formally, $F$ represents the set of models $A$, because
for each interpretation $I$, $I \in A$ holds if and only if $I \models
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.

\end{example}


\subsection{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~\citeyear{bene-dech-91,bene-dech-94}
proposed a translation from default logic to PL, and a translation
from disjunctive logic programs to PL, while Winslett~\citeyear{wins-89}
introduced a translation from revised knowledge bases to PL, and
Gelfond, Przymusinska, and Przymusinskyi~\citeyear{gelf-przy-przy-89}
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
\citeyear{cado-doni-scha-96} have shown that many interesting
fragments of default logic and circumscription cannot be expressed by
polynomial-time 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 \cite{cado-etal-97-c} and most operators
for belief revision into PL \cite{cado-etal-99,libe-95}.

Gogic and collegues~\citeyear{gogi-etal-95}
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 \citeyear{kaut-kear-selm-95} and Khardon and Roth
\citeyear{khar-roth-96,khar-roth-97} considered representations of knowledge
bases based on the notion of {\em 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
\cite{cado-etal-96}, a new complexity measure for decision problems,
called {\em compilability}, has been introduced. In the 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.

\subsection{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 {\em 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, \eg\ 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.

\begin{example}

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 \vee \salad) \wedge (\neg \sandwich \vee \neg \salad)
  \wedge (\water \vee \coke) \wedge (\neg \water \vee \neg \coke)
\]

The set of models of this formula is $A$, and the models of $A$ are
exactly the minimal models of the formula $F_c$ defined as follows.

\[
  F_c = (\sandwich \vee \salad) \wedge (\water \vee \coke)
\]

By the definition of circumscription \cite{mcca-80} it holds that $F$
is equivalent to
$CIRC(F_c;\{\sandwich,\salad,\water,\coke\},\emptyset,\emptyset)$. Note
that $F_c$ 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.

\end{example}

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.


\subsection{Results}

We introduce two new compactness measures ({\em model\/} and {\em
 theorem compactness\/}) and the corresponding classes (\mC\ and \tC,
where C is a complexity class like \P, \NP, \coNP, etc.). Such classes
form two hierarchies that are isomorphic to the polynomial-time
hierarchy \cite{stoc-76}. We show that the relative space efficiency
of a PKR formalism is 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.

\subsection{Outline}

In the next section we introduce the notation and the assumptions that
we adopt in this work. In Section~\ref{compilability}~(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 \cite{cado-etal-96}. In
Section~\ref{reductions}~(Reductions) we describe the constraints we
impose on reductions, while in Section~\ref{succinctness}~(Space
Efficiency) we introduce our compactness classes.
%Section~\ref{pkr}~(Propositional Knowledge Representation) we give the
%basic definitions and assumptions about PKR formalisms, we propose two
%general definitions about translations between formalisms, and show
%how compilability classes can be used to compare the space efficiency
%of PKR formalisms.
In Section~\ref{applications}~(Applications) we actually compare many
known PKR formalisms using our framework.  Finally, in
Section~\ref{conclusions}~(Related Work and Conclusions) we compare
our work with other proposals presented in the literature and draw some
conclusions.



% Local Variables: 
% mode: latex
% TeX-master: "main"
% End: 

%%%%%%%%%%%%% notation-pkr %%%%%%%%%%%%%%
\section{Notations and Assumptions}
\label{pkr}

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:

\begin{enumerate}

\item a {\em syntax}, which is used to define the well-formed
formulae;

\item a {\em proof theory}, which allows for saying when a
formula follows from another one; and

\item a {\em model-theoretic semantics}, which establishes
when a model satisfies a formula.

\end{enumerate}

The syntax is defined from a finite alphabet of propositional
symbols $L=\{a,b,c,\ldots\}$, possibly with subscripts, and the
usual set of propositional connectives $\wedge$, $\vee$, $\neg$.

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

In some cases, we want knowledge bases to represent models
rather than sets of formulas. An {\em interpretation\/} for
an alphabet of propositional variables $L$ is a mapping from
$L$ in $\{\true, \false \}$. The {\em 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 $\frac{~~:~~}{~~~}$
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 well-formed formula, according
to the syntax of the formalism.

Each formalism has its own proof theory as well.
The proof theory of a formalism $F$ is a binary
relation $\vdash_F$ on the set of knowledge bases and formulae.
Intuitively, $FB \vdash_F \phi$ means that $\phi$ is a consequence
of the knowledge base $KB$, according to the rules of the
formalism $F$. As a result, the set of formulae $\phi$ 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 \vdash_F \phi$, we assume that
$KB$ is a knowledge base in the syntax of $F$, while $\phi$ is
a propositional formula.

This allows for saying that two knowledge bases $KB_1$ and
$KB_2$, expressed in two different formalisms $F_1$ and $F_2$,
represent the same piece of knowledge: this is true when,
for any propositional formula $\phi$ it holds
$KB_1 \vdash_{F_1} \phi$ if and only if
$KB_2 \vdash_{F_2} \phi$.

The {\em model-theoreric semantics of a formalism} is a relation
$\models_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 \models_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~\cite{reit-80}, 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 \vdash_F \phi
\mbox{ ~~ iff ~~ }
\forall I ~.~ I \models KB \mbox{ implies } I \models \phi
\]

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

\begin{assumption}
\label{size-query}

We consider only formulae whose size is less than or
equal to that of the knowledge base.

\end{assumption}

All formalisms we consider satisfy the right-hand side
distruibutivity of conjunction, that is,
$KB \vdash_F \phi \wedge \mu$
if and only if $KB \vdash_F \phi$ and $KB \vdash_F \mu$.
The assumption on the size of $\phi$ is not restrictive in
this case, if $\phi$ is a CNF formula.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 

%%%%%%%%%%%%% compilability %%%%%%%%%%%%%%
\section{Compilability Classes}
\label{compilability}

We assume the reader is familiar with basic complexity classes, such
as \P, \NP\ and (uniform) classes of the polynomial hierarchy
\cite{stoc-76,gare-john-79}.  Here we just briefly introduce
non-uniform classes \cite{john-90}. In the
sequel, \C, $\C'$, 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 $\epsilon$ the empty string and
assume that the alphabet $\Sigma$ contains a special symbol $\#$ to
denote blanks. The {\em length} of a string $x \in \Sigma^*$ is
denoted by $|x|$.

\begin{definition}

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

\end{definition}

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.

\begin{definition}

An {\em 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.

\end{definition}

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 {\em size} of the input,
not of the input itself. Hence, advice-taking Turing machines are
closely related to non-uniform families of circuits
\cite{bopp-sips-90}. 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.

\begin{definition}
  
An advice-taking Turing machine uses {\em polynomial advice} if
there exists a polynomial $p$ such that the advice oracle $A$
satisfies $|A(n)| \leq p(n)$ for any nonnegative integers $n$.

\end{definition}

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.

\begin{definition}

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.

\end{definition}

Any class C/poly is also known as {\em 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
\citeyear{karp-lipt-80} proved that if \Sone\ $\subseteq$~\P/poly
then $\Pi^p_2 = \Sigma^p_2 =$ PH, \ie\ the polynomial hierarchy
collapses at the second level, while Yap \citeyear{yap-83}
generalized their results, in particular by showing that if \Sone\ 
$\subseteq$~\Pone/poly then $\Pi^p_3 = \Sigma^p_3 =$ PH, \ie\ the
polynomial hierarchy collapses at the third level. An inprovement of
this results has been given by K\"obler and Watanabe
\citeyear{kobl-wata-98}: they proved that $\Pi^p_k \subseteq
\Sigma^p_{k}/\poly$ implies that the polynomial hierarchy collapses to
ZPP($\Sigma^p_{k+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 \cite{cado-etal-96}, 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 {\em 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
\cite{kaut-selm-92-a,kaut-kear-selm-95,khar-roth-97}. 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 {\em fixed} or {\em
 accessible off-line} (the knowledge base), and the second one is {\em
 varying}, or {\em accessible on-line} (the interpretation/formula).
Compilability aims at capturing the {\em 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 {\em poly-size} if there exists a polynomial
$p$ such that for all strings $x$ it holds $|f(x)| \leq p(|x|)$. An
exception to this definition is when $x$ represents a number: in this
case, we impose $|f(x)| \leq 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 {\em 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 {\em language of pairs} $S$ as a subset of $\Sigma^*
\times \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 = \{ \pair x y ~|~ 
x \mbox{ is a set of propositional formulae (the KB), }
y \mbox{ is a formula, and } x \vdash y \}
\]

% 
% While the problem {\sc Literal Inference}, is defined as	follows.%
% 
% \[ 
% \LI = \{	\pair x	y ~|~ 
% x \mbox{	is a {\sc cnf} propositional formula, }
% y \mbox{	is a literal, and }	x \vdash y \}
% \]
%
% It is well known that both \PLI\  and \LI\  are \coNP-complete, i.e., they are two
% of the ``hardest'' problems among those belonging to \coNP. Our goal is to
% prove that \CI\  is the ``hardest'' theorem-proving problem among those that can
% be solved by preprocessing in an arbitrary way the first input, i.e., the KB,
% while \LI\  can be solved in polynomial time after a preprocessing of the KB.

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'' theorem-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 {\em non-uniform compilability classes},
denoted as \nucC, where C is a generic uniform complexity class, such
as P, \NP, \coNP, or \Stwo.

\begin{definition}[\nucC\  classes]

A language of pairs $S \subseteq \Sigma^* \times \Sigma^*$ belongs to \nucC\
iff there exists a binary poly-size function $f$ and a language of pairs $S'
\in \C$ such that for all $\pair x y \in S$ it holds:

\[
\pair {f(x,|y|)} y \in S' \mbox{ iff } \pair x y \in S
\]

\end{definition}

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 \cite{cado-etal-96}. 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.

\begin{theorem}{\bf \protect{\cite[Theorem~6]{cado-etal-97-d}}}
\label{upper-bound}
  Let $C$ be a class in the polynomial hierarchy and $S \subseteq
  \Sigma^* \times \Sigma^*$.  A problem $S$ belongs to \nucC\ if and
  only if there exists a poly-size function $f$ and a language of
  pairs $S'$, such that for all ${\pair x y}\in \Sigma^* \times
  \Sigma^*$ it holds that:
  %
  \begin{enumerate}
    \item for all $y$ such that $|y| \le k$, 
    ${\pair {f(x,k)} y } \in S'$ if and only if ${\pair x y } \in S$;

    \item $S' \in$ \C.
  \end{enumerate}
\end{theorem}

Clearly, any problem whose time complexity is in \C\ is also in \nucC:
just take $f(x,|y|)=x$ and $S'=S$.  What is interesting is that some
problem in \C\ may belong to $\nucC'$ with $\C' \subset C$,
\eg, some problems in \NP\ are in \nucP. This is true for example
for some problems in belief revision \cite{cado-etal-99}. In the rest
of this paper, however, we mainly focus on ``complete'' problems,
defined below.
A pictorial representation of the class \nucC\ is in
Figure~\ref{defi-c-poli-ab}, where we assume that $S' \in C$.

%\nota{Dim che basta upper bound?}

% Using the above definition it is simple to show that the literal inference
% problem \LI\ is in \nucP.
% 
% \begin{proposition}
% 
% \LI\  is in \nucP.
% 
% \end{proposition}
% 
% In fact, given $x$ we (pre)compute once and for all the set of literals $T=\{y | x \vdash 
% y\}$ and record this set. At runtime, given the on-line
% part $y$, we decide whether $x \vdash y$ with the simple look-up $y  \in T$. Notice
% that $|T|=O(|x|)$, i.e., 
% the preprocessing phase generates an output of polynomial space (hence $f$
% is poly-size) and that we only need polynomial time on-line.
%However, for t
For the problem \PLI\ no method proving that it belongs to \nucP\ is
known. In order to show that it (probably) does not belong to \nucP,
we define a notion of reduction and completeness.

\begin{figure}
\begin{center}
  %%%%%%%%%%%%% figure/defi-c-poli-ab %%%%%%%%%%%%%%
{\setlength{\unitlength}{1mm}
\begin{picture}(62.25,24)
\put(19.12,11.26){$|y|$}

\put(14.99,12){\line(5,2){10}}
\put(24.99,16){\vector(3,1){0}}
\put(2.99,20){\line(1,0){22}}
\put(24.99,20){\vector(1,0){0}}
\put(9.5,11.27){$|~|$}

\put(6.99,8){\framebox(8,8){}}

\put(0.25,3.78){$y$}

\put(36.99,4){\line(-1,0){34}}
\put(36.99,4){\vector(1,0){0}}
\put(47.63,17.38){$\langle x,y \rangle \in S$}

\put(0.31,20.39){$x$}

\put(39.62,12.88){$S'$}

\put(28.15,17.28){$f$}

\put(54.99,14){\line(-1,0){10}}
\put(54.99,14){\vector(1,0){0}}
\put(36.99,20){\line(-1,0){4}}
\put(36.99,20){\vector(1,0){0}}
\put(36.99,0){\framebox(8,24){}}

\put(24.99,14){\framebox(8,8){}}

\put(10.99,8){\line(0,-1){4}}
\put(10.99,8){\vector(0,1){0}}
\end{picture}}

\caption{A representation of \nucC.}
\label{defi-c-poli-ab}
\end{center}
\end{figure}

\begin{definition}[Non-uniform comp-reducibility]
\label{non-uniform-reduction}

Given two problems $A$ and $B$,  $A$ is {\em non-uniformly comp-reducible\/}
to $B$ (denoted as $A \leqnucomp B$) iff there exist two poly-size binary
functions $f_1$ and $f_2$, and a polynomial-time binary function $g$ such that
for every pair ${\pair x y }$ it holds that ${\pair x y } \in A$ if and only if
${\pair {f_1(x,|y|)} {g(f_2(x,|y|),y)} } \in B$.

\end{definition}

The $\leqnucomp$ reductions can be represented as depicted in
Figure~\ref{defi-comp-ridu-ab}.%
%
\begin{figure}[ht]
\begin{center}
  %%%%%%%%%%%%% figure/defi-comp-ridu-ab %%%%%%%%%%%%%%
{\setlength{\unitlength}{1mm}
\begin{picture}(60.2,26)
\put(6.87,19.27){$|y|$}

\put(16.74,20){\line(0,-1){10}}

\put(16.74,10){\line(1,0){10}}
\put(26.74,10){\vector(1,0){0}}
\put(10.74,20){\line(1,0){16}}
\put(26.74,20){\vector(1,0){0}}
\put(10.74,16){\line(0,1){4}}

\put(10.74,2){\line(0,1){6}}
\put(10.74,8){\vector(0,1){0}}
\put(44.74,12){\line(-1,0){10}}

\put(9.25,11.27){$|~|$}

\put(6.74,8){\framebox(8,8){}}

\put(57.64,5.2){$y'$}

\put(44.74,12){\line(0,-1){4}}
\put(44.74,8){\vector(0,-1){0}}
\put(18.74,14){\line(1,0){8}}
\put(26.74,14){\vector(1,0){0}}
\put(18.74,24){\line(0,-1){10}}

\put(28.68,11.35){$f_2$}

\put(26.74,8){\framebox(8,8){}}

\put(0.45,2.18){$y$}

\put(40.74,2){\line(-1,0){38}}
\put(40.74,2){\vector(1,0){0}}
\put(57.64,22.94){$x'$}

\put(0.18,24.21){$x$}

\put(44.05,3.89){$g$}

\put(29.23,20.6){$f_1$}

\put(34.74,22){\line(1,0){22}}
\put(56.74,22){\vector(1,0){0}}
\put(56.74,4){\line(-1,0){8}}
\put(56.74,4){\vector(1,0){0}}
\put(26.74,24){\line(-1,0){24}}
\put(26.74,24){\vector(1,0){0}}
\put(40.74,0){\framebox(8,8){}}

\put(26.74,18){\framebox(8,8){}}

\end{picture}}

  \caption{The nu-comp-C reductions.}
  \label{defi-comp-ridu-ab}
\end{center}
\end{figure}
%
%
Such reductions satisfy all important properties of a reduction.

\begin{theorem}{\bf \protect{\cite[Theorem~5]{cado-etal-96}}}
\label{non-unif-red}
The reductions $\leqnucomp$ satisfy transitivity and are compatible
\cite{john-90} with the class \nucC\  for every complexity class~{\rm C}. 

\end{theorem}

Therefore, it is possible to define the notions of {\em hardness} and {\em
completeness\/} for \nucC\  for every complexity class C.

\begin{definition}[\nucC-completeness]
  Let $S$ be a language of pairs and {\rm C} a complexity class. $S$ is
  \nucC{\em -hard} iff for all problems $A \in$~\nucC\  we have that $A
  \leqnucomp S$. Moreover, $S$ is \nucC{\em -complete} if $S$ is in \nucC\  and
  is \nucC{\em -hard}.
\end{definition}

We now have the right complexity class to completely characterize the
problem \PLI. In fact \PLI\ is \nuccoNP-complete
\cite[Theorem~7]{cado-etal-96}.  Furthermore, the hierarchy formed by
the compilability classes is proper if and only if the polynomial
hierarchy is proper \cite{cado-etal-96,karp-lipt-80,yap-83} --- a fact
widely conjectured to be true.

Informally, we may say that \nucNP-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
\nuccoNP-hard problems. In general, a problem which is \nucC-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
\nucC\  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~\cite{mcca-80}.
Let $x$ be any propositional formula. The {\em minimal\/} models of
$x$ are the truth assignments satisfying $x$ having as
few positive values as possible (\wrt\  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 \cite{cado-92-b}.

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:%

\[
\mbox{\mmc} = \{ \langle x,y \rangle ~|~ \mbox{$y$ is a minimal model of $x$ } \}
\]

This problem can be shown to be \nuccoNP-complete
\cite[Theorem~13]{cado-etal-96}. Hence, it is very unlikely that it
can be in \nucP; that is, it is very unlikely that there exists some
off-line processing of the knowledge base, yielding (say) some data
structure $x'$, such that given $y$, it can now checked in polynomial
time whether $y$ is a minimal model of $x$. This, of course, unless
$x'$ has exponential size. This observation applies also when $x'$ is
a knowledge base in Propositional Logic, and led to the interpretation
that Circumscription is more compact, or succint, than PL
\cite{cado-doni-scha-95,gogi-etal-95}. Our framework allows to
generalize these results for all PKR formalisms, as shown in the
sequel.

% Local Variables: 
% mode: latex
% TeX-master: "main"
% End: 

%%%%%%%%%%%%% reductions %%%%%%%%%%%%%%
\section{Reductions among KR Formalisms}
\label{reductions}

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 $F_1$ and $F_2$ be two PKR formalisms. There exists a {\em poly-size
reduction} from $F_1$ to $F_2$, denoted as $f:F_1 \diventa F_2$, if $f$ is a
poly-size function such that for any given knowledge base $KB$ in $F_1$,
$f(KB)$ is a knowledge base in $F_2$.
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~\citeyear{gogi-etal-95} 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 $F_1$ is translated
into a knowledge base $KB'$ of the formalism $F_2$, 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 $F$
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 $KB$ is $\emptyset$,
while any model of any consistent knowledge base of the modified
propositional calculus contains $x_1$.

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 $g_{KB}$ from models of $KB$ to models of $f(KB)$.  We
stress that, to be as general as possible, the translation may depend
on $KB$ --- \ie\ 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 $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 $g_{KB}$ is a
\emph{circuit} of polynomial-size wrt $KB$.  We still use a
functional notation $g_{KB}(M)$ to denote the result of applying a
model $M$ to the circuit $g_{KB}$.  A formal definition follows.

% Hence, a reduction  preserving models is a poly-size function $f$ for
% translating knowledge bases such that there exists a polynomial $p$
% such that, for any knowledge base $KB$, there exists a circuit
% $g_{KB}$ whose size is bounded by $p(|KB|)$, and such that $M
% \models_{F_1} KB$ if and only if $M \models_{F_2} KB'$, where
% $KB'=f(KB)$.

\begin{definition}[Model Preservation]
\label{model-def}
A poly-size reduction $f:F_1 \diventa F_2$ satisfies {\em
 model-preservation} if there exists a polynomial $p$ such that, for each
 knowledge base $KB$ in $F_1$ there exists a circuit $g_{KB}$ whose
 size is bounded by $p(|KB|)$, and such that for every interpretation $M$
 of the variables of $KB$ it holds that $M \models_{F_1} KB$ iff
 $g_{KB}(M) \models_{F_2} f(KB)$.
\end{definition}


% \begin{definition}[Model Preservation]
% \label{model-def}
% 
% A poly-size reduction $f:F_1 \diventa F_2$ satisfies {\em model-preservation}
% if for each knowledge base $KB$ in $F_1$ there exists a poly-time binary
% function $g$ such that for every interpretation $M$ of the variables of $KB$ it
% holds that $M \models_{F_1} KB$ iff $g(KB,M) \models_{F_2} f(KB)$.
% 
% \end{definition}

The rationale of model-preserving reduction is that the knowledge base $KB$ of
the first formalism $F_1$ can be converted into a knowledge base $f(KB)$ in the
second one $F_2$, and this reduction should be such that
%
%the represented sets of models are more or less the same, that is,
%
each model $M$ in $F_1$ can be
easily translated into a model $g_{KB}(M)$ in $F_2$.

% We require $g_{KB}$ to be
% a circuit of polynomial size wrt $KB$; computable in polynomial time; if $g$ were
% more powerful --- \eg\ computable in nondeterministic polynomial time
% ---, it could hide the complexity of the target formalism $F_{2}$. 
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 model-preserving translation.

\noindent
%{\bf Example} We reduce a fragment of skeptical default logic to
%circumscription with varying letters, using the transformation shown in
%\cite{ethe-87-a}.  Let $\deftheory{D}{W}$ be a {\em prerequisite-free
%  normal\/} (PFN) default theory, i.e., all defaults are of the form
%$\defaultone{\gamma}$, where $\gamma$ is a generic formula. Let $Z$ be the
%set of letters occurring in $\deftheory{D}{W}$. Define $P_D$ as the set of
%letters $\{a_\gamma | \defaultone{\gamma} \in D\}$. The function $f$ can be
%defined in the following way: $f(\deftheory{D}{W}) = CIRC(T;P_D;Z)$, where
%$T = W \cup \{ a_\gamma \equiv \neg \gamma | a_\gamma \in P_D\}$, $P_D$ are
%the letters to be minimized, and $Z$ (the set of letters occurring in
%$\deftheory{D}{W}$) are varying letters. We show that $f$ is a
%model-preserving poly-size reduction. In fact, given a set of PFN defaults
%$D$ let $g_D$ be a function such that for each interpretation $M$ for $Z$,
%$g_D(M) = M \cup \{a_\gamma \in P_D | M\models \neg\gamma\}$.  Clearly, $f$
%is poly-size, $g_D$ is poly-time, and $M$ is a model of at least one
%extension of $\deftheory{D}{W}$ iff $g_D(M) \models CIRC(T;P_D;Z)$. The
%subscript $D$ of $g_D$ stresses the fact that the function $g_D$ does not
%depend in this case on the whole knowledge base $\deftheory{D}{W}$, but
%just on $D$.

\begin{example}
\label{reduction-skeptical-default}

We reduce a fragment of skeptical default logic \cite{kaut-selm-91-a} to 
circumscription with varying letters, using the transformation 
introduced by Etherington \citeyear{ethe-87-a}.  Let 
$\deftheory{D}{W}$ be a {\em prerequisite-free normal\/} (PFN) default 
theory, \ie\ all defaults are of the form $\defaultone{\gamma}$, where
$\gamma$ is a generic formula.  Let $Z$ be the set of letters
occurring in $\deftheory{D}{W}$.  Define $P_D$ as the set of letters
$\{a_\gamma | \defaultone{\gamma} \in D\}$.  The function $f$ can be
defined in the following way: $f(\deftheory{D}{W}) = CIRC(T;P_D;Z)$,
where $T = W \cup \{ a_\gamma \equiv \neg \gamma | a_\gamma \in
P_D\}$, $P_D$ are the letters to be minimized, and $Z$ (the set of
letters occurring in $\deftheory{D}{W}$) are varying letters.  We show
that $f$ is a model-preserving poly-size reduction.  In fact, given a
set of PFN defaults $D$ let $g_{D}$ be a function such that for each
interpretation $M$ for $Z$, $g_{D}(M) = M \cup \{a_\gamma \in P_D |
M\models \neg\gamma\}$.  Clearly, $f$ is poly-size, $g_{D}$ can be
realized by a circuit whose size is polynomial in $|D|$, and $M$ is a
model of at least one extension of $\deftheory{D}{W}$ iff $g_{D}(M)
\models CIRC(T;P_D;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 $\deftheory{D}{W}$, but just on $D$.

\end{example}

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 $g_{KB}$ to theorems of $KB$.

%\begin{definition}[Theorem Preservation]
%  A poly-size reduction $f:F_1 \diventa F_2$ satisfies {\em
%  theorem-preservation } if for each knowledge base $KB$ in $F_1$
%  there exists a poly-time function $g_{KB}$ such that for every
%  query $Q$ on the
%  variables of $KB$ it holds that $KB \vdash_{F_1} Q$ iff $f(KB) \vdash_{F_2}
%g_{KB}(Q)$. 
%\end{definition}

\begin{definition}[Theorem Preservation]
\label{theorem-def}

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

\end{definition}

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 be used to
represent the same set of theorems. More precisely, we have that each
theorem $\varphi$ of $KB$ is represented by a theorem $g_{KB}(\varphi)$ of 
$f(KB)$.

%This way, we represent the theorem of $KB$ in $F_1$ using a knowledge
%base of $F_2$.

%An example of theorem-preserving (and non-model-preserving) poly-size
%reduction from updated knowledge bases to PL is given in \cite{wins-89}.
%The reduction shown in the previous example is also theorem-preserving,
%using for $g_{KB}$ the identity function.

%We remark that our definitions of reduction are more general than those
%proposed in \cite{gogi-etal-95}. In particular, in \cite{gogi-etal-95} only
%a notion analogous to Definition~\ref{model-def} is considered, and only
%for the case when $g_{KB}$ is the identity -- \ie\  models in the two
%formalisms should be identical.

Winslett~\citeyear{wins-89} 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~\ref{reduction-skeptical-default} 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~\citeyear{gogi-etal-95}.
In fact, these authors consider
only a notion analogous to Definition~\ref{model-def}.
and only for the case when $g$ is the identity --- \ie\ models in the
two formalisms should be identical.  By allowing a simple translation
$g$ between models Definition~\ref{model-def} covers more general
forms of reductions preserving models, like the one of
Example~\ref{reduction-skeptical-default}.

% Local Variables: 
% mode: latex
% TeX-master: "main"
% End: 

%%%%%%%%%%%%% succinctness %%%%%%%%%%%%%%
\section{Comparing the Space Efficiency of PKR Formalisms}
\label{succinctness}

In this section we show how to use the compilability classes defined
in Section~\ref{compilability} to compare the succinctness of PKR
formalisms.

Let $F_1$ and $F_2$ be two formalisms representing sets of models. We
prove that any knowledge base $\alpha$ in $F_1$ can be reduced, via a
poly-size reduction, to a knowledge base $\beta$ in $F_2$ satisfying
model-preservation if and only if the compilability class of the
problem of {\em model checking\/} (first input: KB, second input:
interpretation) in $F_2$ is higher than or equal to the compilability
class of the problem of model checking in $F_1$.

Similarly, we prove that theorem-preserving poly-size reductions exist
if and only if the compilability class of the problem of {\em
 inference\/} (first input: KB, second input: formula, cf.\  definition
of the problem \PLI) in $F_1$ is higher than or equal to the
compilability class of the problem of inference in $F_2$.

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

% \nota{espandere 2 o 4 definizioni}
\begin{definition}
\label{mC}

{\bf (Model hard\-ness/com\-ple\-te\-ness)} Let $F$ be a PKR formalism 
and \C\ be a complexity class. If the
problem of model checking for $F$ belongs to the compilability class \nucC,
where the model is the varying part of the instances, we say that $F$ is in
\mC. Similarly, if model checking is \nucC-complete (hard), we say that $F$ is
\mC-complete (hard).

\end{definition}

\begin{definition}
\label{tC}

{\bf (Theorem hard\-ness/com\-ple\-te\-ness)} 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 \nucC, whenever the formula is the varying part of the instance, we say
that $F$ is in \tC.  Similarly, if inference is \nucC-complete (hard), we say
that $F$ is \tC-complete (hard).

\end{definition}

These definitions implicitly define two hierarchies, which parallel the
polynomial hierarchy \cite{stoc-76}: the model hierarchy (\mP,\mNP,\mS{2},etc.)
and the theorem hierarchy (\tP,\tNP,\tS{2},etc.).  The higher a formalism is in
the model hierarchy, the more its efficiency in representing models is --- and
analogously for theorems. As an example \cite[Thm.\
6]{cado-doni-scha-96}, we characterize model and theorem classes of
Propositional Logic.

\begin{theorem}
\label{model-thm-ci}

\PL\  is in \mP\  and it is \tcoNP-complete.

\end{theorem}

We can now formally establish the connection between succinctness of
representations and compilability classes. In the following theorems, the
complexity classes C, C$_1$, C$_2$ belong to the polynomial hierarchy
\cite{stoc-76}. In Theorems~\ref{model-different} and~\ref{thm-different} 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.

\begin{theorem}
\label{model-equal}

Let $F_1$ and $F_2$ be two PKR formalisms. If $F_1$ is in \mC\  and $F_2$ is
\mC-hard, then there exists a poly-size reduction $f : F_1 \diventa F_2$
satisfying model preservation.

\end{theorem}

\proof
Recall that since $F_1$ is in \mC, model checking in $F_1$ is in
\nucC, and since $F_2$ is \mC-hard, model checking in $F_1$ is
non-uniformly comp-reducible to model checking in $F_2$. That is,
(adapting Def.\  \ref{non-uniform-reduction}) there exist two poly-size
binary functions $f_1$ and $f_2$, and a polynomial-time binary
function $g$ such that for every pair ${\pair {KB}{M}}$ it holds that
%
\[
M \models_{F_1} KB \mbox{ if and only if } g(f_2(KB,|M|),M) \models_{F_2}
f_1(KB,|M|)
\]
(note that $g$ is the poly-time function appearing in 
Def.~\ref{non-uniform-reduction}, different from $g_{KB}$ which is the 
poly-size circuit appearing in Def.~\ref{model-def}).

Now observe that $|M|$ can be computed from $KB$ by simply counting 
the letters appearing in $KB$; let $f_3$ be such a counting function, 
i.e., $|M| = f_3 (KB)$.  Clearly, $f_3$ is poly-size.  Define the 
reduction $f$ as $f(KB)=f_1(KB,f_3 (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~\ref{model-def}, we 
need to prove that there exists a polynomial $p$ such that for each knowledge 
base $KB$ in $F_1$, there exists a poly-size circuit $g_{KB}$ such that for 
every interpretation $M$ of the variables of $KB$ it holds that $M 
\models_{F_1} KB$ iff $g_{KB}(M) \models_{F_2} f(KB)$.

We proceed as follows: Given a $KB$ in $F_1$, we compute 
$z=f_2(KB,|M|)= f_2(KB,f_3(KB))$.  Since $f_2$ and $f_3$ are 
poly-size, $z$ has size polynomial with respect to $|KB|$.  Define 
the circuit $g_{KB}(M)$ as the one computing $g(z,M) = g(f_2(KB,f_3(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 $g_{KB}$ whose size is polynomial wrt $KB$.  From this 
construction, $M \models_{F_1} KB$ iff $g_{KB}(M) \models_{F_2} 
f(KB)$.  Hence, the thesis follows.~\qed

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

\begin{theorem}
\label{model-different}

Let $F_1$ and $F_2$ be two PKR formalisms.  If the polynomial 
hierarchy does not collapse, $F_1$ is \mC$_1$-hard, $F_2$ is in 
\mC$_2$, and {\rm C}$_2 \subset$ {\rm C}$_1$, then there is no 
poly-size reduction $f : F_1 \diventa F_2$ satisfying model 
preservation.

\end{theorem}

\proof We show that if such a reduction exists, then C$_1$/poly $\subseteq$
C$_2$/poly which implies that the polynomial hierarchy collapses at some level
\cite{yap-83}. Let $A$ be a complete problem for class C$_1$ --- e.g., if C$_1$ is
$\Sigma^p_3$ then $A$ may be validity of $\exists\forall\exists$-quantified
boolean formulae \cite{stoc-76}. Define the problem $\epsilon A$ as follows.
%
\[ 
\epsilon A = \{{\pair x y } ~|~ x=\epsilon \mbox{~(the empty string) and~} y
\in A \} 
\] 

We already proved \cite[Thm.\ 6]{cado-etal-96} that $\epsilon A$ is
\nucC$_1$-complete.  
Since model checking in $F_1$ is \mC$_1$-hard, $\epsilon A$ is 
non-uniformly comp-reducible to model checking in $F_1$.  That is, 
(adapting Def.\ \ref{non-uniform-reduction}) there exist two poly-size 
binary functions $f_1$ and $f_2$, and a polynomial-time binary 
function $g$ such that for every pair ${\pair {\epsilon} y}$, it holds 
${\pair {\epsilon} y}\in \epsilon A$ if and only if 
$g(f_2(\epsilon,|y|),y) \models_{F_1} f_1(\epsilon,|y|)$.  Let 
$|y|=n$.  Clearly, the knowledge base $f_1(\epsilon,|y|)$ depends only 
on $n$, i.e., there is exactly one knowledge base for each integer.  
Call it $KB_n$.  Moreover, $f_2(\epsilon,|y|)=f_2(\epsilon,n)$ also 
depends on $n$ only: call it $O_n$ (for Oracle).  Observe that both 
$KB_{n}$ and $O_n$ have polynomial size with respect to $n$.

If there exists a poly-size reduction $f : F_1 \diventa F_2$ 
satisfying model preservation, then given the knowledge base $KB_n$ 
there exists a poly-size circuit $h_n$ such that $g(O_n,y) 
\models_{F_1} KB_n$ if and only if $ h_{n}(g(O_n,y)) \models_{F_2} 
f(KB_n)$.

Therefore, the \nucC$_1$-complete problem $\epsilon A$ can be 
non-uniformly reduced to a problem in \nucC$_2$ as follows: Given $y$, 
from its size $|y|=n$ one obtains (with a preprocessing) $f(KB_n)$ and 
$O_n$.  Then one checks whether the interpretation $h_{n}(g(O_n,y))$ 
(computable in polynomial time given $n$, $y$ and $O_n$) is a model in 
$F_2$ for $f(KB_n)$.  From the fact that model checking in $F_2$ is in 
\nucC$_2$, we have that \nucC$_1 \subseteq$ \nucC$_2$.
We proved in a previous paper that such result implies that
C$_1$/poly $ \subseteq$ C$_2$/poly \cite[Thm.\ 9]{cado-etal-96},
which in turns implies that the polynomial hierarchy collapses
\cite{yap-83}.~\qed

The above theorems show that the hierarchy of classes \mC\ 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~\ref{model-equal}), while there is no poly-size reduction 
from a formalism ($F_1$) higher up in the hierarchy into one ($F_2$) 
in a lower class (Theorem~\ref{model-different}).  In the latter case 
we say that $F_1$ is {\em more space-efficient} than $F_2$.

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.

\begin{theorem}
\label{thm-equal}

Let $F_1$ and $F_2$ be two PKR formalisms. If $F_1$ is in \tC\  and $F_2$ is
\tC-hard, then there exists a poly-size reduction $f : F_1 \diventa F_2$
satisfying theorem preservation.

\end{theorem}

\proof Recall that since $F_1$ is in \tC, inference in $F_1$ is in
\nucC, and since $F_2$ is \tC-hard, inference in $F_1$ is
non-uniformly comp-reducible to inference in $F_2$. That is, (adapting
Def.~\ref{non-uniform-reduction}) there exist two poly-size binary
functions $f_1$ and $f_2$, and a polynomial-time binary function $g_{1}$ 
such that for every pair ${\pair {KB}{\varphi}}$ it holds that

\[
KB \vdash_{F_1} \varphi \mbox{ if and only if }
f_1(KB,|\varphi|) \vdash_{F_2} g(f_2(KB,|\varphi|),\varphi)
\]
%
(here we distinguish the poly-time function $g$ appearing in 
Def.~\ref{non-uniform-reduction} and the poly-size circuit $g_{KB}$ 
appearing in Def.~\ref{theorem-def}).

Using Theorem~\ref{upper-bound} we can replace $|\varphi|$ with an 
upper bound in the above formula.  From Assumption~\ref{size-query}, 
we know that the size of $\varphi$ is less than or equal to the size 
of $KB$; therefore we replace $|\varphi|$ with $|KB|$.  The 
above formula now becomes

\[
KB \vdash_{F_1} \varphi \mbox{ if and only if }
f_1(KB,|KB|) \vdash_{F_2} g(f_2(KB,|KB|),\varphi)
\]
%
Define the reduction $f$ as $f(KB)=f_1(KB,f_3 (KB))$, where $f_3$ 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, \ie $f$ 
satisfies Def.~\ref{theorem-def}.  This amounts to proving that for 
each knowledge base $KB$ in $F_1$ there exists a circuit $g_{KB}$, 
whose size is poynomial wrt $KB$, such that for every formula 
$\varphi$ on the variables of $KB$ it holds that $KB \vdash_{F_1} 
\varphi$ iff $f(KB) \vdash_{F_2} g_{KB}(\varphi)$.

We proceed as in the proof of Theorem~\ref{model-equal}: Given a $KB$ in 
$F_1$, let $z=f_2(KB,f_3(KB))$.  Since $f_2$ and $f_3$ are poly-size, 
$z$ has polynomial size with respect to $|KB|$.  Define 
$g_{KB}(\varphi) = g(z,\varphi) = g(f_2(KB,f_3(KB)),\varphi)$.  
Clearly, $g_{KB}$ can be represented by a circuit of polynomial size 
wrt $KB$.  From this construction, $KB \vdash_{F_1} \varphi$ iff $f(KB) 
\vdash_{F_2} g_{KB}(\varphi)$.  Hence, the claim follows.~\qed

\begin{theorem}
\label{thm-different}

Let $F_1$ and $F_2$ be two PKR formalisms. If the polynomial hierarchy does not
collapse, $F_1$ is \tC$_1$-hard,  $F_2$ is in \tC$_2$, and {\rm C}$_2 \subset$
{\rm C}$_1$, then there is no poly-size reduction $f : F_1 \diventa F_2$
satisfying theorem preservation.

\end{theorem}

\proof We show that if such a reduction exists, then C$_1$/poly $\subseteq$
C$_2$/poly and the polynomial hierarchy collapses at some level 
\cite{yap-83}.  Let $A$ be a complete problem for class C$_1$.  Define 
the problem $\epsilon A$ as in the proof of 
Theorem~\ref{model-different}: this problem is \nucC$_1$-complete 
\cite[Thm.\ 6]{cado-etal-96}.  Since inference in $F_1$ is 
\tC$_1$-hard, $\epsilon A$ is non-uniformly comp-reducible to 
inference in $F_1$.  That is, (adapting Def.\ 
\ref{non-uniform-reduction}) there exist two poly-size binary 
functions $f_1$ and $f_2$, and a polynomial-time binary function $g$ 
such that for every pair ${\pair {\epsilon} y}$, ${\pair {\epsilon} 
y}\in \epsilon A$ if and only if $ f_1(\epsilon,|y|) \vdash_{F_1} 
g(f_2(\epsilon,|y|),y)$.  Let $|y|=n$.  Clearly, the knowledge base 
$f_1(\epsilon,|y|)$ depends just on $n$, i.e., there is one knowledge 
base for each integer.  Call it $KB_n$.  Moreover, also 
$f_2(\epsilon,|y|)=f_2(\epsilon,n)$ depends just on $n$: call it $O_n$ 
(for Oracle).  Observe that both $KB_{n}$ and $O_n$ have polynomial 
size with respect to $n$.

If there exists a poly-size reduction $f : F_1 \diventa F_2$
satisfying theorem preservation, then given the knowledge base $KB_n$
there exists a poly-time function $h_n$ such that $ KB_n \vdash_{F_1}
g(O_n,y)$ if and only if $ f(KB_n) \vdash_{F_2} h_n(g(O_n,y))$.

Therefore, the \nucC$_1$-complete problem $\epsilon A$ can be
non-uniformly reduced to a problem in \nucC$_2$ as follows: Given $y$,
from its size $|y|=n$ one obtains (with an arbitrary preprocessing)
$f(KB_n)$ and $O_n$. Then one checks whether the formula $h_n(g(O_n,y))$
(computable in poly-time given $y$ and $O_n$) is a theorem in $F_2$ of
$f(KB_n)$. From the fact that inference in $F_2$ is in \nucC$_2$, we
have that \nucC$_1 \subseteq$ \nucC$_2$.
It follows that C$_1$/poly $ \subseteq$ C$_2$/poly \cite[Thm.\ 9]{cado-etal-96},
which implies that the polynomial hierarchy collapses \cite{yap-83}.~\qed

\

Theorems~\ref{model-equal}-\ref{thm-different} 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~\ref{model-thm-ci} and
\ref{thm-different} 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 \citeyear{kaut-selm-92-a} proved non-existence of such a
reduction for a problem strictly related to \PLI\  using a specific proof.


% Local Variables: 
% mode: latex
% TeX-master: "main"
% End: 

%%%%%%%%%%%%% applications %%%%%%%%%%%%%%
\section{Applications}
\label{applications}
% struttura della sezione:
% 1. definizioni preliminari
% 2. teoremi
% 3. tabella
% 4. discussione risultati

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

This section is devoted to the application of the theorems presented
in the previous section. Using
Theorems~\ref{model-equal}-\ref{thm-different} and results previously
known from the literature, we are able to asses model- and
theorem-compactness of some PKR formalisms.

%By proving membership and completeness for
%appropriate complexity classes, we are able to assess the relative
%space efficiency of several PKR formalisms.

%We first recall definitions of some PKR formalisms.
We assume that definitions of Propositional Logic, default logic
\cite{reit-80}, and circumscription \cite{mcca-80} are known.
Definitions of WIDTIO, SBR, GCWA, and stable model semantics are in
the appropriate subsections.

%\riga
In the following proofs we refer to the problem $\exists\forall$3QBF,
that is, the problem of verifying whether a quantified Boolean formula
$\exists X \forall Y. \neg F$ is valid, where $X$ and $Y$ are
disjoint sets of variables, and $F$ is a set of clauses on the
alphabet $X \cup Y$, each composed of three literals. As an example, a
simple formula belonging to this class is: $\exists x_1,x_2 \forall
y_1,y_2 ~~\neg ((x_1 \vee y_2) \wedge (\neg x_1 \vee \neg x_2 \vee
\neg y_1) \wedge (\neg y_1 \vee \neg x_2 \vee \neg y_2) \wedge (\neg
x_1 \vee \neg x_2))$.

The problem of deciding validity of a $\exists\forall$3QBF is complete
for the class \Stwo. As a consequence, the corresponding problem
$*\exists\forall$3QBF, that is deciding whether an input composed of
any string ($*$) as the fixed part and a quantified Boolean formula
$\exists X \forall Y. \neg F$ as the varying one, is complete for
the class \nucS{2} \cite{libe-98-b}. Notice that in most of the
hardness proofs we show in the sequel we use problems without any
meaningful fixed part.

\subsection{Stable Model Semantics}
\label{app:stable}

Stable model semantics ({\bf SM}) was introduced by Gelfond and Lifschitz
\citeyear{gelf-lifs-88} 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.

%\noindent {\bf SM} (Stable Model  semantics \cite{gelf-lifs-88})
%for propositional logic programs is defined as follows:
Let $P$ be a propositional, general logic program. Let $M$ be a subset
(\ie\ 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 $\neg A$ such that $A \in M$ then
$C$ is deleted; if a body of a clause contains a negated atom $\neg A$
such that $A \not\in M$ then $\neg 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 \models_{\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
%For the next theorem we need the definition of
the kernel of a graph.

\begin{definition}[Kernel]
        Let $G=(V,E)$ be a graph.
        A \emph{kernel} of $G$ is a set $K \subseteq V$ such that, denoting 
        $H=V-K$, it holds:
        \begin{enumerate}
                \item  $H$ is a vertex cover of $G$
                \item  for all $j \in H$, there exists an $i \in K$ such that 
                $(i,j) \in E$.
         \end{enumerate}  
\end{definition}

\noindent We can now state the theorem on the compilability class of
inference in the stable model semantics, and the corresponding theorem
compactness class.

\begin{theorem}
\label{theo:inference-sm}
The problem of inference for the Stable Model semantics is
\nuccoNP-complete, thus Stable Model Semantics is \tcoNP complete.

\end{theorem}

\proof Membership in the class follows from the fact that the problem
is \coNP-complete \cite{mare-trus-91-a}. For the hardness, we adapt
the proof of Marek and Truszczy\'nski \citeyear{mare-trus-91-a} showing that
deciding whether a query is true in all stable models is \coNP-hard.

Let $\epsilon$\kernel\  be the language $\{ \epsilon, 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 $P_{n}$ such that 
for every graph $G$ with at most  $n$ vertices, there exists a query $Q_{G}$ such 
that $G$ has a kernel iff $P_{n} \not\models_{\SM} Q_{G}$.

Let the alphabet of $P_{n}$ be composed by the following $2n^{2}+n$ 
propositional letters:
$\{ a_{i} | i \in\{1..n\} ~ \} \cup 
\{  r_{ij}, s_{ij} | i,j \in \{1..n\} ~\}$.

The program $P_{n}$ is defined as:
%
\[\left.
\begin{array}{rcl}
   a_{j} & \prologif & \neg a_{i}, r_{ij} \\
   s_{ij} & \prologif & \neg r_{ij} \\
   r_{ij} & \prologif & \neg s_{ij}
\end{array}\right\} \mbox{for } i,j\in\{1..n\}
\]
%
Given a graph $G=(V,E)$, the query $Q_{G}$ is defined as
%
\[ Q_{G} = (\bigvee_{(i,j)\in E} \neg r_{ij}) 
             \vee (\bigvee_{(i,j)\not\in E} r_{ij})  \]
%  
The reduction from $\epsilon$\kernel\  to \SM\  is defined as: 
%\nota{\`e una nu-comp-reduction? se si, dirlo. mc}
$f_{1}(x,n) = P_{n}$, \ie\  $f_{1}$ depends only on its second 
argument, $f_{2}(x, n) = \epsilon$, \ie\  $f_{2}$ is a constant 
function, and $g = Q_{y}$,
%$g(y,f_{2}(x,n))=g(y,\epsilon)=Q_{y}$,
%\ie\ given a pair $\pair{\epsilon}{G}$, the function $g$ computes the
\ie\ given a graph $G$, the circuit $g$ computes the query $Q_{G}$.

As a result, this is a \nucomp\  reduction. We now show that this reduction is
correct, \ie\  $\pair{\epsilon}{G}\in \epsilon$\kernel\  ($G$ has a kernel) iff
$P_{n} \not\models_{SM} Q_{G}$.

\textsl{If-part.} Suppose $P_{n} \not\models_{SM} Q_{G}$. Then, there 
exists a stable model $M$ of $P_{n}$ such that $M \models \neg Q_{G}$.
Observe that $\neg Q_{G}$ is equivalent to the conjunction of all 
$r_{ij}$ such that $(i,j)\in E$, and all $\neg r_{ij}$ such that 
$(i,j)\not\in E$. Simplifying $P_{n}$ with $\neg Q_{G}$ we obtain 
the clauses:
\begin{equation} 
   a_{j}  \prologif  \neg a_{i}, \mbox{ for } (i,j) \in E  
   \label{edge:clauses}
\end{equation}
Observe that $M$ contains all $s_{ij}$  such that $(i,j) \not\in E$, 
and in order to be stable, --- \ie\  to support atoms $r_{ij}$ such that 
$(i,j)\in E$ --- $M$ contains no atom 
$s_{ij}$ such that $(i,j) \in E$.

Let $H= \{ j | a_{j} \in M \}$, $K = \{ i | a_{i} \not\in M \}$. 
Now $H$ is a vertex cover of G, since 
for each edge $(i,j)\in E$, $M$ should satisfy the corresponding clause 
(\ref{edge:clauses}) 
$a_{j} \prologif \neg a_{i}$, hence either $a_{i} \in M$, or $a_{j} \in M$.
Moreover, for each $j$ in $H$, the atom $a_{j}$ is in $M$,
and since $M$ is a stable model, there exists a clause 
$a_{j} \prologif \neg a_{i}$ such that 
$a_{i} \not\in M$, that is, $i\in K$. Therefore, $K$ is a kernel of 
$G$.  

\textsl{Only-if part.} Suppose $G=(V,E)$ has a kernel $K$, and let 
$H=V-K$. Let $M$ be the interpretation
\[
M = \{ r_{ij} | (i,j) \in E \} \cup 
\{ s_{ij} | (i,j) \not\in E \} \cup 
\{ a_{j} | j \in H \}
\]
%
Obviously, $M \not\models Q_{G}$. We now show that $M$ is a stable 
model of $P_{n}$, \ie\  $M$ is a least Herbrand model of $P_{n}^{M}$. 
In fact, $P_{n}^{M}$ contains the following clauses:
\begin{eqnarray}
        s_{ij} &  &  \mbox{ for } (i,j) \not\in E  \\
        r_{ij} &  &  \mbox{ for } (i,j) \in E  \label{clause:for:edge} \\
        a_{j} & \prologif r_{ij} & \mbox{ for } i \in K \label{clause:for:K}
\end{eqnarray}
%
Clauses in the last line are obtained from clauses in $P_{n}$ of the form
$a_{j} \prologif \neg a_{i}, r_{ij}$, where the clauses such that $i \in H$
(hence $a_{i} \in M$) are deleted, while in the other clauses the negated atom
$\neg a_{i}$ is deleted, since $i \in K$, hence $a_{i} \not\in M$.  Now for
each $a_{j} \in M$, the vertex $j$ is in $H$, hence there is an edge $(i,j)\in
E$, and $i \in K$.  Hence clauses (\ref{clause:for:K}) and
(\ref{clause:for:edge}) are in $P_{n}^{M}$, hence in the least Herbrand model
of $P_{n}^{M}$ there are exactly all $a_{j}$ such that $j\in H$.  \qed


\subsection{Minimal Model Reasoning}
\label{app:minimal}

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
\cite{mcca-80} and the Generalized Closed World Assumption (GCWA)
\cite{mink-82}, 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 \models_{GCWA} KB  ~\mbox{iff~} M \models KB \cup \{\neg a ~|~ \mbox{for
 any positive} \mbox{~clause $\gamma$,
if $KB \not\vdash \gamma$ then $KB \not\vdash \gamma \vee a \}$ }
\]

We can now present the results for these two formalisms.

\begin{theorem}
\label{theo:model-circ}
The problem of model checking for Circumscription is
\nuccoNP-complete, thus Circumscription is \mcoNP-complete.
\end{theorem}

This result is a trivial corollary of a theorem already proved
\cite[Theorem~6]{cado-etal-97-c}. In fact, that proof implicitly
shows that model checking for circumscription is \nuccoNP-complete.

\begin{theorem}
\label{theo:model-gcwa}
The problem of model checking for GCWA is in
\nucP, thus GCWA is in \mP.
\end{theorem}

\proof As already pointed out \cite{cado-etal-97-c}, it is possible
to rewrite $GCWA(T)$ into a propositional formula $F$ such that, for
any given model $M$, $M \models GCWA(T)$ if and only if $M \models 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~\ref{model-thm-ci} the thesis
follows.~\qed

\begin{theorem}
\label{theo:inference-circ}
The problem of inference for Circumscription is
\nucPi{2}-complete, thus Circumscription is \tPi{2}-complete.
\end{theorem}

This result is a trivial corollary of a theorem published
in a previous paper
\cite[Theorem~7]{cado-etal-97-c} which implicitly
shows that inference for circumscription is \nucPi{2}-complete.

\begin{theorem}
\label{theo:inference-gcwa}
The problem of inference for GCWA is \nuccoNP-complete, thus GCWA is
\tcoNP-complete.
\end{theorem}

\proof As already pointed out in the proof of
Theorem~\ref{theo:model-gcwa}, it is possible to rewrite $GCWA(T)$
into a formula $F$ that is equivalent to it. As a consequence, a
formula $\alpha$ is a theorem of $GCWA(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
\tcoNP-complete.~\qed

\subsection{Default Logic}
\label{app:default}

%\riga
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~\citeyear{kaut-selm-91-a}. Notice that
model-compactness is only applicable to skeptical default logic.
%\nota{Da completare con commenti.}
%We are now ready to present the technical results of this section.
%Using Theorems~\ref{model-equal}-\ref{thm-different} and results previously
%known from the literature, we are able to asses  model- and
%theorem-compactness of some PKR formalisms.

\begin{theorem}
\label{theo:model-skep-dl}
The problem of model checking for skeptical default logic is
\nucS{2} complete, thus skeptical default logic is \mS{2} complete.

\end{theorem}

\proof The proof of membership is straightforward: since model checking for
skeptical default logic is in \Stwo\  \cite{libe-scha-98}, it
follows that it is also in \nucS{2}.

The proof of \nucS{2}-hardness is similar to the proof of
\Stwo-hardness \cite{libe-scha-98}. The reduction is from the
problem $*\exists\forall$3QBF.  Let $\langle \alpha,\beta \rangle$ be
an instance of $*\exists\forall$3QBF, where $\beta = \exists X \forall
Y . \neg F$ represents a valid $\exists\forall$3QBF formula, and
$\alpha$ 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=\{\gamma_1,\ldots,\gamma_k\}$ 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(n^3)$, thus
bounded by a polynomial in $n$.

We prove that $\exists X \forall Y .\neg F$ is valid if
and only if $M$ is a model of some extension of $\langle W,D \rangle$, where

\begin{eqnarray*}
W &=& \emptyset \\
D &=&
\bigcup_{\gamma_i\in\Gamma} \left\{ \defaultone{c_i}, \defaultone{\neg c_i} \right\}
\cup
\bigcup_{x_i \in X} \left\{
        \defaultthree{}{w \wedge (w \rightarrow x_i)}{w \rightarrow x_i},
        \defaultthree{}{w \wedge (w \rightarrow \neg x_i)}{w \rightarrow \neg x_i}
                \right\}
\cup 
\left\{
        \defaultthree{}
                {w \wedge \bigwedge_{\gamma_i\in\Gamma} c_i \rightarrow \gamma_i}
                {w}
\right\}
\\
M &=& \{ c_i ~|~ \gamma_i \in F \}
\end{eqnarray*}

The set $\{ c_i ~|~ 1 \leq i \leq 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 $\leqnucomp$
reduction.

We now prove that the formula is valid if and only if $M$ is a model of some
extension of the default theory $\langle W,D \rangle$. This is similar to an
already published proof \cite{libe-scha-98}. Consider an evaluation $C_1$ of the
variables $\{c_i\}$ and an evaluation $X_1$ of the variables $X$. Let $D'$ be
the following set of defaults.

\[
D' =
\bigcup_{c_i \in C_1} \left\{ \defaultone{c_i} \right\}
\bigcup_{c_i \not\in C_1} \left\{ \defaultone{\neg c_i} \right\} 
\cup
\bigcup_{x_i \in X_1}   \left\{
        \defaultthree{}{w \wedge (w \rightarrow x_i)}{w \rightarrow x_i}
                        \right\}
\bigcup_{x_i \neg\in X_1}       \left\{
        \defaultthree{}{w \wedge (w \rightarrow \neg x_i)}{w \rightarrow \neg x_i}
                                \right\}
\]

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

\begin{eqnarray*}
c_i \in C_1 & \mbox{iff} & R \models c_i \\
c_i \not\in C_1 & \mbox{iff} & R \models \neg c_i \\
x_i \in X_1 & \mbox{iff} & R \models w \rightarrow x_i \\
x_i \not\in X_1 & \mbox{iff} & R \models w \rightarrow \neg x_i 
\end{eqnarray*}

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:

\begin{enumerate}
\itemsep=0pt

\item the set of consequences of $D'$ is consistent; and

\item no other default is applicable, that is, there is no other default whose
precondition is consistent with $R$.

\end{enumerate}

Consistency of $R$ follows by construction: assigning $c_i$ to true for each
$c_i \in C_1$, etc., we obtain a model of $R$.

We have then to prove that no other default is applicable. If $c_i \in C_1$,
the default $\defaultone{\neg c_i}$ is not applicable, and vice versa, if $\neg
c_i \in C_1$, then $\defaultone{c_i}$ is not applicable. Moreover, none of the
defaults $\defaultthree{}{w \wedge (w \rightarrow x_i)}{w \rightarrow x_i}$, is
applicable if $x_i \not\in X_1$, because in this case $w \rightarrow \neg x_i
\in R$, thus $\neg w$ would follow (while $w$ is a justification of the
default). A similar statement holds for $\defaultthree{}{w \wedge (w
\rightarrow \neg x_i)}{w \rightarrow \neg x_i}$ if $x_i \in X_1$.

As a result, the only applicable default may be the last one,
$\defaultthree{}{w \wedge \bigwedge_{\gamma_i\in\Gamma} c_i
 \rightarrow \gamma_i}{w}$ (recall that F is negated).  This default
is applicable if and only if, for the given evaluation of the $c_i$'s
and $x_i$'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 \not\models 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.~\qed

%A complementary result holds for skeptical default logic:

\begin{theorem}
\label{theo:inference-skep-dl}
The inference problem for skeptical default logic is
\nucPi{2} complete, thus skeptical default logic is \tPi{2} complete.

\end{theorem}

\proof Since inference in skeptical default logic is in \Ptwo,
it is also in \nucPi{2}. \nucPi{2}-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 $\langle T,D \rangle$,
where \cite{ethe-87-a}:

\[
D = \bigcup \left\{ \defaultone{\neg x_i} \right\}
\]

As a result, $CI\!RC(T) \models Q$ if and only if $Q$ is implied by
$\langle T,D \rangle$ under skeptical semantics. Since $\langle T,D
\rangle$ only depends on $T$ (and not on $Q$) this is a $\leqnucomp$
reduction. Since inference for circumscription is \nucPi{2}-complete
(see Theorem~\ref{theo:inference-circ}), it follows that skeptical
default logic is \nucPi{2}-hard.~\qed


\begin{theorem}
\label{theo:inference-cred-dl}
The inference problem  for credulous default logic is \nucS{2}
complete, thus credulous default logic is \tS{2} complete.

\end{theorem}

\proof The proof is very similar to the proof for model checking of skeptical
default logic. Indeed, both problems are \nucS{2} complete.  Since the problem
is in \Stwo, as proved by Gottlob \citeyear{gott-92-b}, it is also in \nucS{2}.
Thus, what we have to prove is that is hard for that class.

We prove that the $*\exists\forall$3QBF 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 $\forall X \exists Y . \neg F$ is valid if and only
if $Q$ is derived by some extension of the default theory $\langle D,W \rangle$,
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$).

\begin{eqnarray*}
W &=& \emptyset \\
D &=& 
\bigcup_{c_i \in C} \left\{ \defaultone{c_i} , \defaultone{\neg c_i} \right\}
\cup
\bigcup_{x_i \in X} \left\{ \defaultone{x_i} , \defaultone{\neg x_i} \right\}
\cup
\left\{
        \defaultthree{\neg ( \bigwedge_{c_i \in C} c_i \rightarrow \gamma_i )}{}{w}
\right\}
\\
Q &=&
\bigwedge_{\gamma_i \in F} c_i \wedge \bigwedge_{\gamma_i \not\in F} \neg c_i
\wedge w
\end{eqnarray*}

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

\[
\neg \bigwedge_{c_i={\rm true}} \gamma_i
\]

\noindent 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 $c_i$ is true if and only if $\gamma_i \in
F$, and such that $w$ also holds. When the variables $c_i$ have the given
value, the above formula is equivalent to $\neg F$. As a result, such an
extension exists if and only if there exists a truth evaluation of the
variables $X$ in which $\neg F$ is valid.~\qed

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Belief Revision}
\label{app: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:
\[
\begin{array}{ll}
W(K,A) = \{ K'
& \multicolumn{1}{|l}{K' \mbox{ is a maximal consistent subset }} \mbox{of $K \cup \{A\}$ containing $A$} \}
\end{array}
\]

Any set of formulae $K' \in 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.
%There are various possibilities for defining the revision $K*A$
%of $K$ with $A$. We recall two of them from the literature.

\begin{description}

\item[SBR] Skeptical Belief Revision
\cite{fagi-ullm-vard-83,gins-86}. The revised theory is defined as a
set of theories: $K * A \doteq \{K' \mid K'\in W(K,A)\}$. Inference in
the revised theory is defined as inference in each of the theories:
\[ 
\begin{array}{rcl}
K*A \vdash_{SBR} Q & \mbox{iff} & \mbox{ for all $K' \in W(K,A)$ }, \mbox{ we have that } K' \vdash Q
\end{array}
\]
The model semantics is defined as:
\[ 
\begin{array}{rcl}
M \models_{SBR} K*A & \mbox{iff} & \mbox{ there exists a $K' \in W(K,A)$ } \mbox{ such that } M \models K'
\end{array}
\]

\item[WIDTIO] When In Doubt Throw It Out \cite{wins-90}.
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:
\[ 
\begin{array}{rcl}
K*A \vdash_{WIDTIO} Q & \mbox{iff} & \bigcap W(K,A) \vdash Q
\end{array}
\]

The model semantics of this formalism is defined as:
\[
M \models_{WIDTIO} K*A \mbox{ ~~ iff ~~ }  M \models \bigcap W(K,A) 
\]

\end{description}

The results on model compactness have been shown by Liberatore
and Schaerf \citeyear{libe-scha-00-b}. Here we recall them.

\begin{theorem}{\bf \cite[Theorem 11]{libe-scha-00-b}}
\label{theo:model-widtio}
The problem of model checking for WIDTIO is in \nucP, thus WIDTIO is
in \mP.
\end{theorem}

\begin{theorem}{\bf \cite[Theorem 5]{libe-scha-00-b}}
\label{theo:model-sbr}
The problem of model checking for Skeptical Belief Revision is
\nuccoNP-complete, thus Skeptical Belief Revision is \mcoNP-complete.
\end{theorem}

The results on theorem compactness are quite simple and we provide
here the proofs.

\begin{theorem}
\label{theo:inference-widtio}
The problem of inference for WIDTIO is
\nuccoNP-complete, thus WIDTIO is \tcoNP-complete.
\end{theorem}

\proof Membership in the class \tcoNP\ 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 \cup 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 \tcoNP-complete (see
Theorem~\ref{model-thm-ci}).~\qed

\begin{theorem}
\label{theo:inference-sbr}
The problem of inference for Skeptical Belief Revision is
\nucPi{2}-complete, thus Skeptical Belief Revision is \tPi{2}-complete.
\end{theorem}

\proof Membership follows from the complexity results of Eiter and
Gottlob \citeyear{eite-gott-91-b}, where they show that deciding whether
$K*A \vdash_{SBR} Q$ is a $\Pi^p_2$-complete problem. Hardness follows
easily from Theorem~\ref{theo:model-sbr}. In fact, $M \models_{SBR}
K*A$ iff $K*A \not\vdash_{SBR} \neg form(M)$, where $form(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 \nucPi{2}-complete.~\qed

\subsection{Discussion}
\label{app:discussion}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\riga Tables~\ref{risultati1}~and~\ref{risultati2} summarize the results
on space efficiency of PKR formalisms and where they were proved (a
dash ``{\bf --}'' denotes a folklore result).

\begin{table*}[tb]
  \begin{center}
    \leavevmode
%\begin{footnotesize}
\begin{small}
\begin{tabular}{|c||c|c|}
\hline
                & Time Complexity                & Space Efficiency\\
\hline
\hline
Propositional           & \P            & \mP\\
Logic           &     {\bf --}          & {\bf --}\\
\hline
WIDTIO          & \Stwo-complete & \mP\\
                & \cite{libe-scha-96}&  Th.\ \ref{theo:model-widtio} \\
\hline
Skeptical       & \coNP-complete & \mcoNP-complete \\
Belief Revision &\cite{libe-scha-96} & Th.\ \ref{theo:model-sbr} \\
\hline
Circumscription         & \coNP-complete  & \mcoNP-complete \\
                &\cite{cado-92-b}& Th.\ \ref{theo:model-circ} \\
\hline
GCWA            & \coNP-hard,  & \mP \\
                & in \Dtwo[$\log n$] & Th.\ \ref{theo:model-gcwa} \\
                & \cite{eite-gott-93-b} &  \\
\hline  
Skeptical       & \Stwo-complete & \mS{2}-complete \\
Default Reasoning& \cite{libe-scha-98} & Th.\ \ref{theo:model-skep-dl} \\
\hline
Credulous       & N/A & N/A \\
Default Reasoning&    &    \\
\hline 
Stable Model    & P     & \mP \\
Semantics&   {\bf --}      &      {\bf --} \\
%Logic Programs&&&&\\
\hline
\end{tabular}
%\end{footnotesize}
\end{small}
  \end{center}
\caption{Complexity of model checking and Space Efficiency of Model Representations}
\label{risultati1}
\end{table*}


\begin{table*}[tb]
  \begin{center}
    \leavevmode
%\begin{footnotesize}
\begin{small}
\begin{tabular}{|c||c|c||c|c|}
\hline
                & Time Complexity   &Space Efficiency \\
\hline
\hline
Propositional           & \coNP-complete  & \tcoNP-complete\\
Logic           &    \cite{cook-71}  &   \cite{cado-doni-scha-96}         \\
\hline
WIDTIO          & \Ptwo-complete  & \tcoNP-complete\\
               & \cite{eite-gott-91-b} \& \cite{nebe-98} & Th.\ \ref{theo:inference-widtio} \\
\hline
Skeptical       & \Ptwo-complete & \tPi{2}-complete \\
Belief Revision & \cite{eite-gott-91-b} & Th.\ \ref{theo:inference-sbr} \\
\hline
Circumscription         & \Ptwo-complete       & \tPi{2}-complete\\
                & \cite{eite-gott-93-b}&Th.\ \ref{theo:inference-circ}\\
\hline
GCWA            & \Ptwo-complete   & \tcoNP-complete\\
               & \cite{eite-gott-93-b} \& \cite{nebe-98}& Th.\ \ref{theo:inference-gcwa}\\
\hline
Skeptical       & \Ptwo-complete  & \tPi{2}-complete\\
Default Reasoning& \cite{gott-92-b}   &  Th.\ \ref{theo:inference-skep-dl}   \\
\hline
Credulous       & \Stwo-complete        & \tS{2}-complete\\
Default Reasoning& \cite{gott-92-b}  & Th.\ \ref{theo:inference-cred-dl}    \\
\hline 
Stable Model    & \coNP-complete   &  \tcoNP-complete\\
Semantics&   \cite{mare-trus-91-a} &  Th.\ \ref{theo:inference-sm} \\
%Logic Programs&&&&\\
\hline
\end{tabular}
%\end{footnotesize}
\end{small}
  \end{center}
\caption{Complexity of inference and Space Efficiency of Theorem Representations}
\label{risultati2}
\end{table*}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4 4
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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 \tS{2}-complete and WIDTIO is
\tcoNP-complete (and thus in \tS{2}), there exists a poly-size reduction from
WIDTIO to circumscription satisfying theorem preservation.  The converse does
not hold: since circumscription is \tS{2}-complete and WIDTIO is \tcoNP, 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 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.


%The same considerations hold for the other results.  
Figures~\ref{model} and~\ref{theorem} contain the same information of
Tables~\ref{risultati1} and \ref{risultati2}, 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 poly-size 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 \cite{gogi-etal-95}, a
theorem-preserving poly-size reduction exists, as shown by
Theorem~\ref{theo:inference-skep-dl}.

\begin{figure*}
%%%%%%%%%%%%% model-new.latex %%%%%%%%%%%%%%
\setlength{\unitlength}{3552sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(7599,3141)(1714,-5515)
\put(8626,-4786){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Stable}}}
\put(8626,-5011){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Model}}}
\thinlines
\put(3001,-3136){\vector( 0, 1){225}}
\put(3001,-3661){\vector( 0, 1){225}}
\put(2401,-3961){\vector(-1, 0){  0}}
\put(2401,-3961){\vector( 1, 0){450}}
\put(3001,-4486){\vector( 0, 1){225}}
\put(2476,-4861){\vector(-1, 0){  0}}
\put(2476,-4861){\vector( 1, 0){525}}
\put(6901,-4186){\makebox(1.8519,12.9630){\SetFigFont{5}{6}{\rmdefault}{\mddefault}{\updefault}.}}
\put(6901,-4486){\vector( 0, 1){300}}
\put(6901,-3436){\vector( 0, 1){375}}
\put(6301,-3886){\vector(-1, 0){  0}}
\put(6301,-3886){\vector( 1, 0){525}}
\put(4726,-5161){\dashbox{67}(4575,600){}}
\put(5176,-4861){\vector(-1, 0){  0}}
\put(5176,-4861){\vector( 1, 0){450}}
\put(8026,-4861){\vector(-1, 0){  0}}
\put(8026,-4861){\vector( 1, 0){525}}
\put(6601,-4861){\vector(-1, 0){  0}}
\put(6601,-4861){\vector( 1, 0){600}}
\put(5701,-4111){\dashbox{67}(2850,450){}}
\put(1726,-4186){\dashbox{67}(2775,450){}}
\put(2026,-5086){\dashbox{67}(2325,450){}}
\put(1726,-2836){\dashbox{67}(2925,450){}}
\put(2851,-2611){\vector(-1, 0){  0}}
\put(2851,-2611){\vector( 1, 0){600}}
\put(1951,-2686){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}WIDTIO}}}
\put(2701,-3361){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}GCWA}}}
\put(3001,-4036){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Circumscription}}}
\put(1951,-4036){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}SBR}}}
\put(2176,-4936){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}PL}}}
\put(3151,-4936){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Stable Model}}}
\put(5851,-3961){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}SBR}}}
\put(6976,-3961){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Circumscription}}}
\put(6301,-2986){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Skeptical Default}}}
\put(4876,-4936){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}PL}}}
\put(5776,-4936){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}WIDTIO}}}
\put(7351,-4936){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}GCWA}}}
\put(2401,-5461){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}a. Time Complexity}}}
\put(6001,-5461){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}b. Space Efficiency}}}
\put(3601,-2536){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Skeptical}}}
\put(3601,-2761){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}Default}}}
\end{picture}

\caption{Complexity of Model Checking vs.\  Space Efficiency of Model
Representation}
\label{model}
\end{figure*}

\begin{figure*}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%MAGNIFICATION XFIG = 90%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%% theorem-new.latex %%%%%%%%%%%%%%
\setlength{\unitlength}{3552sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(7824,2541)(739,-5290)
\thinlines
\put(6901,-4111){\vector(-1, 2){150}}
\put(1276,-3436){\vector(-1, 0){  0}}
\put(1276,-3436){\vector( 1, 0){450}}
\put(2401,-3436){\vector(-1, 0){  0}}
\put(2401,-3436){\vector( 1, 0){450}}
\put(2776,-4786){\dashbox{67}(1500,600){}}
\put(3331,-4096){\vector(-3, 4){225}}
\put(3871,-4096){\vector( 1, 2){225}}
\put(6226,-3436){\vector(-1, 0){  0}}
\put(6226,-3436){\vector( 1, 0){300}}
\put(4801,-3736){\dashbox{67}(2625,600){}}
\put(7846,-4096){\vector( 1, 2){225}}
\put(4801,-4786){\dashbox{67}(3750,600){}}
\put(5176,-4486){\vector(-1, 0){  0}}
\put(5176,-4486){\vector( 1, 0){300}}
\put(7426,-4486){\vector(-1, 0){  0}}
\put(7426,-4486){\vector( 1, 0){300}}
\put(6376,-4486){\vector(-1, 0){  0}}
\put(6376,-4486){\vector( 1, 0){300}}
\put(3226,-4486){\vector(-1, 0){  0}}
\put(3226,-4486){\vector( 1, 0){300}}
\put(751,-3736){\dashbox{67}(2850,975){}}
\put(1051,-3061){\vector( 0, 1){  0}}
\put(1051,-3061){\vector( 0,-1){300}}
\put(1576,-2986){\vector(-1, 0){  0}}
\put(1576,-2986){\vector( 1, 0){450}}
\put(5251,-3436){\vector(-1, 0){  0}}
\put(5251,-3436){\vector( 1, 0){375}}
\put(1801,-3511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Circum}}}
\put(2926,-3361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Skeptical}}}
\put(3001,-3586){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Default}}}
\put(901,-3511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}SBR}}}
\put(3901,-3586){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Default}}}
\put(3826,-3361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Credulous}}}
\put(4876,-3511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}SBR}}}
\put(5701,-3511){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Circum}}}
\put(6676,-3361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Skeptical}}}
\put(6751,-3586){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Default}}}
\put(7726,-3361){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Credulous}}}
\put(7801,-3586){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Default}}}
\put(7876,-4636){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Model}}}
\put(7876,-4411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Stable}}}
\put(4951,-4561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}PL}}}
\put(6826,-4561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}GCWA}}}
\put(5626,-4561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}WIDTIO}}}
\put(2926,-4561){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}PL}}}
\put(3751,-4411){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Stable}}}
\put(3751,-4636){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}Model}}}
\put(901,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}WIDTIO}}}
\put(2176,-3061){\makebox(0,0)[lb]{\smash{\SetFigFont{9}{10.8}{\familydefault}{\mddefault}{\updefault}GCWA}}}
\put(6076,-5236){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}b. Space efficiency}}}
\put(2176,-5236){\makebox(0,0)[lb]{\smash{\SetFigFont{11}{13.2}{\familydefault}{\mddefault}{\updefault}a. Time complexity}}}
\end{picture}

\caption{Complexity of Inference vs.\  Space Efficiency of Theorem
Representation}
\label{theorem}
\end{figure*}


% Local Variables: 
% mode: latex
% TeX-master: "main"
% End: 

%%%%%%%%%%%%% conclusions %%%%%%%%%%%%%%
\section{Related Work and Conclusions}
\label{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 second-order logic 
\cite{schl-87}. Kolaitis and Papadimitriou 
\citeyear{kola-papa-90} 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 first-order language is used, more 
results on compactness and existence of reductions are reported by 
Schlipf \citeyear{schl-95-b}.  

Khardon and Roth \citeyear{khar-roth-96,khar-roth-97}, and Kautz, 
Kearns and Selman \citeyear{kaut-kear-selm-95} propose model-based 
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 
\emph{different} PKR formalisms.  The same comment applies also to the idea of 
representing a $KB$ with an efficient basis by Moses and Tennenholz 
\citeyear{mose-tenn-96}, 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 {\em modularity} and
{\em faithfulness}. Janhunen \citeyear{janh-98}, improving on results
of Imielinski \citeyear{imie-87} and Gottlob \citeyear{gott-95},
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.

%Bisogna citare \cite{janh-98}, che tratta traduzioni fra formalismi
%non-monotoni che hanno le propriet\`a di essere:
%\begin{itemize}
%\item {\em polynomial time \& space}
%\item faithful
%\end{itemize}
%e che estende lavori precedenti (\cite{imie-87,gott-95}) sulla modularit\`a
%delle traduzioni.

The first result on compactness of representations for a propositional
language is presented, to the best of our knowledge, by Kautz and
Selman \citeyear{kaut-selm-92-a}.  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 
\cite{selm-kaut-96}.  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 
\cite{cado-doni-scha-96,cado-etal-97-c,cado-etal-99,gogi-etal-95}.

%Using this tool we have been able to improve on previous work on
%compact representations
%\cite{kaut-selm-92-a}.
%\cite{schl-88}
%\cite{schl-95}

In a recent paper \cite{cado-etal-96} we introduced a new complexity 
measure, \ie\ {\em 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:

\begin{enumerate}
  
\item All the proofs presented in the previous papers only compare
  pairs of PKR formalisms, for example propositional circumscription
  and Propositional Logic \cite{cado-etal-97-c}. These results do not
  allow for a precise classification of the level of compactness of
  the considered formalisms. Rephrasing and adapting these results in
  our framework allows us to infer that circumscription is
  \mcoNP-complete and {\tPi 2}-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.
  
\item Using the proposed framework it is now possible to find criteria
  for adapting existent polynomial reductions showing C-hardness into
  reductions that show \mC\ or \tC-hardness, where C is a class in the
  polynomial hierarchy \cite{libe-98-b}.

\end{enumerate}


% Local Variables: 
% mode: latex
% TeX-master: "main"
% End: 

%%%%%%%%%%%%% ack %%%%%%%%%%%%%%
\vbox{
\acks{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) \cite{cado-etal-96-b}.
Partial supported has been given by ASI (Italian Space Agency) and CNR
(National Research Council of Italy).}
}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 


%\newpage
\bibliographystyle{theapa}
\begin{thebibliography}{}

\bibitem[\protect\BCAY{Ben-Eliyahu \BBA\ Dechter}{Ben-Eliyahu \BBA\
  Dechter}{1991}]{bene-dech-91}
Ben-Eliyahu, R.\BBACOMMA\  \BBA\ Dechter, R. \BBOP1991\BBCP.
\newblock \BBOQ Default logic, propositional logic and constraints\BBCQ\
\newblock In {\Bem Proceedings of the Ninth National Conference on Artificial
  Intelligence (AAAI'91)}, \BPGS\ 379--385.

\bibitem[\protect\BCAY{Ben-Eliyahu \BBA\ Dechter}{Ben-Eliyahu \BBA\
  Dechter}{1994}]{bene-dech-94}
Ben-Eliyahu, R.\BBACOMMA\  \BBA\ Dechter, R. \BBOP1994\BBCP.
\newblock \BBOQ Propositional semantics for disjunctive logic programs\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem 12},
  53--87.

\bibitem[\protect\BCAY{Boppana \BBA\ Sipser}{Boppana \BBA\
  Sipser}{1990}]{bopp-sips-90}
Boppana, R.\BBACOMMA\  \BBA\ Sipser, M. \BBOP1990\BBCP.
\newblock \BBOQ The complexity of finite functions\BBCQ\
\newblock In van Leeuwen, J.\BED, {\Bem Handbook of Theoretical Computer
  Science}, \lowercase{\BVOL}~A, \BCH~14. Elsevier Science Publishers
  (North-Holland), Amsterdam.

\bibitem[\protect\BCAY{Cadoli}{Cadoli}{1992}]{cado-92-b}
Cadoli, M. \BBOP1992\BBCP.
\newblock \BBOQ The complexity of model checking for circumscriptive
  formulae\BBCQ\
\newblock {\Bem Information Processing Letters}, {\Bem 44}, 113--118.

\bibitem[\protect\BCAY{Cadoli, Donini, Liberatore, \BBA\ Schaerf}{Cadoli
  et~al.}{1996a}]{cado-etal-96-b}
Cadoli, M., Donini, F., Liberatore, P., \BBA\ Schaerf, M. \BBOP1996a\BBCP.
\newblock \BBOQ Comparing space efficiency of propositional knowledge
  representation formalisms\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Conference on the
  Principles of Knowledge Representation and Reasoning (KR'96)}, \BPGS\
  364--373.

\bibitem[\protect\BCAY{Cadoli, Donini, Liberatore, \BBA\ Schaerf}{Cadoli
  et~al.}{1996b}]{cado-etal-96}
Cadoli, M., Donini, F.~M., Liberatore, P., \BBA\ Schaerf, M. \BBOP1996b\BBCP.
\newblock \BBOQ Feasibility and unfeasibility of off-line processing\BBCQ\
\newblock In {\Bem Proceedings of the Fourth Israeli Symposium on Theory of
  Computing and Systems (ISTCS'96)}, \BPGS\ 100--109. IEEE Computer Society
  Press.
\newblock {\sc url = \tt
  ftp://ftp.dis.uniroma1.it/PUB/AI/papers/cado-etal-96.ps.gz}.

\bibitem[\protect\BCAY{Cadoli, Donini, Liberatore, \BBA\ Schaerf}{Cadoli
  et~al.}{1997}]{cado-etal-97-d}
Cadoli, M., Donini, F.~M., Liberatore, P., \BBA\ Schaerf, M. \BBOP1997\BBCP.
\newblock \BBOQ Preprocessing of intractable problems\BBCQ\
\newblock \BTR\ DIS 24-97, Dipartimento di Informatica e Sistemistica,
  Universit{\`a} di Roma ``La Sapienza''.
\newblock {\sc url = \tt
  http://ftp.dis.uniroma1.it/PUB/AI/papers/cado-etal-97-d-REVISED.ps.gz}.

\bibitem[\protect\BCAY{Cadoli, Donini, Liberatore, \BBA\ Schaerf}{Cadoli
  et~al.}{1999}]{cado-etal-99}
Cadoli, M., Donini, F.~M., Liberatore, P., \BBA\ Schaerf, M. \BBOP1999\BBCP.
\newblock \BBOQ The size of a revised knowledge base\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 115\/}(1), 25--64.

\bibitem[\protect\BCAY{Cadoli, Donini, \BBA\ Schaerf}{Cadoli
  et~al.}{1995}]{cado-doni-scha-95}
Cadoli, M., Donini, F.~M., \BBA\ Schaerf, M. \BBOP1995\BBCP.
\newblock \BBOQ On compact representations of propositional
  circumscription\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth Symposium on Theoretical Aspects
  of Computer Science (STACS'95)}, \BPGS\ 205--216.
\newblock Extended version as RAP.14.95 DIS, Univ. of Roma ``La Sapienza'',
  July 1995.

\bibitem[\protect\BCAY{Cadoli, Donini, \BBA\ Schaerf}{Cadoli
  et~al.}{1996}]{cado-doni-scha-96}
Cadoli, M., Donini, F.~M., \BBA\ Schaerf, M. \BBOP1996\BBCP.
\newblock \BBOQ Is intractability of non-monotonic reasoning a real
  drawback?\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 88\/}(1--2), 215--251.

\bibitem[\protect\BCAY{Cadoli, Donini, Schaerf, \BBA\ Silvestri}{Cadoli
  et~al.}{1997}]{cado-etal-97-c}
Cadoli, M., Donini, F.~M., Schaerf, M., \BBA\ Silvestri, R. \BBOP1997\BBCP.
\newblock \BBOQ On compact representations of propositional
  circumscription\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 182}, 183--202.

\bibitem[\protect\BCAY{Cook}{Cook}{1971}]{cook-71}
Cook, S.~A. \BBOP1971\BBCP.
\newblock \BBOQ The complexity of theorem-proving procedures\BBCQ\
\newblock In {\Bem Proceedings of the Third ACM Symposium on Theory of
  Computing (STOC'71)}, \BPGS\ 151--158.

\bibitem[\protect\BCAY{Eiter \BBA\ Gottlob}{Eiter \BBA\
  Gottlob}{1992}]{eite-gott-91-b}
Eiter, T.\BBACOMMA\  \BBA\ Gottlob, G. \BBOP1992\BBCP.
\newblock \BBOQ On the complexity of propositional knowledge base revision,
  updates and counterfactuals\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 57}, 227--270.

\bibitem[\protect\BCAY{Eiter \BBA\ Gottlob}{Eiter \BBA\
  Gottlob}{1993}]{eite-gott-93-b}
Eiter, T.\BBACOMMA\  \BBA\ Gottlob, G. \BBOP1993\BBCP.
\newblock \BBOQ Propositional circumscription and extended closed world
  reasoning are {$\Pi^p_2$}-complete\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 114}, 231--245.

\bibitem[\protect\BCAY{Etherington}{Etherington}{1987}]{ethe-87-a}
Etherington, D.~V. \BBOP1987\BBCP.
\newblock {\Bem Reasoning with incomplete information}.
\newblock Morgan Kaufmann, Los Altos, Los Altos, CA.

\bibitem[\protect\BCAY{Fagin, Ullman, \BBA\ Vardi}{Fagin
  et~al.}{1983}]{fagi-ullm-vard-83}
Fagin, R., Ullman, J.~D., \BBA\ Vardi, M.~Y. \BBOP1983\BBCP.
\newblock \BBOQ On the semantics of updates in databases\BBCQ\
\newblock In {\Bem Proceedings of the Second ACM SIGACT SIGMOD Symposium on
  Principles of Database Systems (PODS'83)}, \BPGS\ 352--365.

\bibitem[\protect\BCAY{Garey \BBA\ Johnson}{Garey \BBA\
  Johnson}{1979}]{gare-john-79}
Garey, M.~R.\BBACOMMA\  \BBA\ Johnson, D.~S. \BBOP1979\BBCP.
\newblock {\Bem Computers and Intractability: {A} Guide to the Theory of
  {NP}-Completeness}.
\newblock W.H. Freeman and Company, San Francisco, Ca.

\bibitem[\protect\BCAY{Gelfond \BBA\ Lifschitz}{Gelfond \BBA\
  Lifschitz}{1988}]{gelf-lifs-88}
Gelfond, M.\BBACOMMA\  \BBA\ Lifschitz, V. \BBOP1988\BBCP.
\newblock \BBOQ The stable model semantics for logic programming\BBCQ\
\newblock In {\Bem Proceedings of the Fifth Logic Programming Symposium},
  \BPGS\ 1070--1080. The {MIT} Press.

\bibitem[\protect\BCAY{Gelfond, Przymusinska, \BBA\ Przymusinsky}{Gelfond
  et~al.}{1989}]{gelf-przy-przy-89}
Gelfond, M., Przymusinska, H., \BBA\ Przymusinsky, T. \BBOP1989\BBCP.
\newblock \BBOQ On the relationship between circumscription and negation as
  failure\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 38}, 49--73.

\bibitem[\protect\BCAY{Ginsberg}{Ginsberg}{1986}]{gins-86}
Ginsberg, M.~L. \BBOP1986\BBCP.
\newblock \BBOQ Conterfactuals\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 30}, 35--79.

\bibitem[\protect\BCAY{Gogic, Kautz, Papadimitriou, \BBA\ Selman}{Gogic
  et~al.}{1995}]{gogi-etal-95}
Gogic, G., Kautz, H.~A., Papadimitriou, C., \BBA\ Selman, B. \BBOP1995\BBCP.
\newblock \BBOQ The comparative linguistics of knowledge representation\BBCQ\
\newblock In {\Bem Proceedings of the Fourteenth International Joint Conference
  on Artificial Intelligence (IJCAI'95)}, \BPGS\ 862--869.

\bibitem[\protect\BCAY{Gottlob}{Gottlob}{1992}]{gott-92-b}
Gottlob, G. \BBOP1992\BBCP.
\newblock \BBOQ Complexity results for nonmonotonic logics\BBCQ\
\newblock {\Bem Journal of Logic and Computation}, {\Bem 2}, 397--425.

\bibitem[\protect\BCAY{Gottlob}{Gottlob}{1995}]{gott-95}
Gottlob, G. \BBOP1995\BBCP.
\newblock \BBOQ Translating default logic into standard autoepistemic
  logic\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 42}, 711--740.

\bibitem[\protect\BCAY{Imielinski}{Imielinski}{1987}]{imie-87}
Imielinski, T. \BBOP1987\BBCP.
\newblock \BBOQ Results on translating defaults to circumscription\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 32}, 131--146.

\bibitem[\protect\BCAY{Janhunen}{Janhunen}{1998}]{janh-98}
Janhunen, T. \BBOP1998\BBCP.
\newblock \BBOQ On the intertranslatability of autoepistemic, default and
  priority logics, and parallel circumscription\BBCQ\
\newblock In {\Bem Proceedings of the Sixth European Workshop on Logics in
  Artificial Intelligence (JELIA'98)}, \lowercase{\BNUM}\ 1489 in Lecture Notes
  in Artificial Intelligence, \BPGS\ 216--232. Springer-Verlag.

\bibitem[\protect\BCAY{Johnson}{Johnson}{1990}]{john-90}
Johnson, D.~S. \BBOP1990\BBCP.
\newblock \BBOQ A catalog of complexity classes\BBCQ\
\newblock In van Leeuwen, J.\BED, {\Bem Handbook of Theoretical Computer
  Science}, \lowercase{\BVOL}~A, \BCH~2. Elsevier Science Publishers
  (North-Holland), Amsterdam.

\bibitem[\protect\BCAY{Karp \BBA\ Lipton}{Karp \BBA\
  Lipton}{1980}]{karp-lipt-80}
Karp, R.~M.\BBACOMMA\  \BBA\ Lipton, R.~J. \BBOP1980\BBCP.
\newblock \BBOQ Some connections between non-uniform and uniform complexity
  classes\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth ACM Symposium on Theory of
  Computing (STOC'80)}, \BPGS\ 302--309.

\bibitem[\protect\BCAY{Kautz, Kearns, \BBA\ Selman}{Kautz
  et~al.}{1995}]{kaut-kear-selm-95}
Kautz, H.~A., Kearns, M.~J., \BBA\ Selman, B. \BBOP1995\BBCP.
\newblock \BBOQ Horn approximations of empirical data\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 74}, 129--145.

\bibitem[\protect\BCAY{Kautz \BBA\ Selman}{Kautz \BBA\
  Selman}{1991}]{kaut-selm-91-a}
Kautz, H.~A.\BBACOMMA\  \BBA\ Selman, B. \BBOP1991\BBCP.
\newblock \BBOQ Hard problems for simple default logics\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 49}, 243--279.

\bibitem[\protect\BCAY{Kautz \BBA\ Selman}{Kautz \BBA\
  Selman}{1992}]{kaut-selm-92-a}
Kautz, H.~A.\BBACOMMA\  \BBA\ Selman, B. \BBOP1992\BBCP.
\newblock \BBOQ Forming concepts for fast inference\BBCQ\
\newblock In {\Bem Proceedings of the Tenth National Conference on Artificial
  Intelligence (AAAI'92)}, \BPGS\ 786--793.

\bibitem[\protect\BCAY{Khardon \BBA\ Roth}{Khardon \BBA\
  Roth}{1996}]{khar-roth-96}
Khardon, R.\BBACOMMA\  \BBA\ Roth, D. \BBOP1996\BBCP.
\newblock \BBOQ Reasoning with models\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 87}, 187--213.

\bibitem[\protect\BCAY{Khardon \BBA\ Roth}{Khardon \BBA\
  Roth}{1997}]{khar-roth-97}
Khardon, R.\BBACOMMA\  \BBA\ Roth, D. \BBOP1997\BBCP.
\newblock \BBOQ Defaults and relevance in model-based reasoning\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 97}, 169--193.

\bibitem[\protect\BCAY{K\"obler \BBA\ Watanabe}{K\"obler \BBA\
  Watanabe}{1998}]{kobl-wata-98}
K\"obler, J.\BBACOMMA\  \BBA\ Watanabe, O. \BBOP1998\BBCP.
\newblock \BBOQ New collapse consequences of {NP} having small circuits\BBCQ\
\newblock {\Bem {SIAM} Journal on Computing}, {\Bem 28\/}(1), 311--324.

\bibitem[\protect\BCAY{Kolaitis \BBA\ Papadimitriou}{Kolaitis \BBA\
  Papadimitriou}{1990}]{kola-papa-90}
Kolaitis, P.~G.\BBACOMMA\  \BBA\ Papadimitriou, C.~H. \BBOP1990\BBCP.
\newblock \BBOQ Some computational aspects of circumscription\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 37\/}(1), 1--14.

\bibitem[\protect\BCAY{Liberatore}{Liberatore}{1995}]{libe-95}
Liberatore, P. \BBOP1995\BBCP.
\newblock \BBOQ Compact representation of revision of {H}orn clauses\BBCQ\
\newblock In Yao, X.\BED, {\Bem Proceedings of the Eighth Australian Joint
  Artificial Intelligence Conference (AI'95)}, \BPGS\ 347--354. World
  Scientific.

\bibitem[\protect\BCAY{Liberatore}{Liberatore}{1998}]{libe-98-b}
Liberatore, P. \BBOP1998\BBCP.
\newblock {\Bem Compilation of intractable problems and its application to
  artificial intelligence}.
\newblock Ph.D.\ thesis, Dipartimento di Informatica e Sistemistica,
  Universit{\`a} di Roma ``La Sapienza''.
\newblock URL = {\tt ftp://ftp.dis.uniroma1.it/pub/AI/papers/libe-98-c.ps.gz}.

\bibitem[\protect\BCAY{Liberatore \BBA\ Schaerf}{Liberatore \BBA\
  Schaerf}{1996}]{libe-scha-96}
Liberatore, P.\BBACOMMA\  \BBA\ Schaerf, M. \BBOP1996\BBCP.
\newblock \BBOQ The complexity of model checking for belief revision and
  update\BBCQ\
\newblock In {\Bem Proceedings of the Thirteenth National Conference on
  Artificial Intelligence (AAAI'96)}, \BPGS\ 556--561.

\bibitem[\protect\BCAY{Liberatore \BBA\ Schaerf}{Liberatore \BBA\
  Schaerf}{1998}]{libe-scha-98}
Liberatore, P.\BBACOMMA\  \BBA\ Schaerf, M. \BBOP1998\BBCP.
\newblock \BBOQ The complexity of model checking for propositional default
  logics\BBCQ\
\newblock In {\Bem Proceedings of the Thirteenth European Conference on
  Artificial Intelligence (ECAI'98)}, \BPGS\ 18--22.

\bibitem[\protect\BCAY{Liberatore \BBA\ Schaerf}{Liberatore \BBA\
  Schaerf}{2000}]{libe-scha-00-b}
Liberatore, P.\BBACOMMA\  \BBA\ Schaerf, M. \BBOP2000\BBCP.
\newblock \BBOQ The compactness of belief revision and update operators\BBCQ\
\newblock \BTR, Dipartimento di Informatica e Sistemistica, Universit{\`a} di
  Roma ``La Sapienza''.

\bibitem[\protect\BCAY{Marek \BBA\ Truszczy\'nski}{Marek \BBA\
  Truszczy\'nski}{1991}]{mare-trus-91-a}
Marek, W.\BBACOMMA\  \BBA\ Truszczy\'nski, M. \BBOP1991\BBCP.
\newblock \BBOQ Autoepistemic logic\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 38\/}(3), 588--619.

\bibitem[\protect\BCAY{McCarthy}{McCarthy}{1980}]{mcca-80}
McCarthy, J. \BBOP1980\BBCP.
\newblock \BBOQ Circumscription - {A} form of non-monotonic reasoning\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 13}, 27--39.

\bibitem[\protect\BCAY{Minker}{Minker}{1982}]{mink-82}
Minker, J. \BBOP1982\BBCP.
\newblock \BBOQ On indefinite databases and the closed world assumption\BBCQ\
\newblock In {\Bem Proceedings of the Sixth International Conference on
  Automated Deduction (CADE'82)}, \BPGS\ 292--308.

\bibitem[\protect\BCAY{Moses \BBA\ Tennenholtz}{Moses \BBA\
  Tennenholtz}{1996}]{mose-tenn-96}
Moses, Y.\BBACOMMA\  \BBA\ Tennenholtz, M. \BBOP1996\BBCP.
\newblock \BBOQ Off-line reasoning for on-line efficiency: knowledge
  bases\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 83}, 229--239.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1998}]{nebe-98}
Nebel, B. \BBOP1998\BBCP.
\newblock \BBOQ How hard is it to revise a belief base?\BBCQ\
\newblock In Dubois, D.\BBACOMMA\  \BBA\ Prade, H.\BEDS, {\Bem Belief Change -
  Handbook of Defeasible Reasoning and Uncertainty Management Systems, Vol. 3}.
  Kluwer Academic.

\bibitem[\protect\BCAY{Reiter}{Reiter}{1980}]{reit-80}
Reiter, R. \BBOP1980\BBCP.
\newblock \BBOQ A logic for default reasoning\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 13}, 81--132.

\bibitem[\protect\BCAY{Schlipf}{Schlipf}{1987}]{schl-87}
Schlipf, J.~S. \BBOP1987\BBCP.
\newblock \BBOQ Decidability and definability with circumscription\BBCQ\
\newblock {\Bem Annals of Pure and Applied Logic}, {\Bem 35}, 173--191.

\bibitem[\protect\BCAY{Schlipf}{Schlipf}{1995}]{schl-95-b}
Schlipf, J.~S. \BBOP1995\BBCP.
\newblock \BBOQ A survey of complexity and undecidability results for logic
  programming\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem 15},
  257--288.

\bibitem[\protect\BCAY{Selman \BBA\ Kautz}{Selman \BBA\
  Kautz}{1996}]{selm-kaut-96}
Selman, B.\BBACOMMA\  \BBA\ Kautz, H.~A. \BBOP1996\BBCP.
\newblock \BBOQ Knowledge compilation and theory approximation\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 43}, 193--224.

\bibitem[\protect\BCAY{Stockmeyer}{Stockmeyer}{1976}]{stoc-76}
Stockmeyer, L.~J. \BBOP1976\BBCP.
\newblock \BBOQ The polynomial-time hierarchy\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 3}, 1--22.

\bibitem[\protect\BCAY{Winslett}{Winslett}{1989}]{wins-89}
Winslett, M. \BBOP1989\BBCP.
\newblock \BBOQ Sometimes updates are circumscription\BBCQ\
\newblock In {\Bem Proceedings of the Eleventh International Joint Conference
  on Artificial Intelligence (IJCAI'89)}, \BPGS\ 859--863.

\bibitem[\protect\BCAY{Winslett}{Winslett}{1990}]{wins-90}
Winslett, M. \BBOP1990\BBCP.
\newblock {\Bem Updating Logical Databases}.
\newblock Cambridge University Press.

\bibitem[\protect\BCAY{Yap}{Yap}{1983}]{yap-83}
Yap, C.~K. \BBOP1983\BBCP.
\newblock \BBOQ Some consequences of non-uniform conditions on uniform
  classes\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 26}, 287--300.

\end{thebibliography}

\end{document}
