\documentstyle[jair,twoside,11pt,theapa]{article}

\jairheading{11}{1999}{277-300}{5/99}{10/99}

\ShortHeadings{Reasoning about minimal belief and negation as failure}{Rosati}

\firstpageno{277}

%\input{macros}

%%%%%%%%%%%%%%%%%%%%%%%%%%% theorems, proofs, examples and general assumptions
\newtheorem%
     {theorem}{Theorem}[section]
\newtheorem%
     {corollary}[theorem]{Corollary}
\newtheorem%
     {proposition}[theorem]{Proposition} 
\newtheorem%
     {lemma}[theorem]{Lemma} 
\newtheorem%
     {definition}[theorem]{Definition}

\newtheorem%
     {exampleAux}[theorem]{Example} 
\newenvironment%
     {example}{\begin{exampleAux}\rm}{\end{exampleAux}}

\newtheorem%
     {examplesAux}[theorem]{Examples} 
\newenvironment%
     {examples}{\begin{examplesAux}\rm}{\end{examplesAux}}

\newtheorem%
     {constructionAux}[theorem]{Construction} 
\newenvironment%
     {construction}{\begin{constructionAux}\rm}{\end{constructionAux}}

\def\proof{{\sl Proof.\ \ }}

\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}}


\newcommand{\hangif}[1]{\raisebox{-1ex}{\hspace{2em}
                                        \makebox[1.0em][l]{if}
                                        \parbox[t]{300pt}{#1}}}


\newenvironment%
     {genass}%
        {\medbreak\noindent{\bf General Assumption.\enspace}\it}%
        {\ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi}

\newenvironment%%%%%%%%%%%%%%%%%%%   Commented Equations   %%%%%%%%%%%%
     {comeqns}%   
        {\vspace{-.5ex}      %\begin-part
         \[   \renewcommand{\arraystretch}{1.3}%
              \begin{array}{lcl@{\qquad}rl}}%
        {\end{array}%         %\end-part
         \]
         \vspace{-.5ex}}


\newenvironment%%%%%%%%%%%%%%%%%%%   Pairs of Equations   %%%%%%%%%%%%
     {paireqns}%   
        {\vspace{-.5ex}      %\begin-part
         \[   \renewcommand{\arraystretch}{1.3}%
              \begin{array}{rcl@{\qquad}rcl}}%
        {\end{array}%        %\end-part
         \]
         \vspace{-.5ex}}

%%%%%%%%%%%%%%%%%%%%%%%%% Abbreviazioni calligrafiche

\def\A{{\cal A}} 
\def\B{{\cal B}} \def\C{{\cal C}} \def\D{{\cal D}} 
\def\E{{\cal E}} \def\F{{\cal F}} \def\G{{\cal G}} 
\def\I{{\cal I}} \def\J{{\cal J}} \def\L{{\cal L}}  
\def\M{{\cal M}} \def\N{{\cal N}}
\def\R{{\cal R}} \def\S{{\cal S}} \def\V{{\cal V}} \def\X{{\cal X}}
\def\W{{\cal W}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  altre abbreviazioni

\def\per{\mbox{\bf .}}   % period


\def\ol#1{\overline{#1}}                   %overline
\def\dd#1#2{#1_1,\ldots,#1_{#2}}                                                                %da da, makes x1,...,xn

%%\def\set#1{\{#1\}}

%%\def\bigset#1{ \Bigl\{ #1 \Bigr\} }           % makes the big set { #1 }
%%\def\bigmid{\ \Big|\ }
%%\def\card#1\def\set#1{\{#1\}}{|{#1}|}
%%\def\sub#1{[#1]}

\def\Onlyif{{\em Only-if part.\/}}  %---> of iff-proof
\def\If{{\em If part.\/}}           %<--- of iff-proof

\def\true{\mbox{{\sf true}}}
\def\false{\mbox{{\sf false}}}

\def\TRUE{\mbox{{\it TRUE}}}
\def\FALSE{\mbox{{\it FALSE}}}

\def\derives{\vdash}

\newcommand{\pair}[2]{\langle#1,#2\rangle}

\newcommand{\commento}[1]{}  

\newcommand{\picfont}{\tt}   % picture font

\newcommand{\wncomment}[1]{{\bf COMMENT begin\ }{\sl #1 }{\bf end\ \ }}


%%%%%%%%%%%%%%%%%%%%%%%    Figures

\newcommand {\boxfigureone}[1]%
   {\framebox[\textwidth]{%
    \parbox {0.90\textwidth}
                {{#1}\vspace {0cm}\hfill}}}

%%%%%%%%%%%%%%%%%%%%%%%    Symbols


\newcommand{\bb}{B}
\newcommand{\k}{\bb}

%%%%%%%%%%%%%%%%%%%%%%%%    Languages and Logics Names

\newcommand{\En}{{\bf\sf N}}
\newcommand{\K}{{\bf\sf K}}
\newcommand{\T}{{\bf\sf T}}
\newcommand{\SWfive}{{\bf\sf SW5}}
\def\SWfiven{{\bf\sf SW5n}}
\newcommand{\Kfour}{{\bf\sf K4}}
\newcommand{\KDfour}{{\bf\sf KD4}}
\newcommand{\Sfour}{{\bf\sf S4}}
\def\Sfourtwo{{\bf\sf S4.2}}
\def\Sfourthree{{\bf\sf S4.3}}
\newcommand{\SfourF}{{\bf\sf S4F}}
\newcommand{\Kfourfive}{{\bf\sf K45}}
\newcommand{\KDfourfive}{{\bf\sf KD45}}
\newcommand{\Sfive}{{\bf\sf S5}}




\newif\ifcomment \commentfalse
\def\commentON{\commenttrue}
\def\commentOFF{\commentfalse}
\typeout{Commenti On/Off by Fabio Massacci, Nov. 1995}
\long\outer\def\BC#1\EC{\ifcomment\sloppy\par\#\ldots\dotfill
{\tt #1}$\,$\dotfill\#\par\fi}

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

\def\mbnf{{\rm MBNF}}
\def\mknf{{\rm MKNF}}
\def\ael{{\rm AEL}}

\def\lm{\L_M}
\def\lb{\L_B}
%%\def\lk{\L_K}
\def\lmk{\L_M^S}
\def\lmf{\L_M^1}
\def\lms{\L_M^S}
\def\lbs{\L_B^S}

\def\n{{\it not}}
\def\nn{\neg{\it not}}

\def\sigmatre{\Sigma^p_3}
\def\sigmadue{\Sigma^p_2}

\def\pitre{\Pi^p_3}
\def\pidue{\Pi^p_2}

\def\cons{\vdash}

\def\np{NP}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BOXES

\newcommand{\fpbox}[3]{\framebox[#1]{\parbox{#2}{#3}}}
\newcommand{\boxtext}[1]{\fpbox{\textwidth}{0.9\textwidth}{#1}}
\newcommand{\boxnarrow}[1]{\fpbox{0.7\columnwidth}{0.9\columnwidth}{#1}}
\newcommand{\boxcolumn}[1]{\fpbox{\columnwidth}{0.9\columnwidth}{#1}}
%\newcommand{\box}[2]{\fpbox{#1\columnwidth}{0.9\columnwidth}{#2}}
\newcommand{\boxformula}[1]{%
  \vspace{\abovedisplayskip}
  \boxtext{\vspace{-\abovedisplayskip} #1 \vspace{-\abovedisplayskip}}
  \vspace{\abovedisplayskip}}
\newcommand{\boxtwo}[2]{\fpbox{#1\columnwidth}{0.9\columnwidth}{#2}}

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

\def\imp{\Rightarrow}

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

\def\olk{{\cal OL}_\Kfourfive}
\def\olsfive{{\cal OL}_\Sfive}

\def\objo#1{\Sim{OBJ(#1)}}

\def\schemaK{{\bf K}}
\def\schemaD{{\bf D}}
\def\schemaT{{\bf T}}
\def\schemaB{{\bf B}}
\def\schemafour{{\bf 4}}
\def\schemafive{{\bf 5}}
\def\schemaWfive{{\bf W5}}
\def\schemaF{{\bf F}}

\def\adls{{\rm ADLs}}
\def\allog{{\cal AL}\mbox{{\sc -log}}}
\def\dllog{\dl\mbox{\sc -log}}
\def\datalog{\mbox{\sc Datalog}}
\def\carin{\mbox{\sc Carin}}

\def\tb{{\cal T}}
\def\ab{{\cal A}}
\def\GER{\gamma}
\def\TR{\Gamma}
\def\inds{{\cal O}}
\def\dl{{\cal DL}}
\def\dlk{{\cal DLK}}
\def\pp{\tau_{\it prdl}}
\def\trK{\tau_K}
\def\trdef{\tau_{DK}}
\def\Alpha{\Lambda}
\def\ae{A}
\def\IMP{\Rightarrow}


\def\vfi{\varphi}
\def\ob{{\it ob}(P,N)}
\def\obp{{\it ob}(P',N')}
\def\obpp{{\it ob}(P'',N'')}
\def\masi{MA(\Sigma)}
\def\parti{{\it Prt}}
\def\partiob{\parti(\Sigma,\ob)}
\def\partiobp{\parti(\Sigma,\obp,\ob)}

\def\tetapdue{{\rm P}^{{\rm NP}}[O(\log n)]}
\def\sfiveg{{\Sfive_G}}
\def\Sfiveg{\sfiveg}

\def\ST{{\it ST}}

\def\married{{\it married}}
\def\hasnochildren{{\it hasNoChildren}}

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

\title{Reasoning about Minimal Belief and Negation as Failure}

\author{\name Riccardo Rosati \email rosati@dis.uniroma1.it\\
\addr Dipartimento di Informatica e Sistemistica\\
Universit\`a di Roma ``La Sapienza''\\
Via Salaria 113, 00198 Roma, Italy}

\begin{document}

\maketitle

%\input{abstract}
\begin{abstract} 
We investigate the problem of reasoning in the propositional fragment of
$\mbnf$, the logic of minimal belief and negation as failure introduced by
Lifschitz, which can be considered as a unifying framework for several
nonmonotonic formalisms, including default logic, autoepistemic logic,
circumscription, epistemic queries, and logic programming.
We characterize the complexity and provide algorithms for reasoning in
propositional $\mbnf$.  In particular, we show that skeptical entailment in
propositional $\mbnf$ is $\Pi^p_3$-complete, hence it is harder than
reasoning in all the above mentioned propositional formalisms for
nonmonotonic reasoning.
We also prove the exact correspondence between negation as failure in
$\mbnf$ and negative introspection in Moore's autoepistemic logic.
\end{abstract}


%\input{intro}
\section{Introduction}

Research in the formalization of commonsense reasoning has pointed out the
need of formalizing agents able to reason introspectively about their own
knowledge and ignorance \cite{moor-85,Leve90}.
%Among the logical formalisms proposed to this aim, 
Modal epistemic logics have thus been proposed, in which modalities are
interpreted in terms of knowledge or belief.  Generally speaking, the
conclusions an introspective agent is able to draw depend on both what she
knows and what she \emph{does not} know.  Hence, any such conclusion may be
retracted when new facts are added to the agent's knowledge. For this
reason, many \emph{nonmonotonic} modal formalisms have been proposed in
order to characterize the reasoning abilities of an introspective agent.

Among the nonmonotonic modal logics proposed in the literature, the logic
of minimal belief and negation as failure $\mbnf$ \cite{Lifs91,Lifs94} is
one of the most studied formalisms \cite{Chen94,Boch95,BeSc93}.
Roughly speaking, such a logic is built by adding to first-order logic two
distinct modalities, a ``minimal belief'' modality $B$ and a ``negation as
failure'' modality $\n$.  The logic thus obtained is characterized in terms
of a nice model-theoretic semantics.  $\mbnf$ has been used in order to
give a declarative semantics to very general classes of logic programs
\cite{LiWo92,LiSc93,InSa94}, which generalize the stable model semantics of
negation as failure in logic programming
\cite{gelf-lifs-88,gelf-lifs-90,gelf-lifs-91}.  Also, $\mbnf$ can be viewed
as an extension of the theory of epistemic queries to databases
\cite{Reit90}, which deals with the problem of querying a first-order
database about its own knowledge.  Due to its ability of expressing many
features of nonmonotonic logics \cite{Lifs94,LiSc93}, $\mbnf$ is generally
considered as a unifying framework for several nonmonotonic formalisms,
including default logic, autoepistemic logic, circumscription, epistemic
queries, and logic programming.

Although several aspects of the logic $\mbnf$ have been thoroughly
investigated \cite{LiSc93,Chen94,Boch95}, the existing studies concerning
the computational properties of $\mbnf$ are limited to subclasses of
propositional $\mbnf$ theories \cite{InSa94} or to a very restricted subset
of the first-order case \cite{BeSc93}. 

In this paper we present a computational characterization of deduction in
the propositional fragment of $\mbnf$.  In particular, we show that logical
implication in the propositional fragment of $\mbnf$ is a
$\Pi^p_3$-complete problem: hence, it is harder (unless the polynomial
hierarchy collapses) than reasoning in all the best known propositional
formalisms for nonmonotonic reasoning, like autoepistemic logic
\cite{niem-92,gott-92-b}, default logic \cite{gott-92-b}, circumscription
\cite{eite-gott-93-b}, (disjunctive) logic programming \cite{EiGo95}, and
several McDermott and Doyle's logics \cite{mare-trus-93}. As shown in the
following, this result also implies that minimal knowledge is
computationally harder than negation as failure.

Moreover, we study the subclass of \emph{flat} $\mbnf$ theories, i.e.\
$\mbnf$ theories without nested occurrences of modalities, showing that in
this case logical implication is $\Pi^p_2$-complete.  This case is the most
interesting one from the logic programming viewpoint.  Indeed, it implies
that, under the stable model semantics, increasing the syntax of program
rules, by allowing propositional formulas as goals in the rules, does not
affect the worst-case complexity of query answering for disjunctive logic
programs with negation as failure.

Furthermore, we provide algorithms for reasoning both in $\mbnf$ and in its
flat fragment, which are optimal with respect to worst-case complexity.
Notably, such deductive methods can be considered as generalizations of
known methods for reasoning in nonmonotonic formalisms such as default
logic, autoepistemic logic, and logic programming under stable model
semantics.

We also show that the ``negation as failure'' modality in $\mbnf$ exactly
corresponds to negative introspection in autoepistemic logic
\cite{moor-85}. This result implies that the logic $\mbnf$ can be
considered as the ``composition'' of two epistemic modalities: the
``minimal knowledge'' operator due to \citeA{HaMo85n}
and Moore's autoepistemic operator.

Besides its theoretical interest, we believe that such a computational and
epistemological analysis of $\mbnf$ has interesting implications for the
development of knowledge representation systems with nonmonotonic
abilities, since it allows for a better understanding and comparison of the
different nonmonotonic formalisms captured by $\mbnf$.  The interest in
defining deductive methods for $\mbnf$ also arises from the fact that such
a logic, originally developed as a framework for the comparison of
different logical approaches to nonmonotonic reasoning, has recently been
considered as an attractive knowledge representation formalism.  In
particular, it has been shown \cite{DoNR97b} that the full power of
$\mbnf$ is necessary in order to logically formalize several features of
implemented frame-based knowledge representation systems.

In the following, we first briefly recall the logic $\mbnf$.  In Section~3
we address the relationship between $\mbnf$ and Moore's autoepistemic
logic. Then, in Section~4 we study the problem of reasoning in
propositional $\mbnf$: we first consider the case of general $\mbnf$
theories, then we deal with flat $\mbnf$ theories. In Section~5 we present
the computational characterization of reasoning in $\mbnf$. We conclude in
Section~6. This paper is an extended and thoroughly revised version of
\cite{Rosa97}.


%\input{prel}
\section{The Logic MBNF} \label{sec-prel}

In this section we briefly recall the logic $\mbnf$ \cite{Lifs94}, which is
a modal logic with two epistemic operators: a ``minimal belief'' modality
$B$ and a ``negation as failure'' (also called ``negation by default'')
modality $\n$. We use $\L$ to denote a fixed propositional language built
in the usual way from: (i) an alphabet $\A$ of propositional symbols; (ii)
the symbols $\true$, $\false$; (iii) the propositional connectives
$\vee,\wedge,\neg,\supset$.
We denote as $\lm$ the modal extension of $\L$ with the modalities $B$
and $\n$.  We say that a formula $\vfi\in\lm$ has \emph{(modal) depth} $i$
(with $i\geq 0$) if each subformula in $\vfi$ lies within the scope of at
most $i$ modalities, and there exists a subformula in $\vfi$ which lies
within the scope of exactly $i$ modalities.

We denote as $\lms$ the set of \emph{subjective} $\mbnf$ formulas, i.e.\
the subset of formulas from $\lm$ in which each occurrence of a
propositional symbol lies within the scope of at least one modality, and
with $\lmf$ the set of \emph{flat} $\mbnf$ formulas, that is the set of
formulas from $\lm$ in which each propositional symbol lies within the
scope of exactly one modality.  We call a modal formula $\varphi$ from
$\lm$ \emph{positive} (resp.\ \emph{negative}) if the modality $\n$ (resp.\
$B$) does not occur in $\varphi$.  $\lb$ denotes the set of positive
formulas from $\lm$, while $\lbs$ denotes the set of positive formulas from
$\lms$.  

We now recall the notion of $\mbnf$ model.  An \emph{interpretation} is a
set of propositional symbols. An \emph{$\mbnf$ structure} is a triple
$(I,M_b,M_n)$, where $I$ is an interpretation (also called initial world)
and $M_b,M_n$ are non-empty sets of interpretations (worlds).
Satisfiability of a formula in an $\mbnf$ structure is defined inductively
as follows:
\begin{enumerate}
\item if $\varphi$ is a propositional symbol, $\varphi$ is satisfied by
  $(I,M_b,M_n)$ iff $\varphi\in I$;
\item $\neg \varphi$ is satisfied by $(I,M_b,M_n)$ iff $\varphi$ is not
  satisfied by $(I,M_b,M_n)$;
\item $\varphi_1\wedge \varphi_2$ is satisfied by $(I,M_b,M_n)$ iff
  $\varphi_1$ is satisfied by $(I,M_b,M_n)$ and $\varphi_2$ is satisfied by
  $(I,M_b,M_n)$;
\item $\varphi_1\vee \varphi_2$ is satisfied by $(I,M_b,M_n)$ iff either
  $\varphi_1$ is satisfied by $(I,M_b,M_n)$ or $\varphi_2$ is satisfied by
  $(I,M_b,M_n)$;
\item $\varphi_1\supset \varphi_2$ is satisfied by $(I,M_b,M_n)$ iff either
  $\varphi_1$ is not satisfied by $(I,M_b,M_n)$ or $\varphi_2$ is satisfied
  by $(I,M_b,M_n)$;
\item $B\varphi$ is satisfied by $(I,M_b,M_n)$ iff, for every $J\in M_b$,
  $\varphi$ is satisfied by $(J,M_b,M_n)$;
\item $\n\:\varphi$ is satisfied by $(I,M_b,M_n)$ iff there exists $J\in
  M_n$ such that $\varphi$ is not satisfied by $(J,M_b,M_n)$.
\end{enumerate}

We write $(I,M_b,M_n)\models \varphi$ to indicate that $\varphi$ is
satisfied by $(I,M_b,M_n)$.  We say that a theory $\Sigma\subseteq\lm$ is
satisfied by $(I,M_b,M_n)$ (and write $(I,M_b,M_n)\models\Sigma$) iff each
formula from $\Sigma$ is satisfied by $(I,M_b,M_n)$.  If $\varphi\in\lms$,
then the evaluation of $\varphi$ is insensitive to the initial
interpretation $I$: thus, in this case we also write
$(M_b,M_n)\models\varphi$. Analogously, if $\varphi\in\lbs$, then the
evaluation of $\varphi$ is insensitive both to the initial interpretation
$I$ and to the set $M_n$, and we also write $M_b\models\varphi$.  If
$\varphi\in\L$ then the evaluation of $\varphi$ does not depend on the sets
$M_b,M_n$, and in this case we write $I\models\varphi$.

In order to relate $\mbnf$ structures to standard interpretation structures
in modal logic (i.e.\ Kripke structures), we remark that, due to the above
notion of satisfiability, we can consider the sets $M_b$, $M_n$ in an
$\mbnf$ interpretation structure as two distinct \emph{universal} Kripke
structures, i.e.\ possible-world structures in which each world is
connected to all worlds of the structure. In fact, since the accessibility
relation in such a structure is universal, without loss of generality it is
possible to identify a universal Kripke structure with the set of
interpretations contained in it.  We recall that the class of universal
Kripke structures characterizes the logic $\Sfive$ \cite[Theorem
7.52]{mare-trus-93}.

The nonmonotonic character of $\mbnf$ is obtained by imposing the following
preference semantics over the interpretation structures satisfying a given
theory. 

\begin{definition} \label{def-mbnf-sem}
  A structure $(I,M,M)$, where $M\neq\emptyset$, is an \emph{$\mbnf$ model}
  of a theory $\Sigma\subseteq\lm$ iff $(I,M,M)\models\Sigma$ and, for each
  interpretation $J$ and for each set of interpretations $M'$, if
  $M'\supset M$ then $(J,M',M)\not\models\Sigma$.
\end{definition}

We say that a formula $\varphi$ is \emph{entailed} (or \emph{logically
 implied}) by $\Sigma$ in $\mbnf$ (and write
$\Sigma\models_{\mbnf}\varphi$) iff $\varphi$ is satisfied by every $\mbnf$
model of $\Sigma$. In order to simplify notation, we denote the $\mbnf$
model $(I,M,M)$ with the pair $(I,M)$, and, if $\Sigma\in\lms$, we denote
$(I,M,M)$ with $M$, since in this case the evaluation of $\Sigma$ is
insensitive to the initial world $I$, namely, if $(I,M)$ is a model for
$\Sigma$, then, for each interpretation $J$, $(J,M)$ is a model for
$\Sigma$.

\begin{example} \label{exa-prel}
Let $\Sigma=\{\bb p\}$. The only \mbnf\ models for $\Sigma$ are of the form
$(I,M)$, with $M=\{I:I\models p\}$.  Hence, $\Sigma\models_\mbnf \bb p$,
and $\Sigma\models_\mbnf\neg \bb \psi$ for each $\psi\in\L$ such that the
propositional formula $p\supset \psi$ is not valid.  Therefore, the agent
modeled by $\Sigma$ has minimal belief, in the sense that she only believes
$p$ and the objective facts logically implied by $p$.  
\qed \end{example}

\begin{example}
Let $\Sigma= \{\n\: \married\supset \bb\:\hasnochildren\}$. It is easy to
see that the only models for $\Sigma$ are of the form $(I,M)$ such that
$M=\{I:I\models \hasnochildren\}$, since $\married$ can be assumed not to
hold by the agent modeled by $\Sigma$, which is then able to conclude
$B\:\hasnochildren$.  Notably, the meaning of $\Sigma$ is analogous to the
default rule $\frac{:\neg \married}{\hasnochildren}$ in Reiter's default
logic \cite{Lifs94}.  Also, let $\Sigma=\{\k\,{\it bird}\wedge\n\neg\,{\it
 flies}\supset \k\,{\it flies}, \k\,{\it bird}\}$.  In a way analogous to
the previous case, it can be shown that the only \mbnf\ models for $\Sigma$
are of the form $(I,M)$, with $M=\{I:I\models {\it bird}\wedge{\it
 flies}\}$. Therefore, $\Sigma\models_\mbnf \k\,{\it flies}$. As shown by
\citeA{Lifs94}, $\Sigma$ corresponds to the default theory $(\{\frac{{\it
  bird}:{\it flies}}{{\it flies}}\},{\it bird})$.  \qed
\end{example}

Given a set of interpretations $M$, $Th(M)$ denotes the set of formulas
$\bb\varphi$ such that $\bb\varphi\in\lb$ and $M\models \bb\varphi$.  Let
$M_1,M_2$ be sets of interpretations. We say that $M_1$ is
\emph{equivalent} to $M_2 $ iff $Th(M_1)=Th(M_2)$.

\begin{definition}
  A set of interpretations $M$ is \emph{maximal} iff, for each set
  of interpretations $M'$, if $M'$ is equivalent to $M$ then
  $M'\subseteq M$.
\end{definition}

It turns out that, when restricting to theories composed of subjective
positive formulas, \mbnf\ corresponds to the modal logic of minimal
knowledge due to \citeA{HaMo85n}, also known as ground
nonmonotonic modal logic $\Sfive_G$ \cite{Kami91,DoNR97}.
In fact, $\sfiveg$ is obtained from modal logic $\Sfive$
by imposing the following preference order over the universal Kripke
structures satisfying a theory $\Sigma\in\lb$: $M$ is a model for $\Sigma$
iff $M\models\Sigma$ and, for each $M'$, if $M'\models\Sigma$ then
$M'\not\supset M$ \cite{shoh-87}. In fact, it is immediate to see that the
$\mbnf$ semantics of theories composed of subjective positive formulas
corresponds to the above semantics according to $\Sfiveg$.  Hence, the
following property holds.

\begin{proposition} \label{pro-sfiveg}
Let $\Sigma\subseteq\lb$. Then, $M$ is an $\Sfive_G$ model for $\Sigma$
iff, for each $I$, $(I,M)$ is an $\mbnf$ model for
$\{B\vfi:\vfi\in\Sigma\}$.
\end{proposition}

The previous proposition implies that, when $\Sigma\subseteq\lbs$, a set of
interpretations $M$ satisfying $\Sigma$ is compared with all other sets of
interpretations satisfying $\Sigma$, while, in the case
$\Sigma\subseteq\lm$, $M$ is only compared with the sets $M'$ such that
$(M',M)$ satisfies $\Sigma$.

Hence, the main difference between \mbnf\ and $\Sfive_G$ lies in the fact
that in $\Sfive_G$ all models are maximal with respect to set containment
(or minimal with respect to the objective knowledge which holds in the
model), while in \mbnf\ this property is not generally true. E.g., the
theory $\Sigma=\{\n\:\married \vee \bb\:\married\}$ has two types of models,
for each possible choice of the initial world $J$: $(J,M_1)$, where $M_1$
corresponds to the set of all interpretations (which represents the case in
which $\married$ is not assumed to hold); and $(J,M_2)$, where
$M_2=\{I:I\models \married\}$.  Namely, if $\married$ is assumed to hold,
then $\Sigma$ forces one to conclude $\bb\:\married$:
that is, the initial assumption is \emph{justified} by the knowledge
derived on the basis of such an assumption \cite{LiSh92}.
We remark that, by Proposition~\ref{pro-sfiveg}, the interpretation of the
$\mbnf$ operator $B$ exactly corresponds to the interpretation of the
modality $\bb$ in $\Sfive_G$.


%\input{a2m}
\section{Relating MBNF to Autoepistemic Logic}

In this section we study the relationship between autoepistemic logic and
$\mbnf$.  First, we briefly recall Moore's autoepistemic logic ($\ael$).
In order to keep notation to a minimum, we change the language of $\ael$,
using the modality $\bb$ instead of $L$. Thus, in the following a formula
of $\ael$ is a formula from $\lb$.

\begin{definition}
A propositionally consistent set of formulas $T\subset\lb$ is a
\emph{stable expansion} for a set of initial knowledge $\Sigma \subseteq
\lb$ if $T$ satisfies the following equation:
\begin{equation} \label{eqn-ael}
T = Cn(\Sigma \cup \{ \bb\varphi \mid \varphi \in T \}\cup
\{ \neg \bb\varphi \mid \varphi \not\in T \} )
\end{equation}
where $Cn(S)$ denotes the propositional deductive closure of the modal
theory $S\subseteq\lb$.
\end{definition}

Given a theory $\Sigma\subseteq\lb$ and a formula $\varphi\in\lb$, we write
$\Sigma\models_\ael \varphi$ iff $\varphi$ belongs to all the stable
expansions of $\Sigma$.  Each stable expansion $T$ is a \emph{stable set}
according to the following definition \cite{Stal93}.

\begin{definition} \label{def-stable}
A modal theory $T \subseteq \L_B$ is a \emph{stable set} if
\begin{enumerate}
\item $T=Cn(T)$;
\item for every $\varphi \in \L_B$, if $\varphi \in T$ then $B\varphi 
  \in T$; 
\item for every $\varphi \in \L_B$, if $\varphi \not \in T$ then $\neg
  B\varphi \in T$.
\end{enumerate}
\end{definition}

We recall that a stable set $T$ corresponds to a maximal universal Kripke
structure $M_T$ such that $T$ is the set of formulas satisfied by $M_T$
\cite{mare-trus-93}.  With the term {\em $\ael$ model} for $\Sigma$ we will
thus refer to a set of interpretations $M$ whose set of theorems $Th(M)$
corresponds to a stable expansion for $\Sigma$ in $\ael$.

Finally, notice that we have adopted the notion of \emph{consistent}
autoepistemic logic \cite{mare-trus-93}, i.e.\ in~(\ref{eqn-ael}) we do not
allow the inconsistent theory $T=\lb$ composed of all modal formulas to be
a (possible) stable expansion. The results presented in this section can be
easily extended to this case (corresponding to Moore's original proposal):
however, this requires to slightly change the semantics of $\mbnf$,
allowing in Definition~\ref{def-mbnf-sem} the empty set of interpretations
to be a possible component of $\mbnf$ structures.

In the following, we use the term \emph{embedding} (or translation) to
indicate a transformation function $\tau(\cdot)$ for modal theories.  We
are interested in finding a \emph{faithful} embedding
\cite{Gott95,Schw96,Janh98}, in the following sense: $\tau(\cdot)$ is a
faithful embedding of $\ael$ into $\mbnf$ if, for each theory
$\Sigma\subseteq \lb$ and for each model $M$, $M$ is an $\ael$ model for
$\Sigma$ iff $M$ is an $\mbnf$ model for $\tau(\Sigma)$.

It is already known that $\ael$ theories can be embedded into $\mbnf$
theories. In particular, it has been proven \cite{LiSh92,ScTr94} that
$\ael$ theories with no nested occurrences of $\bb$ (called \emph{flat}
theories) can be embedded into $\mbnf$; now, since in $\ael$ any theory
can be transformed into an equivalent flat theory (which has in general
size exponential in the size of the initial theory), it follows that any
$\ael$ theory can be embedded into $\mbnf$.

However, we now prove a much stronger result: negation as
failure in $\mbnf$ \emph{exactly} corresponds to negative introspection in
$\ael$, i.e.\ $\ael$'s modality $\neg \bb$ and $\mbnf$'s modality $\n$ are
semantically equivalent. Hence, such a correspondence is not only limited
to modal theories without nested modalities, and induces a polynomial-time
embedding of \emph{any} $\ael$ theory into $\mbnf$.

We first define the translation $\tau(\cdot)$ of modal theories from
$\ael$ to $\mbnf$ theories.
% and its inverse $\trael(\cdot)$. 

\begin{definition}
Let $\varphi\in\lb$. Then, $\tau(\varphi)$ is the $\mbnf$ formula
obtained from $\varphi$ by substituting each occurrence of $\bb$ with
$\neg\n$.  Moreover, if $\Sigma\subseteq\lb$, then $\tau(\Sigma)$
denotes the $\mbnf$ theory $\{B\tau(\varphi)|\varphi\in\Sigma\}$.
\end{definition}

We now show that the translation $\tau(\cdot)$ embeds $\ael$ theories into
$\mbnf$.  To this aim, we exploit the semantic characterization of $\ael$
defined by \citeA{Schw92a}. Roughly speaking, according to such
a preference semantics over possible-world structures, an $\ael$ model for
$\Sigma$ is a set of interpretations $M$ satisfying $\Sigma$ such that, for
any interpretation $J$ not contained in $M$, the pair $(J,M)$ does not
satisfy $\Sigma$. Formally:

\begin{proposition} \cite[Proposition 4.1]{Schw92a} \label{lem-ael-sem}
  Let $\Sigma\subseteq\lb$. Then, $M$ is an $\ael$ model for $\Sigma$ iff,
  for each interpretation $I\in M$, $(I,M)\models \Sigma$ and, for each
  interpretation $J\not\in M$, $(J,M)\not\models\Sigma$.
\end{proposition}

In the following, we say that an occurrence of a subformula $\psi$ in a
formula $\vfi\in\lm$ is \emph{strict} if it does not lie within the scope
of a modal operator.  E.g., let $\sigma= B\vfi\wedge \n(B\psi\vee\xi)$. The
occurrence of $B\vfi$ in $\sigma$ is strict, while the occurrence of
$B\psi$ is not strict.

\begin{theorem}
Let $\Sigma\subseteq\lb$. Then, $M$ is an $\ael$ model for $\Sigma$ iff,
for each $I$, $(I,M)$ is an $\mbnf$ model of $\tau(\Sigma)$.
\end{theorem}
\begin{proof}  
\emph{If part.} Suppose $(I,M)$ is an $\mbnf$ model of $\tau(\Sigma)$.
Then, for each $M'\supset M$, $(M',M)\not\models\tau(\Sigma)$. Since
$\tau(\Sigma)$ is a set of formulas of the form $B\vfi$, where $\vfi$ does
not contain any occurrence of the operator $B$, it follows that, for each
subformula of the form $\n\:\vfi$ occurring in $\tau(\Sigma)$,
$(M',M)\models\n\:\vfi$ iff $(M,M)\models\n\:\vfi$. Now let
$B\vfi\in\tau(\Sigma)$, let $\vfi'$ denote the propositional formula
obtained from $\vfi$ by replacing each strict occurrence in $\vfi$ of a
formula of the form $\n\:\psi$ with $\true$ if $(M,M)\models\n\:\psi$ and
with $\false$ otherwise, and let $\Sigma'=\{\vfi' :
B\vfi\in\tau(\Sigma)\}$. Now suppose there exists an interpretation $J$
such that $J\models\Sigma'$ and $J\not\in M$. Then, from the definition of
satisfiability in $\mbnf$ structures it follows that
$(M\cup\{J\},M)\models\tau(\Sigma)$, thus contradicting the hypothesis that
$(I,M)$ is an \mbnf\ model for $\tau(\Sigma)$. Hence,
$M=\{I:I\models\Sigma'\}$. Now consider a pair $(J,M)$: again, from the
definition of satisfiability in $\mbnf$ structures it follows immediately
that $(J,M) \models\Sigma$ iff $J\models\Sigma'$. And since $M$ contains
all the interpretations satisfying $\Sigma'$, it follows that, for each
interpretation $J\not\in M$, $(J,M)\not\models\Sigma$, therefore by
Proposition~\ref{lem-ael-sem} it follows that $M$ is an $\ael$ model for
$\Sigma$.

\emph{Only-if part.} Suppose $M$ is an $\ael$ model for $\Sigma$.  Then, by
Proposition~\ref{lem-ael-sem}, for each interpretation $I\in M$,
$(I,M)\models\Sigma$ and, for each interpretation $J\not\in M$,
$(J,M)\not\models\Sigma$.  For each $\vfi\in\Sigma$, let $\vfi''$ denote
the propositional formula obtained from $\vfi$ by replacing each strict
occurrence of a formula of the form $B\psi$ with $\true$ if $M\models
B\psi$ and with $\false$ otherwise, and let $\Sigma''=\{\vfi'' :
\vfi\in\Sigma\}$. Then, suppose there exists an interpretation $J$ such
that $J\models\Sigma''$ and $J\not\in M$. Then, from the definition of
satisfiability in $\mbnf$ structures it follows that $(J,M)\models\Sigma$,
thus contradicting the hypothesis that $M$ is an \ael\ model for $\Sigma$.
Hence, $M=\{I:I\models\Sigma''\}$. Now suppose that, for some
interpretation $I$, $(I,M)$ is not an \mbnf\ model for $\tau(\Sigma)$.
Then, there exists $M'\supset M$ such that $(M',M)\models\tau(\Sigma)$.
From the definition of $\tau(\cdot)$, it follows that each interpretation
in $M'$ satisfies $\Sigma''$, and, since $M'\supset M$, there exists
$J\not\in M$ such that $J\models\Sigma''$.  Contradiction. Therefore,
$(I,M)$ is an \mbnf\ model for $\Sigma$.  \qed
\end{proof}

We remark that the above theorem could alternatively be proved from the
fact that the $K$-free fragment of the logic $\mknf$ \cite{Lifs91} is
equivalent to $\ael$, which is stated (although without proof) by
\citeA[page 123]{ScTr94}, and from the correspondence between $\mbnf$ and
$\mknf$ \cite{Lifs94}.

The previous theorem implies that the interpretation of the modality $\n$
in $\mbnf$ and of the modal operator in autoepistemic logic are the same.
This property extends previous results relating $\mbnf$ with $\ael$
\cite{LiSh92,LiSc93,Chen94}, and has interesting consequences both in the
logic programming framework and in nonmonotonic reasoning.  In particular,
since $\mbnf$ generalizes the stable model semantics for logic programs
\cite{gelf-lifs-88}, the above result strengthens the idea that $\ael$ is
the true logic of negation as failure (as interpreted according to the
stable model semantics).  Moreover, positive theories have the same
interpretation both in $\mbnf$ and in the logic of minimal knowledge
$\Sfive_G$ \cite{HaMo85n}: consequently, the logic $\mbnf$ generalizes both
Halpern and Moses' $\Sfive_G$ and Moore's $\ael$.


%\input{reas}
\section{Reasoning in MBNF}

In this section we present algorithms for reasoning in propositional
$\mbnf$: in particular, we study the entailment problem in $\mbnf$. From
now on, we assume to deal with {\em finite} $\mbnf$ theories $\Sigma$,
therefore we refer to a single formula $\sigma$ (which corresponds to the
conjunction of all the formulas contained in the finite theory $\Sigma$).

\subsection{Characterizing MBNF Models}

We now present a finite characterization of the $\mbnf$ models of a formula
$\sigma\in\lm$.  As in several methods for reasoning in nonmonotonic modal
logics \cite{gott-92-b,mare-trus-93,eite-gott-92-b,niem-92,DoNR97},
the technique we employ is based on the definition of a correspondence
between the preferred models of a theory and the partitions of the set of
modal subformulas of the theory.  In fact, such partitions can be used in
order to provide a finite characterization of a universal Kripke structure:
specifically, a partition satisfying certain properties identifies a
particular universal Kripke structure $M$, by uniquely determining a
propositional theory
such that $M$ is the set of all interpretations satisfying such a theory.

We extend such known techniques in order to deal with the preference
semantics of $\mbnf$. In particular, we characterize the properties that a
partition of modal subformulas of a formula $\sigma\in\lm$ must satisfy in
order to identify an $\mbnf$ model for $\sigma$. In this way, we provide a
method that does not rely on a modal logic theorem prover, but reduces the
problem of reasoning in a bimodal logic to a number of reasoning problems
in propositional logic.

First, we introduce some preliminary definitions.  We call a formula of the
form $B\vfi$ or $\n\:\vfi$, with $\vfi\in\lm$, a \emph{modal atom}.

\begin{definition}
  Let $\sigma\in\lm$. We call the set of modal atoms occurring in $\sigma$
  the \emph{modal atoms of $\sigma$} (and denote such a set as
  $MA(\sigma)$).
\end{definition}

\begin{definition} \label{def-substitute-partition}
  Let $\sigma\in\lm$ and let $(P,N)$ be a partition of a set of modal
  atoms.  We denote as $\sigma(P,N)$ the formula obtained
  from $\sigma$ by substituting each strict occurrence in $\sigma$ of a
  formula in $P$ with $\true$, and each strict occurrence in $\sigma$ of a
  formula in $N$ with $\false$.
\end{definition}

Observe that only the occurrences in $\sigma$ of modal subformulas which
are not within the scope of another modality are replaced; notice also
that, if $P\cup N$ contains $MA(\sigma)$, then $\sigma(P,N)$ is a
propositional formula. In this case, the pair $(P,N)$ identifies a guess on
the modal subformulas from $\sigma$, i.e.\ $P$ contains the modal
subformulas of $\sigma$ assumed to hold, while $N$ contains the modal
subformulas of $\sigma$ assumed not to hold.

\begin{definition} \label{def-ob}
Let $\sigma\in\lm$ and let $(P,N)$ be a partition of $MA(\sigma)$. We
denote as $\ob$ the propositional formula
\[ \ob =  \bigwedge_{\bb\varphi\in P}\varphi(P,N)  \]
\end{definition}

Roughly speaking, the propositional formula $\ob$ represents the
``objective knowledge'' implied by the guess $(P,N)$ on the formulas of the
form $B\vfi$ belonging to $P$. From the semantic viewpoint, in each
structure $(I,M,M')$ satisfying the guess on the modal atoms given by
$(P,N)$, the propositional formula $\ob$ constrains the interpretations of
$M$, since in each such structure the propositional formula $\ob$ must be
satisfied by each interpretation $J\in M$, i.e.\ $J\models \ob$.

\begin{example}
Let 
\[ \sigma = (\bb a\vee \n(b\wedge c)) \wedge d\wedge \neg \bb(\neg f
\vee g) \]
Then, $MA(\sigma) = \{ \bb a, \n(b\wedge c),\k(\neg f\vee g)\}$.
Now suppose that
\begin{eqnarray*}
P & = & \{\k a, \n(b\wedge c)\}\\
N & = & \{\k(\neg f \vee g)\}
\end{eqnarray*}
Then, $\sigma(P,N) = (\true\vee\true)\wedge d \wedge \neg\false$ (which is
equivalent to $d$), and $\ob = a$.
\qed
\end{example}

\begin{definition} \label{def-first-induces}
  We say that a pair of sets of interpretations $(M,M')$
  \emph{induces} the partition $(P,N)$ of $MA(\sigma)$ if, for each modal
  atom $\xi\in MA(\sigma)$, $\xi\in P$ iff $(M,M')\models \xi$.
\end{definition}

\begin{lemma} \label{lem-nuovo}
Let $\vfi\in\lm$, let $I$ be an interpretation, let $M,M'$ be sets of
interpretations, and let $(P,N)$ be the partition induced by $(M,M')$ on a
set of modal atoms $S$.
Then, $(I,M,M')\models \vfi$ iff $(I,M,M')\models\vfi(P,N)$.
\end{lemma}
\begin{proof}
Follows immediately from Definitions~\ref{def-substitute-partition}
and~\ref{def-first-induces}, and from the definition of satisfiability in
$\mbnf$ structures.  
\qed \end{proof}

We now show that, if $(I,M)$ is an $\mbnf$ model for $\sigma$ which induces
the partition $(P,N)$ of $\masi$, then the formula $\ob$ completely
characterizes the set of interpretations $M$.

\begin{theorem} \label{lem-mbnf-obp}
  Let $\sigma\in\lm$, let $(I,M)$ be an $\mbnf$ model for $\sigma$, and let
  $(P,N)$ be the partition of $MA(\sigma)$ induced by $(M,M)$.  Then,
  $M=\{J:J\models\ob\}$.
\end{theorem}
\begin{proof}
Let $M'=\{J:J\models\ob\}$. Since $(M,M)$ induces the partition $(P,N)$, by
Definition~\ref{def-first-induces} it follows that each interpretation in
$M$ must satisfy $\ob$, hence $M\subseteq M'$.  Now suppose $M\subset M'$,
and consider the structure $(I,M',M)$. We prove that each modal atom
$\xi\in MA(\sigma)$ belongs to $P$ iff $(I,M',M)\models \xi$. The proof is
by induction on the depth of formulas in $MA(\sigma)$. 

First, consider a modal atom $\n\:\psi$ such that $\psi\in\L$: from
the definition of satisfiability of a formula in an $\mbnf$ structure, it
follows immediately that $\n\:\psi\in P$ iff $(I,M',M)\models\n\:\psi$.
Then, consider a modal atom $\bb\psi$ such that $\psi\in\L$: if $\bb\psi\in
P$, then, by definition of $\ob$, the propositional formula
$\ob\supset\psi$ is valid, therefore $(I,M',M)\models \bb\psi$. If
$\bb\psi\in N$, then there exists an interpretation $J$ in $M$ such that
$J\not\models \psi$, and since $M'\supset M$, it follows that
$(I,M',M)\not\models \bb\psi$.  Hence, each modal atom $\xi\in MA(\sigma)$
of depth 1 belongs to $P$ iff $(I,M',M)\models \xi$.

Suppose now that $\xi\in P$ iff $(I,M',M)\models \xi$ for each modal atom
$\xi$ in $MA(\sigma)$ of depth less or equal to $i$. Consider a modal atom
$\bb\psi$ of $MA(\sigma)$ of depth $i+1$: by the induction hypothesis, and
by Lemma~\ref{lem-nuovo}, $(I,M',M)\models \bb\psi$ iff $M'\models
\bb(\psi(P,N))$. Now, if $\bb\psi\in P$, then, by definition of $\ob$,
the propositional formula $\ob\supset\psi(P,N)$ is valid, and since
$M'=\{J:J\models\ob\}$, it follows that $M'\models \bb(\psi(P,N))$, which
in turn implies $(I,M',M)\models \bb\psi$; on the other hand, if
$\bb\psi\in N$, then there exists an interpretation $J$ in $M$ such that
$(J,M,M)\not\models \psi$, hence, by the induction hypothesis and
Lemma~\ref{lem-nuovo}, $J\not\models \psi(P,N)$. Now, since $M'\supset M$,
it follows that $M'\not\models \bb(\psi(P,N))$, hence $(I,M',M)\not\models
\bb\psi$. In the same way it is possible to show that a modal atom of the
form $\n\:\psi$ of depth $i+1$ belongs to $P$ iff $(I,M',M)\models
\n\:\psi$. 

We have thus proved that each modal atom $\xi\in MA(\sigma)$ belongs to $P$
iff $(I,M',M)\models \xi$: this in turn implies that
$(I,M',M)\models\sigma$ iff $I\models\sigma(P,N)$, and since by hypothesis
$(I,M,M)$ satisfies $\sigma$ and $(P,N)$ is the partition of $\masi$
induced by $(M,M)$, by Lemma~\ref{lem-nuovo} it follows that
$I\models\sigma(P,N)$. Therefore, $(I,M',M)\models\sigma$, which
contradicts the hypothesis that $(I,M)$ is an $\mbnf$ model for
$\sigma$. Consequently, $M'=M$, which proves the thesis.  
\qed \end{proof}

Informally, the above theorem states that each $\mbnf$ model for $\sigma$
can be associated with a partition $(P,N)$ of the modal atoms of $\sigma$;
moreover, the propositional formula $\ob$ exactly characterizes the set of
interpretations $M$ of an $\mbnf$ model $(I,M)$, in the sense that $M$ is
the set of \emph{all} interpretations satisfying $\ob$. This provides a
finite way to describe all $\mbnf$ models for $\sigma$.

We now define the notion of a partition of a set of modal atoms induced by a
pair of propositional formulas.

\begin{definition} \label{def-induces}
  Let $\sigma\in\lm$, $\vfi_1,\vfi_2\in\L$. We denote as
  $\parti(\sigma,\vfi_1,\vfi_2)$ the partition of $MA(\sigma)$ induced by
  $(M_1,M_2)$, where $M_1 = \{I:I\models\vfi_1\}$, $M_2 =
  \{I:I\models\vfi_2\}$.
\end{definition}

In order to simplify notation, we denote as $\parti(\sigma,\vfi)$ the
partition $\parti(\sigma,\vfi,\vfi)$. The following theorem provides a
constructive way to build the partition $\parti(\sigma,\vfi,\psi)$.

\begin{theorem} \label{thm-constr}
Let $\sigma\in\lm$, $\vfi,\psi\in\L$. Let $(P,N)$ be the partition of
$MA(\sigma)$ built as follows:
\begin{enumerate}
\item start from $P = N = \emptyset$;
\item for each modal atom $B\xi$ in $MA(\sigma)$ such that $\xi(P,N)\in\L$,
  if the propositional formula $\vfi\supset\xi(P,N)$ is valid, then add
  $B\xi$ to $P$, otherwise add $B\xi$ to $N$;
\item for each modal atom $\n\:\xi$ in $MA(\sigma)$ such that
  $\xi(P,N)\in\L$, if the propositional formula $\psi\supset\xi(P,N)$ is
  not valid, then add $\n\:\xi$ to $P$, otherwise add $\n\:\xi$ to $N$;
\item iteratively apply the above rules until $P\cup N = MA(\sigma)$.
\end{enumerate}
Then, $(P,N) = \parti(\sigma,\vfi,\psi)$.
\end{theorem}
\begin{proof}
The proof is by induction on the structure of the formulas in $MA(\sigma)$.
First, from the fact that $\parti(\sigma,\vfi,\psi)$ is the partition
induced by $(M,M')$, with $M = \{I : I \models \vfi \}$, $M' = \{I : I
\models \psi \}$, and from the definition of satisfiability in $\mbnf$
structures, it follows that, if $\xi\in\L$, then $(M,M')\models B\xi$ if
and only if $\vfi\supset\xi$ is a valid propositional formula, and
$(M,M')\models \n\:\xi$ if and only if $\psi\supset\xi$ is not a valid
propositional formula. Therefore, $(P,N)$ agrees with
$\parti(\sigma,\vfi,\psi)$ on all modal atoms of modal depth 1.  Suppose
now that $(P,N)$ and $\parti(\sigma,\vfi,\psi)$ agree on all modal atoms of
modal depth less or equal to $i$. Consider a modal atom $B\xi$ of
$MA(\sigma)$ of modal depth $i+1$. From Lemma~\ref{lem-nuovo} and from the
definition of satisfiability in $\mbnf$ structures, it follows that
$(M,M')\models B\xi$ if and only if
$\vfi\supset\xi(\parti(\sigma,\vfi,\psi))$ is a valid propositional
formula, and since by Definition~\ref{def-substitute-partition} the value
of the formula $\xi(\parti(\sigma,\vfi,\psi))$ only depends on the guess of
the modal atoms of modal depth less or equal to $i$ in
$\parti(\sigma,\vfi,\psi)$, by the induction hypothesis it follows that
$\xi(\parti(\sigma,\vfi,\psi)) = \xi(P,N)$, hence $B\xi$ belongs to $P$ if
and only if $(M,M')\models B\xi$. Analogously, it can be proven that any
modal atom of depth $i+1$ of the form $\n\:\xi$ belongs to $P$ if and only
if $(M,M')\models \n\:\xi$. Therefore, $(P,N)$ and
$\parti(\sigma,\vfi,\psi)$ agree on all modal atoms of modal depth $i+1$.  
\qed \end{proof}  

The algorithms we present in the following for reasoning in $\mbnf$ use the
above shown properties of partitions of modal subformulas of a formula
$\sigma$, together with additional conditions on such partitions (that vary
according to the different classes of theories accepted as inputs), in
order to identify all the $\mbnf$ models for $\sigma$. 

As for the entailment problem $\sigma \models_{\mbnf} \varphi$, we point
out that the occurrences of $\n$ in $\varphi$ are equivalent to occurrences
of $\neg B$, since in each $\mbnf$ model for $\sigma$ both modalities in
$\varphi$ are evaluated on the same set of interpretations.  Therefore, as
in the original formulation of $\mbnf$ \cite{Lifs94}, we restrict query
answering in $\mbnf$ to positive formulas.

Let $\vfi\in\lb$, $\psi\in\L$, and $M=\{J : J\models\psi\}$. We denote as
$\vfi(\psi)$ the propositional formula obtained from $\vfi$ by substituting
each strict occurrence of a modal atom $\bb\xi$ of $\vfi$ with $\true$ if
$M\models \bb\xi$, and with $\false$ otherwise. It can be immediately
verified that $\vfi(\psi)=\vfi(\parti(\vfi,\psi))$.

\begin{theorem} \label{thm-query-mbnf}
  Let $\sigma,\vfi\in\lm$. Let $(I,M)$ be an $\mbnf$ model for $\sigma$ and
  let $(P,N)$ be the partition of $MA(\sigma)$ induced by $(M,M)$. Then,
  $\varphi$ is satisfied by $(I,M,M)$ iff $I\models\varphi(\ob)$.
\end{theorem}
\begin{proof}
The proof follows immediately from the fact that, by
Theorem~\ref{thm-constr}, $\varphi(\ob)=\varphi(\parti(\vfi,\ob))$,
%where $(P_\vfi,N_\vfi)$ is the partition of modal atoms of $MA(\vfi)$
%induced by $(M,M)$, 
and from Lemma~\ref{lem-nuovo}.  
\qed \end{proof}

We now show that the entailment problem in $\mbnf$ is related to the
membership problem for stable sets \cite{Gott95}, which in turn is related
to the notion of (objective) kernel that has been used to characterize
stable expansions of autoepistemic theories \cite{mare-trus-93}.

\begin{definition}
Let $\psi \in \L$. We denote as $\ST(\psi)$ the (unique) stable set
$T\subseteq\lb$ such that
\[T\cap \L=\{\varphi\in\L|\psi\supset\varphi {\rm ~is~valid} \}\]
\end{definition}

\begin{theorem}
  Let $\sigma\in\lm$, $\vfi\in\lbs$. Then, $\sigma\not\models_\mbnf\vfi$
  iff there exists an $\mbnf$ model $(I,M)$ for $\sigma$ such that
  $\vfi\not\in\ST(\ob)$, where $(P,N)$ is the partition of $MA(\sigma)$
  induced by $(M,M)$.
\end{theorem}
\begin{proof}
Let $M=\{I:I\models\ob\}$: from the above definition and
Definition~\ref{def-stable}, it follows immediately that $\ST(\ob)=Th(M)$.
Therefore, if $\vfi\in\lbs$ then $(I,M,M)\models\vfi$ iff $\vfi\in
\ST(\ob)$. \qed
\end{proof}


\subsection{Reasoning in Propositional MBNF}

We now define a deductive method for reasoning in general propositional
$\mbnf$ theories. Specifically, we present the algorithm \mbnf-Not-Entails,
reported in Figure~\ref{fig-gen}, for computing entailment in $\mbnf$.

\begin{figure}
\underline{\hspace \textwidth}
%\hline
\begin{center}
\begin{minipage}{10cm}
%\boxcolumn{\vspace{-1ex}
\begin{tabbing}
{\bf Algorithm} \mbnf-Not-Entails($\sigma,\varphi$)\\ 
{\bf Input:} formula $\sigma\in\lm$, formula $\varphi\in\lb$;\\
{\bf Output:} \true\ if $\sigma \not\models_{\mbnf}\varphi$, \false\
otherwise.\\ 
{\bf begin}\\
%compute $MA(\sigma)$;\\
{\bf if }\={\bf there exists} partition $(P,N)$ of $MA(\sigma)$\\
{\bf such that}\\
\>(a) $(P,N) = \partiob$ {\bf and}\\
\>(b) $\sigma(P,N) \wedge \neg \vfi(\ob)$ is satisfiable {\bf and}\\
\>(c) {\bf for }\={\bf each} partition $(P',N')\neq(P,N)$ of $MA(\sigma)$,\\
\>\>(c1) $\sigma(P',N')$ is not satisfiable {\bf or}\\
\>\>(c2) $(P',N')\neq \partiobp$ {\bf or}\\
\>\>(c3) $\ob \wedge \neg \obp$ is satisfiable\\
{\bf then return} \true\\
{\bf else return} \false\\
{\bf end}
\end{tabbing} %%\vspace{-1em}}\vspace{-0.5em}
\end{minipage}
\end{center}
\underline{\hspace \textwidth}
%\hline
\caption{Algorithm $\mbnf$-Not-Entails.}
\label{fig-gen}
\end{figure}

The algorithm exploits the finite characterization of $\mbnf$ models given
by Theorem~\ref{lem-mbnf-obp} and an analogous finite characterization,
in terms of partitions of $MA(\sigma)$, of all the models relevant for
establishing whether a partition $(P,N)$ of $MA(\sigma)$ identifies an
$\mbnf$ model.

The algorithm checks whether there exists a partition $(P,N)$ of
$MA(\sigma)$ satisfying the three conditions (a), (b), (c).  Intuitively,
the partition cannot be self-contradictory (condition (a)): in particular,
the condition $(P,N) = \partiob$ establishes that the objective knowledge
implied by the partition $(P,N)$ (that is, the formula $\ob$) identifies a
set of interpretations $M=\{I:I\models\ob\}$ such that $(M,M)$ induces the
same partition $(P,N)$ on $MA(\sigma)$.  Moreover, the partition must be
consistent with $\sigma$ and $\neg\vfi$ (condition (b)): such a condition
implies that there exists an interpretation $I$ such that both $\sigma$ is
satisfied in $(I,M,M)$ and $\vfi$ is not satisfied in the structure
$(I,M,M)$. Finally, condition~(c) corresponds to check whether such a
structure $(I,M,M)$ identifies an $\mbnf$ model for $\sigma$ according to
Definition~\ref{def-mbnf-sem}, i.e.\ whether there is no pair $(J,M')$
such that $M'\supset M$ and $(J,M',M)$ satisfies $\sigma$. Again, the
search of such a structure is performed by examining whether there exists a
partition of $MA(\sigma)$, different from $(P,N)$, which does not satisfy
any of the conditions (c1), (c2), (c3).

We illustrate the algorithm through the following simple example.

\begin{example}
Suppose 
\begin{eqnarray*}
\sigma & = & \bb (a\vee\bb b)\wedge (\n (c\vee \neg d)\vee\bb \nn\: b)
\wedge c \\
\vfi & = & \neg B b \vee (\neg b \wedge B(a\wedge b))
\end{eqnarray*}
Then, $MA(\sigma) = \{ \bb (a\vee \bb b), \bb b, \n(c\vee\neg d), \bb\nn\:b,
\n\:b \}$.  Now suppose that $(P,N)=(P_1,N_1)$, where
\begin{eqnarray*}
P_1 & = & \{ \bb (a\vee \bb b), \n(c\vee \neg d), \n\:b \} \\
N_1 & = & \{ \bb b, \bb\nn\:b  \}
\end{eqnarray*}
Then, $\sigma(P,N) = \true\wedge(\true\vee\false)\wedge c$ (which is
equivalent to $c$), and $\ob = a\vee\false$ (which is equivalent to $a$).
Now, let $M=\{I:I\models a\}$: it is easy to see that $(M,M)$ satisfies the
modal atoms in $P$, while it does not satisfy the modal atoms in $N$, hence
$(P,N) = \partiob$, thus satisfying condition (a) of the algorithm. Then,
since $a\supset a\wedge b$ is not a valid propositional formula,
$M\not\models \bb(a\wedge b)$, hence $\neg \vfi(\ob)= \neg(\true\vee(\neg b
\wedge \false))$, which is equivalent to $\false$. Therefore, $\sigma(P,N)
\wedge \neg \vfi(\ob)$ is not satisfiable, thus condition (b) does not
hold.

Suppose now that $(P,N)=(P_2,N_2)$, where
\begin{eqnarray*}
P_2 & = & \{ \bb (a\vee \bb b), \n(c\vee \neg d),  \bb b, \bb\nn\:b\}\\
N_2 & = & \{ \n\:b \}
\end{eqnarray*}
Then, $\sigma(P,N) = \true\wedge(\true\vee\true)\wedge c$ (which is
equivalent to $c$), and $\ob = (a\vee\true) \wedge b \wedge \true$, which
is equivalent to $b$.  Again, it is easy to see that $(P,N) = \partiob$,
thus satisfying condition (a) of the algorithm. Then, since $b\supset
a\wedge b$ is not a valid propositional formula, $\neg \vfi(\ob)=
\neg(\false\vee(\neg b \wedge \false))$, which is equivalent to
$\true$. Hence, $\sigma(P,N) \wedge \neg \vfi(\ob)$ is equivalent to $c$,
which implies that condition (b) holds.  Finally, it is easy to verify that
either condition (c1) or condition (c2) holds for each partition of
$MA(\sigma)$ different from $(P_2,N_2)$, with the exception of $(P_1,N_1)$.
So let $(P',N')=(P_1,N_1)$: as shown before, $\obp$ is equivalent to $a$,
hence $\ob \wedge \neg \obp$ is equivalent to $b\wedge\neg a$, therefore
condition (c3) holds for $(P',N')=(P_1,N_1)$, which implies that condition
(c) holds for $(P,N)=(P_2,N_2)$. Consequently,
$\mbnf$-Not-Entails($\sigma,\vfi$) returns $\true$.  
In fact, the partition $(P_2,N_2)$ identifies the set of $\mbnf$ models for
$\sigma$ $(I,M)$ such that $I$ is an interpretation satisfying $c$ and
$M=\{I:I\models b\}$. Each such model does not satisfy the query $\vfi$:
indeed, it can immediately be verified that, for each interpretation $I$,
$(I,M,M)\not\models\neg\bb b \vee (\neg b \wedge \bb(a\wedge b))$, since
$M\not\models\bb(a\wedge b)$ and $M\models\bb b$.
\qed \end{example}

To prove correctness of the algorithm $\mbnf$-Not-Entails
we need the following preliminary lemma.

\begin{lemma} \label{lem-same-partition}
Let $\sigma\in\lm$, and let $(P,N)$ be the partition
of $\masi$ induced by $(M',M)$. Let $M''=\{I:I\models \ob\}$. Then,
$(P,N)$ is the partition induced by $(M'',M)$.
\end{lemma}
\begin{proof}
The proof is by induction on the depth of the modal atoms of $\masi$.  Let
$\n\:\psi\in \masi$ such that $\psi\in\L$: then, $(M',M)\models\n\:\psi$
iff there exists an interpretation $I\in M$ such that $I\not\models\psi$,
therefore $(M',M)\models \n\:\psi$ iff $(M'',M)\models \n\:\psi$. Now let
$B\psi\in\masi$ such that $\psi\in\L$: by Definition~\ref{def-ob},
$(M',M)\models B\psi$ iff the propositional formula $\ob\supset\psi$ is
valid, and since $M''=\{I:I\models \ob\}$, it follows that $(M',M)\models
B\psi$ iff $(M'',M)\models B\psi$.

Now suppose that, for each modal atom $\xi$ of depth $i$, $(M',M)\models
\xi$ iff $(M'',M)\models \xi$, and let $(P',N')$ denote the partition of
the modal atoms in $\masi$ of depth less or equal to $i$ induced by
$(M',M)$.
First, consider a modal atom $\n\:\psi$ of depth $i+1$. Then, by
Lemma~\ref{lem-nuovo}, $(M',M)\models \n\:\psi$ iff $(M',M)\models
\n(\psi(P',N'))$ and, by the inductive hypothesis and
Lemma~\ref{lem-nuovo}, $(M'',M)\models \n\:\psi$ iff $(M'',M)\models
\n(\psi(P',N'))$. Then, since $\psi$
has depth $i$, $\psi(P',N')$ is a propositional formula, hence
$(M',M)\models\n(\psi(P',N'))$ iff there exists an interpretation $I\in M$
such that $I\not\models\psi(P',N')$, which immediately implies that
$(M',M)\models \n\:\psi$ iff $(M'',M)\models \n\:\psi$.
Now consider a modal atom $B\psi$ of depth $i+1$. Then, by
Lemma~\ref{lem-nuovo}, $(M',M)\models B\psi$ iff $(M',M)\models
B(\psi(P',N'))$ and, by the inductive hypothesis and
Lemma~\ref{lem-nuovo}, $(M'',M)\models B\psi$ iff $(M'',M)\models
B(\psi(P',N'))$. By Definition~\ref{def-ob}, $(M',M)\models B\psi$ iff
the propositional formula $\ob\supset\psi(P',N')$ is valid, and since
$M''=\{I:I\models \ob\}$, it follows that $(M',M)\models B\psi$ iff
$(M'',M)\models B\psi$, which proves the thesis.
\qed \end{proof}

We are now ready to prove correctness of the algorithm \mbnf-Not-Entails.

\begin{theorem} \label{thm-mbnf-corr}
Let $\sigma\in\lm$, $\varphi\in\lb$. Then,
$\mbnf$-Not-Entails($\sigma,\varphi$) returns $\true$ iff
$\sigma\not\models_{\mbnf}\varphi$. 
\end{theorem}
\begin{proof}
{\em If part.}  Suppose $\sigma\not\models_\mbnf\vfi$. Then, there exists a
pair $(I,M)$ such that $(I,M)$ is an $\mbnf$ model for $\sigma$ and
$(I,M,M)\not\models\vfi$.  Let $(P,N)$ be the partition of $\masi$ induced
by $(M,M)$. By Theorem~\ref{lem-mbnf-obp}, $M=\{I:I\models \ob\}$.
Therefore, by Definition~\ref{def-induces}, $(P,N)=\partiob$. Then, since
$(I,M,M)\not\models\vfi$, by Theorem~\ref{thm-query-mbnf} it follows that
$I\not\models\vfi(\ob)$, and since $(I,M,M)\models\sigma$, by
Lemma~\ref{lem-nuovo} $I\models\sigma(P,N)$, therefore
$I\models\sigma(P,N)\wedge\neg\vfi(\ob)$.  Now suppose there exists a
partition $(P',N')$ of $\masi$ such that $(P',N')\neq(P,N)$ and none of
conditions (c1), (c2), and (c3) holds. Then, since $\sigma(P',N')$ is
satisfiable, there exists an interpretation $J$ such that $J\models
\sigma(P',N')$, and since $(P',N')=\partiobp$, from Lemma~\ref{lem-nuovo}
it follows that there exists an interpretation $J$ such that
$(J,M',M)\models \sigma$, where $M'=\{I:I\models \obp\}$. Then, since
condition (c3) does not hold, the propositional formula $\ob\supset\obp$ is
valid, which implies that $M'\supseteq M$. Now, if $M'=M$, then $(P',N')$
would be the partition induced by $(M,M)$, thus contradicting the
hypothesis $(P',N')\neq(P,N)$. Hence, $M'\supset M$, and since
$(J,M',M)\models\sigma$, it follows that $(I,M)$ is not an $\mbnf$ model
for $\sigma$. Contradiction. Consequently, condition (c) in the algorithm
holds, therefore \mbnf-Not-Entails($\sigma,\vfi$) returns \true.

{\em Only-if part.} Suppose \mbnf-Not-Entails($\sigma,\vfi$) returns \true.
Then, there exists a partition $(P,N)$ of $\masi$ such that conditions (a),
(b), and (c) hold. Let $M=\{I:I\models \ob\}$. Since $(P,N)=\partiob$, by
Definition~\ref{def-induces} $(P,N)$ is the partition induced by $(M,M)$.
And since $\sigma(P,N)\wedge\neg\vfi(\ob)$ is satisfiable, it follows that
there exists an interpretation $I$ such that $I\models\sigma(P,N)$ and
$I\not\models\vfi(\ob)$, hence, by Lemma~\ref{lem-nuovo},
$(I,M,M)\models\sigma$ and $(I,M,M)\not\models\vfi$.  Now suppose $(I,M)$
is not an $\mbnf$ model for $\sigma$. Then, there exists a set $M'$ and an
interpretation $J$ such that $M'\supset M$ and $(J,M',M)\models\sigma$. Let
$(P',N')$ be the partition of $\masi$ induced by $(M',M)$.  Since
$M=\{I:I\models \ob\}$, it follows that $M'$ contains at least one
interpretation $J$ which does not satisfy $\ob$, and since
$\ob=\bigwedge_{B\psi\in P} \psi(P,N)$, $J$ does not satisfy at least one
formula of the form $\psi(P,N)$ such that $B\psi\in P$. Therefore, $P'\neq
P$, which implies that $(P',N')\neq (P,N)$.  Then, since
$(J,M',M)\models\sigma$, by Lemma~\ref{lem-nuovo} $J\models\sigma(P',N')$,
hence $\sigma(P',N')$ is satisfiable.  Now let $M''=\{I:I\models \obp\}$.
By Lemma~\ref{lem-same-partition}, it follows that $(P',N')$ is the
partition induced by $(M'',M)$, therefore, by Definition~\ref{def-induces},
$(P',N')=\partiobp$. Moreover, since $M'\supset M$, it follows that the
propositional formula $\ob\supset\obp$ is valid, hence the formula
$\ob\wedge\neg\obp$ is unsatisfiable. Consequently, $(P',N')$ does not
satisfy condition (c) in the algorithm, thus contradicting the hypothesis.
Therefore, $(I,M)$ is an $\mbnf$ model for $\sigma$, and since
$(I,M,M)\not\models\vfi$, it follows that $\sigma\not\models_\mbnf\vfi$,
thus proving the thesis.
\qed \end{proof}

We point out the fact that the algorithm $\mbnf$-Not-Entails does not rely
on a theorem prover for a modal logic: thus, ``modal reasoning'' is not
actually needed for reasoning in $\mbnf$. This is an interesting
peculiarity that $\mbnf$ shares with other nonmonotonic modal formalisms,
like autoepistemic logic \cite{moor-85} or the autoepistemic logic of
knowledge \cite{Schw91}.


\subsection{Reasoning in Flat MBNF}

We now study reasoning in flat $\mbnf$ theories.  The main reason for
taking into account the flat fragment of $\mbnf$ is the fact that reasoning
in many of the best known nonmonotonic formalisms like default logic,
circumscription, and logic programming, can be reduced to reasoning in flat
$\mbnf$ theories \cite{Lifs94}.
 
It is known that, if $\sigma\in\lmf$ and $\vfi\in\lbs$, then it is possible
to reduce the entailment $\sigma\models_{\mbnf}\vfi$ to reasoning in logic
$\SfourF_{MDD}$, by translating $\mbnf$ formulas into unimodal formulas of
$\SfourF_{MDD}$ \cite{ScTr94}. Thus, the procedure for deciding entailment
in the logic $\SfourF_{MDD}$ presented by \citeA{mare-trus-93} can be
employed for computing the entailment $\sigma\models_{\mbnf}\vfi$.
In the following we study a more general problem, that is entailment
$\sigma\models_{\mbnf}\varphi$ in the case $\sigma\in\lmf$ and
$\varphi\in\lb$, and present a specialized algorithm for this problem,
which is simpler than the more general reasoning method for
$\SfourF_{MDD}$.

In Figure~\ref{fig-flat} we report the algorithm Flat-Not-Entails for
computing such an entailment. In the algorithm, $P_n$ denotes the subset of
modal atoms from $P$ prefixed by the modality $\n$, i.e.\ 
$P_n=\{\n\:\psi:\n\:\psi\in P\}$.

\begin{figure}
\underline{\hspace \textwidth}
%\hline
\begin{center}
\begin{minipage}{10cm}
%\boxcolumn{\vspace{-1ex}
\begin{tabbing}
{\bf Algorithm} Flat-Not-Entails($\sigma,\varphi$)\\ 
{\bf Input:} formula $\sigma\in\lmf$, formula $\varphi\in\lb$;\\
{\bf Output:} \true\ if $\sigma \not\models_{\mbnf}\varphi$, 
\false\ otherwise.\\
{\bf begin}\\
{\bf if }\={\bf there exists} partition $(P,N)$ of $MA(\sigma)$\\
{\bf such that}\\
\>(a) $(P,N) = \partiob$ {\bf and}\\
\>(b) $\sigma(P,N)\wedge\neg\varphi(\ob)$ is satisfiable {\bf and}\\
\>(c) $\sigma(P_n,N)\supset \bb(\ob)$ is valid in $\Sfive$\\
{\bf then return} \true\\
{\bf else return} \false\\
{\bf end}
\end{tabbing} %%\vspace{-1em}}\vspace{-0.5em}
\end{minipage}
\end{center}
\underline{\hspace \textwidth}
%\hline
\caption{Algorithm Flat-Not-Entails.}
\label{fig-flat}
\end{figure}

Informally, correctness of the algorithm Flat-Not-Entails is established by
the fact that, if $\sigma\in\lmf$, then (a), (b), and (c) are necessary and
sufficient conditions on a partition $(P,N)$ in order to establish whether
it is induced by a pair $(M,M)$ such that there exists an $\mbnf$ model for
$\sigma$ of the form $(I,M)$. In particular, condition (c) states that
$\bb(\ob)$ must be a consequence of $\sigma(P_n,N)$ in modal logic
$\Sfive$,\footnote{We denote as $\bb$ the modal operator used in $\Sfive$.}
since it can be shown that if $\sigma(P_n,N) \supset \bb(\ob)$ is not valid
in $\Sfive$, then the guess on the modal atoms of the form $\bb\varphi$
in $P$ is not minimal. We illustrate this fact through the following
example.

\begin{example}
Let 
\[\sigma=(\bb a\wedge\n(c\vee d))\vee(\bb(a\wedge b)\wedge\neg Bc)\vee Bc\]
and suppose 
\begin{eqnarray*}
P & = & \{\bb a,\bb(a\wedge b), \n(c\vee d) \}\\ 
N & = & \{ Bc\}
\end{eqnarray*}
Then, 
\[ \sigma(P_n,N) = (\bb a \wedge \true)\vee (\bb(a\wedge b)\wedge
\neg\false) \vee \false, \] 
which is propositionally equivalent to $Ba\vee B(a\wedge b)$, and
$\ob=a\wedge(a\wedge b)$, which is equivalent to $a\wedge b$. Now, $\bb a
\vee \bb(a\wedge b)\supset \bb(a\wedge b)$ is not valid in $\Sfive$, which
is proved by the fact that the set of interpretations $M'=\{I:I\models a\}$
is such that $M'\models(\bb a \vee \bb(a\wedge b))\wedge \neg \bb(a\wedge
b)$. Indeed, the set of interpretations $M'$ can be immediately used in
order to prove that $(P,N)$ does not identify any $\mbnf$ model for
$\sigma$. In fact, let $M=\{J:J\models a\wedge b\}$: it is immediate to see
that, for each interpretation $I$, $(I,M',M)\models \sigma$, and since
$M'\supset M$, $(I,M)$ is not an $\mbnf$ model for $\sigma$.  \qed
\end{example}

Finally, condition (b) corresponds to check whether there exists an
interpretation $I$ satisfying $\neg\vfi(\ob)$: in fact, if such an
interpretation exists, then $(I,M)$ is an $\mbnf$ model for $\sigma$ which
does not satisfy $\vfi$.

Therefore, the algorithms $\mbnf$-Not-Entails and Flat-Not-Entails only
differ in the way in which it is verified whether the $\mbnf$ structure
associated with a partition $(P,N)$ satisfies the preference semantics
provided by Definition~\ref{def-mbnf-sem}, which is implemented through
condition (c) in both algorithms.  In the algorithm $\mbnf$-Not-Entails,
a partition is checked against all other partitions of $MA(\sigma)$, while
in the algorithm Flat-Not-Entails it is sufficient to verify that the
partition $(P,N)$ satisfies a ``local'' property. As shown in the next
section, such a difference reflects the different computational properties
of the entailment problem in the two cases.

In order to establish correctness of the algorithm, we need a preliminary
lemma.

\begin{lemma}
\label{lem-flat}
Let $\sigma\in\lmf$ and let $(P,N)$ be the partition induced by a structure
$(M,M)$.  Then, $(I,M)$ is an $\mbnf$ model for $\sigma$ iff for each
$M'\supset M$ the positive formula $\sigma(P_n,N)$ is not satisfied by
$M'$.
\end{lemma}
\begin{proof}
Suppose $(I,M)$ is an $\mbnf$ model for $\sigma$, and let $(P,N)$ be the
partition induced by $(M,M)$.  Let $M'$ be any set of interpretations such
that $M'\supset M$.  Then, $(M',M)\not\models\sigma$.  Since
$\sigma\in\lmf$ and $M'\supset M$, this implies that for each modal atom
$\xi$ in $N$, $(M',M)\not\models \xi$.  Moreover, for each modal atom
$\n\:\psi\in P$, $(M',M)\models \n\:\psi$.  Therefore, by
Lemma~\ref{lem-nuovo}, $(M',M)\not\models\sigma(P_n,N)$. Now, since
$\sigma\in\lmf$, $\sigma(P_n,N)$ is a flat positive formula, hence its
satisfiability only depends on the structure $M'$, therefore
$M'\not\models\sigma(P_n,N)$.

Conversely, suppose $(I,M)$ is not an $\mbnf$ model for $\sigma$, and let
$(P,N)$ be the partition induced by $(M,M)$.  Then, there exists a set of
interpretations $M'$ such that $M'\supset M$ and $(M',M)\models\sigma$.
As shown before, this implies that the positive formula $\sigma(P_n,N)$
is satisfied by $M'$. \qed
\end{proof}

As observed in Section~\ref{sec-prel}, the class of universal Kripke
structures characterizes modal logic $\Sfive$. This immediately implies the
following property.

\begin{lemma} \label{lem-valid-sfive}
  A formula $\vfi\in\lbs$ is valid in $\Sfive$ iff, for each set of
  interpretations $M$, the formula $\neg\vfi$ is not satisfied by $M$.
\end{lemma}

Based on the above property, we are now able to prove correctness of the
algorithm Flat-Not-Entails.

\begin{theorem} \label{thm-flat}
  Let $\sigma\in\lmf$ and $\varphi\in\lb$. Then,
  Flat-Not-Entails($\sigma,\varphi$) returns \true\ iff
  $\sigma\not\models_{\mbnf}\varphi$.
\end{theorem}
\begin{proof}
{\em If-part.}  If $\sigma\not\models_{\mbnf}\varphi$, then there exists an
$\mbnf$ model $(I,M)$ for $\sigma$ such that $(I,M,M)\not\models\vfi$.  Let
$(P,N)$ be the partition of $MA(\sigma)$ induced by $(M,M)$.  From
Theorem~\ref{lem-mbnf-obp} it follows that $M=\{J:J\models\ob\}$.
Therefore, by Definition~\ref{def-induces}, $(P,N)=\partiob$, hence
condition~(a) in the algorithm holds.

Now let $\sigma'=\sigma(P_n,N)$, and suppose the formula $\sigma'\supset
\bb(\ob)$ is not valid in $\Sfive$. Then, since the formula
$\sigma'\supset\bb(\ob)$ belongs to $\lbs$, by Lemma~\ref{lem-valid-sfive}
it follows that there exists a set of interpretations $M'$ satisfying
$\sigma'\wedge\neg \bb(\ob)$. Let $(P',N')$ be the partition of
$MA(\sigma')$ induced by $(M',M')$, and let $M''=\{I:I\models\obp\}$. Since
%$M'\models\neg \bb(\ob)$ and
$\ob=\bigwedge_{B\vfi\in MA(\sigma')}\vfi$, by
Definition~\ref{def-ob} it follows that $\ob\supset\obp$ is a valid
propositional formula,
hence $M''\supseteq M$. Now, since by hypothesis $M'\models\neg\bb(\ob)$,
it follows that $M''\supset M$. Moreover, since
$\sigma'\in\lb$, by Lemma~\ref{lem-same-partition} it follows that
$(P',N')$ is the partition induced by $(M'',M'')$, and since
$M'\models\sigma'$ and $\sigma'$ is flat, $\sigma'(P',N')$ is equivalent to
$\true$, therefore $M''\models\sigma'(P',N')$ and, by
Lemma~\ref{lem-nuovo}, $M''\models\sigma'$. On the other hand, since
$M''\supset M$, by Lemma~\ref{lem-flat} it follows that
$M''\not\models\sigma'$.
Contradiction. Hence, $\sigma'\supset \bb(\ob)$ is
valid in $\Sfive$, consequently condition~(c) of the algorithm holds.

Finally, since $(I,M,M)\not\models\vfi$ and $M=\{J:J\models\ob\}$, by
Theorem~\ref{thm-query-mbnf} it follows that $I\not\models\vfi(\ob)$.
Moreover, since $(I,M,M)\models\sigma$, from Lemma~\ref{lem-nuovo} it
follows that $I\models\sigma(P,N)$, consequently
$I\models\sigma(P,N)\wedge\neg\vfi(\ob)$, hence the propositional formula
$\sigma(P,N)\wedge\neg\vfi(\ob)$ is satisfiable. Therefore, conditions (a),
(b), and (c) in the algorithm hold, which implies that
Flat-Not-Entails($\sigma,\vfi$) returns \true.

{\em Only-if-part.}  If Flat-Not-Entails($\sigma,\varphi$) returns \true,
then there exists a partition $(P,N)$ of $MA(\sigma)$ for which conditions
(a), (b), and (c) of the algorithm hold. Let $M=\{J:J\models \ob\}$. By
Definition~\ref{def-induces}, $(P,N)$ is the partition of $MA(\sigma)$
induced by $(M,M)$. Now, since $\sigma(P,N)\wedge\neg\varphi(\ob)$ is
satisfiable, there exists an interpretation $I$ such that
$I\models\sigma(P,N)$ and $I\models\neg\varphi(\ob)$, hence by
Lemma~\ref{lem-nuovo} $(I,M,M)\models\sigma$, and by
Theorem~\ref{thm-query-mbnf} $(I,M,M)\not\models\vfi$, therefore we only have
to show that $(I,M)$ is an $\mbnf$ model for $\sigma$.  So, let us suppose
$(I,M)$ is not an $\mbnf$ model for $\sigma$. Then, 
by Lemma \ref{lem-flat} there exists $M'\supset M$ such that
$\sigma(P_n,N)$ is satisfied in $M'$. Now, condition (c) in the algorithm
implies that $B(\ob)$ is a consequence of $\sigma(P_n,N)$ in $\Sfive$,
therefore $\ob$ is satisfied by each interpretation in $M'$, that is,
$M'\subseteq\{J:J\models \ob\}$, which contradicts the hypothesis
$M'\supset M=\{J:J\models \ob\}$.  Consequently,
$(I,M)$ is an $\mbnf$ model for $\sigma$.
\qed \end{proof}

We remark the fact that the algorithm Flat-Not-Entails can be seen as a
generalization of known methods for query answering in Reiter's default
logic, Moore's autoepistemic logic, and (disjunctive) logic programming
under the stable model (and answer set) semantics. In particular, condition
(c) in the algorithm can be seen as a generalization of the minimality
check used in (disjunctive) logic programming for verifying stability of a
model of a logic program \cite{gelf-lifs-90,gelf-lifs-91}.


%\input{compl}
\section{Complexity Results}
\label{sec-complexity}

In this section we provide a computational characterization of reasoning in
$\mbnf$.

We first briefly recall the complexity classes in the \emph{polynomial
 hierarchy}, and refer to~\cite{John90,Papa94} for further details about
the complexity classes mentioned in the paper.  P$^A$ (NP$^A$) is the class
of problems that are solved in polynomial time by deterministic
(nondeterministic) Turing machines using an oracle for $A$ (i.e.\ that
solves in constant time any problem in $A$).  The classes $\Sigma^p_k$,
$\Pi^p_k$ and $\Delta^p_k$ of the polynomial hierarchy are defined by
$\Sigma^p_0 = \Pi^p_0 = \Delta^p_0 =$ P, and for $k \geq 0$,
$\Sigma^p_{k+1} = {\rm NP}^{\Sigma^p_k}$, $\Pi^p_{k+1} = {\rm
 co}\Sigma^p_{k+1}$ and $\Delta^p_{k+1} = {\rm P}^{\Sigma^p_k}$.  In
particular, the complexity class $\sigmadue$ is the class of problems that
are solved in polynomial time by a nondeterministic Turing machine that
uses an NP-oracle, and $\pidue$ is the class of problems that are
complement of a problem in $\sigmadue$, while $\sigmatre$ is the class of
problems that are solved in polynomial time by a nondeterministic Turing
machine that uses an $\sigmadue$-oracle, and $\pitre$ is the class of
problems that are complement of a problem in $\sigmatre$.  It is generally
assumed that the polynomial hierarchy does not collapse: hence, a problem
in the class $\sigmadue$ or $\pidue$ is considered computationally easier
than a $\sigmatre$-hard or $\pitre$-hard problem.

As for the complexity of entailment in $\mbnf$, we start by establishing a
lower bound for reasoning in propositional $\mbnf$ theories.  To this end,
we exploit the correspondence between $\mbnf$ and the logic
of minimal knowledge $\sfiveg$ \cite{HaMo85n}.  Indeed, as stated by
Proposition~\ref{pro-sfiveg}, there is a one-to-one correspondence between
$\mbnf$ models and $\Sfive_G$ models of positive subjective theories.

\begin{lemma} \label{lem-mbnf-hard}
Let $\sigma\in\lms$ and let $\varphi\in\lb$. Then, the problem of deciding
whether $\sigma\models_{\mbnf}\varphi$ is $\pitre$-hard.
\end{lemma}
\begin{proof}
As shown by \cite{DoNR97}, entailment in $\Sfive_G$ is
$\pitre$-complete.  Therefore, by Proposition~\ref{pro-sfiveg}, for
subjective (and hence for general) $\mbnf$ theories, entailment is
$\pitre$-hard.  \qed \end{proof}

Then, we show that the entailment problem in propositional $\mbnf$ is
complete with respect to the class $\pitre$.

\begin{theorem}
Let $\sigma\in\lm$ and let $\varphi\in\lb$. Then, the problem of deciding
whether $\sigma\models_{\mbnf}\varphi$ is $\pitre$-complete.
\end{theorem}
\begin{proof}
Hardness with respect to $\pitre$ follows from
Lemma~\ref{lem-mbnf-hard}. As for membership in $\pitre$, we analyze the
complexity of the algorithm $\mbnf$-Not-Entails reported in Figure~1.  In
particular, observe that:
\begin{itemize}
\item given $(P,N)$, the formula $\ob$ can be computed in polynomial time
  with respect to the size of $P$. Moreover, by Lemma~\ref{thm-constr} it
  follows that, since $MA(\sigma)$ has size linear with respect to the size
  of $\sigma$, construction of the partition $\partiob$ can be performed
  through a linear number (with respect to the size of $\sigma$) of calls
  to an \np-oracle for propositional satisfiability. Therefore, condition
  (a) can be checked through a linear number (in the size of the input) of
  calls to an \np-oracle;
\item since $\vfi(\ob)=\vfi(\parti(\vfi,\ob))$, the formula $\neg
  \vfi(\ob)$ can be computed in time linear with respect to the size of
  $\vfi\wedge\ob$ using an \np-oracle. And since, given $\sigma$ and
  $(P,N)$, $\sigma(P,N)$ can be computed in polynomial time with respect to
  the size of the input, it follows that condition (b)
%%satisfiability of $\sigma(P,N) \wedge \neg \vfi(\ob)$ 
  can be computed through a linear number (in the size of the input) of
  calls to an \np-oracle;
\item given a partition $(P',N')$, each of the conditions (c1), (c2) and
  (c3) (analogous to conditions (a) and (b)) can be checked in polynomial
  time, with respect to the size of $\sigma$, using an \np-oracle.
  Therefore, since the guess of the partition $(P',N')$ of $MA(\sigma)$
  requires a nondeterministic choice, falsity of condition (c) can be
  decided in $\sigmadue$, which implies that verifying whether condition
  (c) holds can be decided in $\pidue$.
\end{itemize}

Since the guess of the partition $(P,N)$ of $MA(\sigma)$ requires a
nondeterministic choice, it follows that the algorithm $\mbnf$-Not-Entails,
if considered as a nondeterministic procedure, decides
$\sigma\not\models_\mbnf\vfi$ in nondeterministic polynomial time (with
respect to the size of $\sigma\wedge\vfi$), using a $\sigmadue$-oracle.
Thus, we obtain an upper bound of $\sigmatre$ for the non-entailment
problem, which implies that entailment in $\mbnf$ is in $\pitre$.  
\qed \end{proof}

The previous analysis also allows for a computational characterization of
the logic $\mknf$ \cite{Lifs91}, which is a slight modification of $\mbnf$.
Indeed, it is known \cite{Lifs94} that, for each theory
$\Sigma\subseteq\lm$, $M$ is an $\mknf$ model of $\Sigma$ iff, for each
interpretation $I$, $(I,M)$ is an $\mbnf$ model of the subjective theory
$\Sigma'=\{B\varphi\,:\,\varphi\in\Sigma\}$. Therefore, from
Proposition~\ref{pro-sfiveg} and from $\pitre$-hardness of entailment in
$\Sfiveg$ \cite{DoNR97}, it follows that entailment in $\mknf$ is
$\pitre$-hard. Then, since $\Sigma\models_{\mknf}\vfi$ iff
$\Sigma'\models_{\mbnf}B\vfi$ \cite{Lifs94}, it follows that entailment in
$\mknf$ can be polynomially reduced to entailment in $\mbnf$, hence such a
problem belongs to $\pitre$.  Therefore, the following property holds.

\begin{theorem}
Entailment in propositional $\mknf$ is $\pitre$-complete.
\end{theorem}

Finally, the previous theorem provides a computational characterization of
the logic of grounded knowledge and justified assumptions GK
\cite{LiSh92}. In fact, the logic GK can be considered as a syntactic
variant of the propositional fragment of $\mknf$.  Therefore, skeptical
entailment in GK is $\pitre$-complete.

\vskip 0.7\baselineskip

\noindent{\bf Remark.}  The computational properties of $\mbnf$ and its
variants relate such formalisms to ground nonmonotonic modal logics
\cite{eite-gott-92-b,DoNR97,Rosa99}.  Notably, ground nonmonotonic modal
logics share with $\mbnf$ the interpretation in terms of minimal knowledge
(or minimal belief) of the modality $B$; specifically, as already
mentioned, the propositional fragment of $\mbnf$ can be considered as built
upon $\Sfive_G$ by adding a second modality $\n$.  Therefore, it turns out
that, in the propositional case, adding a ``negation by default'' modality
to the $\Sfive$ logic of minimal knowledge does not increase the
computational complexity of reasoning, while adding a minimal knowledge
modality to $\ael$ does increase the complexity of deduction. We can thus
summarize as follows: minimal knowledge is computationally harder than
negation as failure. \qed

\vskip 0.7\baselineskip

We now study the complexity of entailment for flat $\mbnf$ theories.
First, it is known that, in the case of flat $\mbnf$ theories and
\emph{subjective} queries, entailment is $\Pi^p_2$-complete: membership in
the class $\Pi^p_2$ is a consequence of the fact that flat $\mknf$ theories
can be polynomially embedded into McDermott and Doyle's nonmonotonic modal
logic $\SfourF$ \cite[Proposition~3.2]{ScTr94}, whose entailment
problem is $\pidue$-complete \cite{mare-trus-93},
while $\Pi^p_2$-hardness follows from the existence of a
polynomial-time embedding of propositional default theories into flat
$\mbnf$ theories \cite{Lifs94}.  Therefore, the following
property holds.

\begin{proposition} \label{pro_flat}
Let $\sigma\in\lmf$ and let $\varphi\in\lbs$. Then, the problem of deciding
whether $\sigma\models_{\mbnf}\varphi$ is $\Pi_2^p$-complete.
\end{proposition}

As for complexity of entailment of generic queries with respect to flat
$\mbnf$ theories, we analyze the complexity of the algorithm
Flat-Not-Entails reported in Figure~2. As shown before, both condition (a)
and condition (b) can be checked through a linear number (with respect to
the size of the input) of calls to an NP-oracle. Moreover, validity in
modal logic $\Sfive$ is a coNP-complete problem \cite{HaMo92}.
Hence, each of the conditions in the algorithm can be computed through a
number of calls to an oracle for the propositional validity problem which
is polynomial in the size of the input, and since the guess of the
partition $(P,N)$ of $MA(\sigma)$ requires a nondeterministic choice, it
follows that the algorithm runs in $\sigmadue$.  Therefore, the following
property holds.

\begin{theorem} \label{thm-pidue}
Let $\sigma\in\lmf$ and let $\varphi\in\lb$. Then, the problem of deciding
whether $\sigma\models_{\mbnf}\varphi$ is $\Pi_2^p$-complete.
\end{theorem}
\begin{proof}
Membership of the problem to the class $\pidue$ is implied by the algorithm
Flat-not-entails, whereas $\pidue$-hardness is implied by Proposition
\ref{pro_flat}.
\qed \end{proof}

Hence, the algorithm Flat-Not-Entails is ``optimal'' in the sense that it
matches the lower bound for the entailment problem.

Finally, we remark that the subset of flat $\mbnf$ theories in conjunctive
normal form can be seen as a further extension of the framework of {\em
 generalized logic programming} introduced by \citeA{InSa94}, which in turn
is an extension of the disjunctive logic programming framework under the
stable model semantics \cite{gelf-lifs-91}.  Roughly speaking, flat $\mbnf$
theories in conjunctive normal form correspond to rules of generalized
logic programs in which propositional formulas (instead of literals) are
allowed as goals.  The above computational characterization implies that
such an extension of the framework of logic programming under the stable
model semantics does not affect the worst-case complexity of the entailment
problem, which is $\Pi^p_2$-complete just like entailment in logic programs
with disjunction under the stable model semantics \cite{EiGo95}. Such a
result extends analogous properties \cite{MaTR95} to the case of
disjunctive logic programs.


%\input{conclu}
\section{Conclusions}

In this paper we have investigated the problem of reasoning in the
propositional fragment of $\mbnf$. The main results presented can be
summarized as follows:

\begin{itemize}
\item the negation as failure modality $\n$ of $\mbnf$ exactly corresponds
  to negative introspection in $\ael$. This implies that the logic $\mbnf$
  can be viewed as the conservative extension of two different nonmonotonic
  modal logics: Halpern and Moses' logic of minimal knowledge $\Sfive_G$
  and Moore's $\ael$;
\item reasoning in the propositional fragment of $\mbnf$ lies at the third
  level of the polynomial hierarchy, hence (unless the polynomial hierarchy
  does not collapse) reasoning in $\mbnf$ is harder than reasoning in the
  best known propositional nonmonotonic logics, like default logic,
  autoepistemic logic, and circumscription;
\item we have defined methods for reasoning in $\mbnf$, which subsume and
  generalize well-known nonmonotonic reasoning algorithms used in logic
  programming \cite{gelf-lifs-91}, default logic \cite{gott-92-b}, and
  autoepistemic logic \cite{mare-trus-93};
\item we have studied the flat fragment of $\mbnf$ and its relationship
  with the logic programming paradigm.
\end{itemize}

As for the computational aspects of reasoning in $\mbnf$, the results
presented in Section~\ref{sec-complexity} prove that one source of
complexity is due to the presence of nested occurrences of modalities in
the theory, since reasoning in flat $\mbnf$ is computationally easier than
in the general case.

It can be proven that another source of complexity lies in the underlying
objective language. In fact, if we consider $\L'$ to be a tractable
fragment of propositional logic, then the complexity of reasoning in the
modal language $\lm'$ built upon $\L'$ is lower than in the general case.
In particular, it is easy to see that, under the assumption that entailment
in $\L'$ can be computed in polynomial time, the algorithm
$\mbnf$-Not-Entails provides an upper bound of $\pidue$ for
$\mbnf$-entailment in the fragment $\lm'$.

One possible development of the present work is towards the analysis of
reasoning about minimal belief and negation as failure in a first-order
setting: in particular, it should be interesting to see whether it is
possible to extend the techniques developed for the propositional case to a
more expressive language. A first attempt in this direction is reported by
\citeA{DoNR97b}.


\section*{Acknowledgments}

This research has been partially supported by Consiglio Nazionale delle
Ricerche, grant 203.15.10.


%\bibliography{medium-string,krdb,nmr,krric}
%\bibliographystyle{theapa}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Beringer \BBA\ Schaub}{Beringer \BBA\
  Schaub}{1993}]{BeSc93}
Beringer, A.\BBACOMMA\  \BBA\ Schaub, T. \BBOP1993\BBCP.
\newblock \BBOQ Minimal belief and negation as failure: a feasible
  approach\BBCQ\
\newblock In {\Bem Proc.\ of the 11th Nat.\ Conf.\ on Artificial Intelligence
  (AAAI'93)}, \BPGS\ 400--405.

\bibitem[\protect\BCAY{Bochman}{Bochman}{1995}]{Boch95}
Bochman, A. \BBOP1995\BBCP.
\newblock \BBOQ On bimodal nonmonotonic modal logics and their unimodal and
  nonmodal equivalents\BBCQ\
\newblock In {\Bem Proc.\ of the 14th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI'95)}, \BPGS\ 1518--1524.

\bibitem[\protect\BCAY{Chen}{Chen}{1994}]{Chen94}
Chen, J. \BBOP1994\BBCP.
\newblock \BBOQ The logic of only knowing as a unified framework for
  non-monotonic reasoning\BBCQ\
\newblock {\Bem Fundamenta Informaticae}, {\Bem 21}, 205--220.

\bibitem[\protect\BCAY{Donini, Nardi, \BBA\ Rosati}{Donini
  et~al.}{1997a}]{DoNR97b}
Donini, F.~M., Nardi, D., \BBA\ Rosati, R. \BBOP1997a\BBCP.
\newblock \BBOQ Autoepistemic description logics\BBCQ\
\newblock In {\Bem Proc.\ of the 15th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI'97)}, \BPGS\ 136--141.

\bibitem[\protect\BCAY{Donini, Nardi, \BBA\ Rosati}{Donini
  et~al.}{1997b}]{DoNR97}
Donini, F.~M., Nardi, D., \BBA\ Rosati, R. \BBOP1997b\BBCP.
\newblock \BBOQ Ground nonmonotonic modal logics\BBCQ\
\newblock {\Bem J.\ of Logic and Computation}, {\Bem 7\/}(4), 523--548.

\bibitem[\protect\BCAY{Eiter \BBA\ Gottlob}{Eiter \BBA\
  Gottlob}{1992}]{eite-gott-92-b}
Eiter, T.\BBACOMMA\  \BBA\ Gottlob, G. \BBOP1992\BBCP.
\newblock \BBOQ Reasoning with parsimonious and moderately grounded
  expansions\BBCQ\
\newblock {\Bem Fundamenta Informaticae}, {\Bem 17\/}(1,2), 31--54.

\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{Eiter \BBA\ Gottlob}{Eiter \BBA\ Gottlob}{1995}]{EiGo95}
Eiter, T.\BBACOMMA\  \BBA\ Gottlob, G. \BBOP1995\BBCP.
\newblock \BBOQ On the computational cost of disjunctive logic programming:
  propositional case\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem
  15\/}(3,4).

\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 \BBA\ Lifschitz}{Gelfond \BBA\
  Lifschitz}{1990}]{gelf-lifs-90}
Gelfond, M.\BBACOMMA\  \BBA\ Lifschitz, V. \BBOP1990\BBCP.
\newblock \BBOQ Logic programs with classical negation\BBCQ\
\newblock In {\Bem Proceedings of the Seventh International Conference on Logic
  Programming}, \BPGS\ 579--597. The {MIT} Press.

\bibitem[\protect\BCAY{Gelfond \BBA\ Lifschitz}{Gelfond \BBA\
  Lifschitz}{1991}]{gelf-lifs-91}
Gelfond, M.\BBACOMMA\  \BBA\ Lifschitz, V. \BBOP1991\BBCP.
\newblock \BBOQ Classical negation in logic programs and disjunctive
  databases\BBCQ\
\newblock {\Bem New Generation Computing}, {\Bem 9}, 365--385.

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

\bibitem[\protect\BCAY{Gottlob}{Gottlob}{1995}]{Gott95}
Gottlob, G. \BBOP1995\BBCP.
\newblock \BBOQ {NP} trees and {C}arnap's modal logic\BBCQ\
\newblock {\Bem J.\ of the ACM}, {\Bem 42\/}(2), 421--457.

\bibitem[\protect\BCAY{Halpern \BBA\ Moses}{Halpern \BBA\
  Moses}{1985}]{HaMo85n}
Halpern, J.~Y.\BBACOMMA\  \BBA\ Moses, Y. \BBOP1985\BBCP.
\newblock \BBOQ Towards a theory of knowledge and ignorance: Preliminary
  report\BBCQ\
\newblock In Apt, K.\BED, {\Bem Logic and models of concurrent systems}.
  Springer-Verlag.

\bibitem[\protect\BCAY{Halpern \BBA\ Moses}{Halpern \BBA\ Moses}{1992}]{HaMo92}
Halpern, J.~Y.\BBACOMMA\  \BBA\ Moses, Y. \BBOP1992\BBCP.
\newblock \BBOQ A guide to completeness and complexity for modal logics of
  knowledge and belief\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 54}, 319--379.

\bibitem[\protect\BCAY{Inoue \BBA\ Sakama}{Inoue \BBA\ Sakama}{1994}]{InSa94}
Inoue, K.\BBACOMMA\  \BBA\ Sakama, C. \BBOP1994\BBCP.
\newblock \BBOQ On positive occurrences of negation as failure\BBCQ\
\newblock In {\Bem Proc.\ of the 4th Int.\ Conf.\ on the Principles of
  Knowledge Representation and Reasoning (KR'94)}, \BPGS\ 293--304. Morgan
  Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Janhunen}{Janhunen}{1998}]{Janh98}
Janhunen, T. \BBOP1998\BBCP.
\newblock \BBOQ On the intertranslatability of autoepistemic, default and
  priority logics\BBCQ\
\newblock In {\Bem Proc.\ of the 6th European Workshop on Logics in Artificial
  Intelligence (JELIA'98)}, \BPGS\ 216--232.

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

\bibitem[\protect\BCAY{Kaminski}{Kaminski}{1991}]{Kami91}
Kaminski, M. \BBOP1991\BBCP.
\newblock \BBOQ Embedding a default system into nonmonotonic logics\BBCQ\
\newblock {\Bem Fundamenta Informaticae}, {\Bem 14}, 345--354.

\bibitem[\protect\BCAY{Levesque}{Levesque}{1990}]{Leve90}
Levesque, H.~J. \BBOP1990\BBCP.
\newblock \BBOQ All {I} know: a study in autoepistemic logic\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 42}, 263--310.

\bibitem[\protect\BCAY{Lifschitz \BBA\ Woo}{Lifschitz \BBA\ Woo}{1992}]{LiWo92}
Lifschitz, V.\BBACOMMA\  \BBA\ Woo, T. \BBOP1992\BBCP.
\newblock \BBOQ Answer sets in general nonmonotonic reasoning (preliminary
  report)\BBCQ\
\newblock In {\Bem Proc.\ of the 3rd Int.\ Conf.\ on the Principles of
  Knowledge Representation and Reasoning (KR'92)}, \BPGS\ 603--614. Morgan
  Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Lifschitz}{Lifschitz}{1991}]{Lifs91}
Lifschitz, V. \BBOP1991\BBCP.
\newblock \BBOQ Nonmonotonic databases and epistemic queries\BBCQ\
\newblock In {\Bem Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI'91)}, \BPGS\ 381--386.

\bibitem[\protect\BCAY{Lifschitz}{Lifschitz}{1994}]{Lifs94}
Lifschitz, V. \BBOP1994\BBCP.
\newblock \BBOQ Minimal belief and negation as failure\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 70}, 53--72.

\bibitem[\protect\BCAY{Lin \BBA\ Shoham}{Lin \BBA\ Shoham}{1992}]{LiSh92}
Lin, F.\BBACOMMA\  \BBA\ Shoham, Y. \BBOP1992\BBCP.
\newblock \BBOQ Epistemic semantics for fixed-point non-monotonic logics\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 57}, 271--289.

\bibitem[\protect\BCAY{Marek \BBA\ Truszczy\'{n}ski}{Marek \BBA\
  Truszczy\'{n}ski}{1993}]{mare-trus-93}
Marek, W.\BBACOMMA\  \BBA\ Truszczy\'{n}ski, M. \BBOP1993\BBCP.
\newblock {\Bem Nonmonotonic Logics -- Context-Dependent Reasoning}.
\newblock Springer-Verlag.

\bibitem[\protect\BCAY{Marek, Truszczy\'{n}ski, \BBA\ Rajasekar}{Marek
  et~al.}{1995}]{MaTR95}
Marek, W., Truszczy\'{n}ski, M., \BBA\ Rajasekar, A. \BBOP1995\BBCP.
\newblock \BBOQ Complexity of computing with extended propositional logic
  programs\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial intelligence}, {\Bem
  15\/}(3,4).

\bibitem[\protect\BCAY{Moore}{Moore}{1985}]{moor-85}
Moore, R.~C. \BBOP1985\BBCP.
\newblock \BBOQ Semantical considerations on nonmonotonic logic\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 25}, 75--94.

\bibitem[\protect\BCAY{Niemel{\"{a}}}{Niemel{\"{a}}}{1992}]{niem-92}
Niemel{\"{a}}, I. \BBOP1992\BBCP.
\newblock \BBOQ On the decidability and complexity of autoepistemic
  reasoning\BBCQ\
\newblock {\Bem Fundamenta Informaticae}, {\Bem 17\/}(1,2), 117--156.

\bibitem[\protect\BCAY{Papadimitriou}{Papadimitriou}{1994}]{Papa94}
Papadimitriou, C.~H. \BBOP1994\BBCP.
\newblock {\Bem Computational Complexity}.
\newblock Addison Wesley Publ.\ Co., Reading, Massachussetts.

\bibitem[\protect\BCAY{Reiter}{Reiter}{1990}]{Reit90}
Reiter, R. \BBOP1990\BBCP.
\newblock \BBOQ What should a database know?\BBCQ\
\newblock {\Bem J.\ of Logic Programming}, {\Bem 14}, 127--153.

\bibitem[\protect\BCAY{Rosati}{Rosati}{1997}]{Rosa97}
Rosati, R. \BBOP1997\BBCP.
\newblock \BBOQ Reasoning with minimal belief and negation as failure:
  {A}lgorithms and complexity\BBCQ\
\newblock In {\Bem Proc.\ of the 14th Nat.\ Conf.\ on Artificial Intelligence
  (AAAI'97)}, \BPGS\ 430--435. {AAAI} Press/The {MIT} Press.

\bibitem[\protect\BCAY{Rosati}{Rosati}{1999}]{Rosa99}
Rosati, R. \BBOP1999\BBCP.
\newblock \BBOQ Reasoning about minimal knowledge in nonmonotonic modal
  logics\BBCQ\
\newblock {\Bem J.\ of Logic, Language and Information}, {\Bem 8\/}(2),
  187--203.

\bibitem[\protect\BCAY{Schwarz}{Schwarz}{1991}]{Schw91}
Schwarz, G. \BBOP1991\BBCP.
\newblock \BBOQ Autoepistemic logic of knowledge\BBCQ\
\newblock In {\Bem Proc.\ of the 1st Int.\ Workshop on Logic Programming and
  Non-monotonic Reasoning (LPNMR'91)}, \BPGS\ 260--274. The {MIT} Press.

\bibitem[\protect\BCAY{Schwarz}{Schwarz}{1992}]{Schw92a}
Schwarz, G. \BBOP1992\BBCP.
\newblock \BBOQ Minimal model semantics for nonmonotonic modal logics\BBCQ\
\newblock In {\Bem Proc.\ of the 7th IEEE Sym.\ on Logic in Computer Science
  (LICS'92)}, \BPGS\ 34--43. IEEE Computer Society Press.

\bibitem[\protect\BCAY{Schwarz}{Schwarz}{1996}]{Schw96}
Schwarz, G. \BBOP1996\BBCP.
\newblock \BBOQ On embedding default logic into {M}oore's autoepistemic
  logic\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 80}, 388--392.

\bibitem[\protect\BCAY{Schwarz \BBA\ Lifschitz}{Schwarz \BBA\
  Lifschitz}{1993}]{LiSc93}
Schwarz, G.\BBACOMMA\  \BBA\ Lifschitz, V. \BBOP1993\BBCP.
\newblock \BBOQ Extended logic programs as autoepistemic theories\BBCQ\
\newblock In {\Bem Proc.\ of the 2nd Int.\ Workshop on Logic Programming and
  Non-monotonic Reasoning (LPNMR'93)}, \BPGS\ 101--114. The {MIT} Press.

\bibitem[\protect\BCAY{Schwarz \BBA\ Truszczy\'nski}{Schwarz \BBA\
  Truszczy\'nski}{1994}]{ScTr94}
Schwarz, G.\BBACOMMA\  \BBA\ Truszczy\'nski, M. \BBOP1994\BBCP.
\newblock \BBOQ Minimal knowledge problem: a new approach\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 67}, 113--141.

\bibitem[\protect\BCAY{Shoham}{Shoham}{1987}]{shoh-87}
Shoham, Y. \BBOP1987\BBCP.
\newblock \BBOQ Nonmonotonic logics: Meaning and utility\BBCQ\
\newblock In {\Bem Proc.\ of the 10th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI'87)}, \BPGS\ 388--392.

\bibitem[\protect\BCAY{Stalnaker}{Stalnaker}{1993}]{Stal93}
Stalnaker, R. \BBOP1993\BBCP.
\newblock \BBOQ A note on non-monotonic modal logic\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 64\/}(2), 183--196.

\end{thebibliography}

\end{document}

