\documentstyle[jair,11pt,twoside,theorem,DEFS,epsfig,theapa]{article}
\newcommand{\square}{\Box}
\newcommand{\blacksquare}{\Box}
\input{diagramsN}

\ShortHeadings{Complexity of Prioritized Default Logics}{Rintanen}
\jairheading{9}{1998}{423-461}{8/98}{12/98}
\firstpageno{423}

\begin{document}

\bibliographystyle{theapa}

\title{Complexity of Prioritized Default Logics}
\author{\name Jussi Rintanen
 \email rintanen@informatik.uni-ulm.de \\
       \addr Universit{\"a}t Ulm \\
       Fakult{\"a}t f{\"u}r Informatik \\
       Albert-Einstein-Allee \\
       89069 Ulm, GERMANY
}

\maketitle

\begin{abstract}
In default reasoning, usually not all possible ways of resolving conflicts
between default rules are acceptable.
Criteria expressing acceptable ways of resolving the conflicts
may be hardwired in the inference mechanism, for example specificity
in inheritance reasoning can be handled this way,
or they may be given abstractly as an ordering on the default rules.
In this article we investigate formalizations of the latter approach
in Reiter's default logic.
Our goal is to analyze and compare the computational properties 
of three such formalizations in terms of their computational complexity:
the prioritized default logics of Baader and Hollunder, and Brewka,
and a prioritized default logic that is based on lexicographic comparison.
The analysis locates the propositional variants of these logics on
the second and third levels of the polynomial hierarchy, and identifies
the boundary between tractable and intractable inference for restricted
classes of prioritized default theories.
\end{abstract}

\section{Introduction}

Nonmonotonic logics and related systems for nonmonotonic and default
reasoning \cite{Reiter80,Moore85,McCarthy80}
were developed for representing knowledge and forms of reasoning
that are not conveniently expressible in monotonic logics, like
the first-order predicate logic or propositional logics.
In nonmonotonic logics inferences can be made on the basis of what cannot
be inferred from a set of facts.
When extending this set, some of the inferences may become invalid,
and hence the set of inferable facts does not monotonically increase.
For example, in the kind of reasoning expressed as inheritance
networks \cite{Horty94},
one network link may say that priests imbibe non-alcoholic beverages only.
This is, in the absence of contrary information, a sufficient reason
to conclude that a certain priest will not drink vodka.
Without contradiction, information stating that the priest does
drink vodka can be added, which retracts the previous conclusion.

The need to incorporate priority information to nonmonotonic logics
\cite{Lifschitz85,Brewka89,GP92,Ryan92,Brewka94:jelia,BH95:jar}
stems from the possibility that two default rules are in conflict.
One source of such priority information is the specificity of defaults.
When one rule says that priests usually do not drink and another says
that men usually do, inferences concerning male priests should be based
on the first one because it is more specific, as male priests are a small
subset of men.
Specificity as a basis for resolving conflicts between defaults has been
investigated in the framework of path-based inheritance theories \cite{Horty94}.
In general, however, priorities may come from different sources,
and therefore it is justified to investigate nonmonotonic reasoning with
an abstract notion of priorities as orderings on defaults.
In this setting the problem is to define what are the correct inferences
in the presence of priorities.
There have been many proposals of differing generality.
Preferred subtheories \cite{Brewka89} and ordered theory
presentations \cite{Ryan92} do not have as general a notion of defaults
as Reiter's default logic, and they can both be translated to
prerequisite-free normal default theories of a prioritized default logic
\cite{Rintanen97:pdl}.
Also the definitions of model minimization in conditional entailment
\cite{GP92} and in prioritized circumscription \cite{Lifschitz85} 
do not directly support defaults with prerequisites.

In this work we concentrate on Brewka's \citeyear{Brewka94:jelia}
and Baader and Hollunder's \citeyear{BH95:jar} proposals for incorporating
priorities to default logic,
as well as a proposal that uses lexicographic comparison \cite{Rintanen97:pdl}.
These three proposals address default reasoning with defaults that have
prerequisites.
Like earlier work on complexity of nonmonotonic logics
\cite{Kautz91,Stillman90,Gottlob92},
the purpose of our investigation is to point out fundamental differences
and similarities between these logics,
characterized by polynomial time translatability between their decision
problems,
and to identify restricted classes of default theories where reasoning
is tractable.
The first kind of results are useful for example when developing
theorem-proving techniques for the logics in question.
The inexistence of polynomial time translations between two decision
problems indicates that the techniques needed are likely to be different:
it is not feasible to solve one decision problem by simply translating
it to the other. Also, if polynomial time translations exist and they
turn out to be simple, there is often no reason to treat the decision
problems separately.
The second kind of results, identification of tractable cases, directly
give efficient, that is polynomial time, decision procedures for
prioritized reasoning in special cases. The utility of these algorithms
depends on the application at hand. In many cases the restrictions
that lead to polynomial time decision procedures are too severe
to make the procedures practically useful.
Even though nonmonotonic reasoning usually cannot be performed in
polynomial time, new developments in implementation techniques
have made it possible to solve problems that previously
were too difficult \cite{NS96}.
Hence there are some prospects of making nonmonotonic reasoning practically
useful, which makes the problem of introducing priority information
in nonmonotonic reasoning more acute. This paper can be seen as giving
guidelines in that direction.

The decision problems of propositional default logic are located on the
second level of the polynomial hierarchy \cite{Gottlob92},
and hence they do not belong to the classes NP or co-NP unless
the polynomial hierarchy collapses to its first level.
The proof of this result suggests that reasoning in default logic
cannot be performed in polynomial time simply by restricting the formulae
in default theories to a tractable subclass of propositional logic like
2-literal clauses \cite{EIS76} or Horn clauses \cite{Dowling84}.
This fact can be seen as a consequence of the possibility of conflicting
defaults. A conflict between defaults gives rise to multiple extensions
because a case analysis on alternative ways of resolving the conflict
is required.
For a default theory of size $n$, the number of conflicts 
may be proportional to $n$, and each conflict may double
the number of extensions.
Hence the number of extensions can be proportional to $2^n$.
Priorities in many cases uniquely determine how a conflict between
defaults is resolved, and hence the case analyses that lead to an
exponential number of extensions can be avoided.
This gives rise to the question whether priorities would in some
cases produce a computational advantage in the sense that the decision problems
could be solved more efficiently than in the unprioritized case.
To investigate these questions we consider three definitions of priorities
in the framework of Reiter's default logic.

First we analyze
the computational complexity of two closely related
prioritized default logics \cite{Brewka94:jelia,BH95:jar}.
These logics are based on the semiconstructive definition of extensions
of default logic \cite{Reiter80}: the priorities control
the construction of extensions, ruling out those that do not respect
the priorities.
In the general case the complexity of the decision problems of these logics
equals the complexity of those of Reiter's default logic,
being complete for the second level of the polynomial hierarchy.
When the priorities are a total ordering on the defaults, the complexity
decreases by one level, leading to many tractable cases when
the propositional reasoning involved is tractable,
for example with Horn clauses or 2-literal clauses.
With arbitrary strict partial orders there is no similar decrease.

We continue by analyzing
a prioritized default logic that is based on comparing
the Reiter extensions of a default theory by lexicographic comparison
\cite{Rintanen97:pdl}.
The decision problem of this logic is harder than the decision problems
of Reiter's default logic, assuming that the polynomial hierarchy does not
collapse.
For default theories with a total priority relation some syntactically
restricted classes are easier than the corresponding unprioritized
ones, but in general even total priorities do not reduce the complexity
of the decision problems.
For partial priorities tractability can be achieved only with
extreme syntactic restrictions, the complexity being the same as with
the prioritized default logics by Brewka and by Baader and Hollunder.

\section{Preliminaries on Computational Complexity}\label{se:complexitytheory}

In this section we introduce some basic concepts in computational complexity.
For details see \cite{Balcazar88}.
The complexity class P consists of decision problems that are solvable
in polynomial time by a deterministic Turing machine.
NP is the class of decision problems that are solvable in polynomial time
by a nondeterministic Turing machine. The class co-NP consists
of problems the complements of which are in NP.
In general, the class co-C consists of problems the complements of which
are in the class C.
The polynomial hierarchy PH is an infinite hierarchy of complexity classes
$\Sigma^p_i$, $\Pi^p_i$ and $\Delta^p_i$ for all $i\geq 0$ that is
\index{$\Sigma^p_i$}\index{$\Pi^p_i$}\index{$\Delta^p_i$}
defined by using oracle Turing machines as follows.
\begin{displaymath}
\begin{array}{rclcrclcrcl}
\Sigma^p_0 & = & P && \Pi^p_0 & = & P && \Delta^p_0 & = & P \\
\Sigma^p_{i+1} & = & \mbox{NP}^{\Sigma^p_i} &&
\Pi^p_{i+1} & = & \mbox{co-}\Sigma^p_{i+1} &&
\Delta^p_{i+1} & = & P^{\Sigma^p_i}
\end{array}
\end{displaymath}
$C_1^{C_2}$ denotes the class of problems that is defined like
the class $C_1$ except that oracle Turing machines that use an oracle for
a problem in $C_2$ are used instead of Turing machines without such an oracle.
Oracle Turing machines with an oracle for a problem $B$ are like
ordinary Turing machines except that they may perform tests for membership
in $B$ with constant cost.
A problem $L$ is {\em Turing reducible}
to a problem $L'$ if there is an oracle Turing machine with an oracle for $L'$
that solves $L$.
The problem is Turing reducible in polynomial time if the oracle Turing
machine solves $L$ with a polynomial number of execution steps.
A problem $L$ is {\em $C$-hard} for a complexity class $C$
if all problems in $C$ are polynomial time {\em many-one reducible} to it;
that is, for all problems $L'\in C$
there is a function $f_{L'}$ that can be computed in polynomial time on
the size of its input and $f_{L'}(x)\in L$ if and only if $x\in L'$.
We say that the function $f_{L'}$ is a translation from $L'$ to $L$.
A problem is {\em $C$-complete} if it belongs to the class $C$ and is $C$-hard.

\section{Preliminaries on Default Logic}\label{se:dl}

Default logic is one of the main formalizations of nonmonotonic reasoning
\cite{Reiter80}.
A {\em default theory} $\Delta = \langle D,W\rangle$ consists of a set
of {\em default rules} $\defaultr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}$
where $\alpha$ (the {\em precondition}), $\gamma$ (the {\em conclusion})
and $\beta_i, i\in\{1,\ldots,n\}$ (the {\em justifications}) are formulae
of the classical propositional logic,
and a set $W$ of {\em objective facts} that also are formulae of the classical
propositional logic.
A default rule $\defr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}$ can be used
for inferring the fact $\gamma$ if $\alpha$ has been derived, and none of
the formulae $\neg\beta_1,\ldots,\neg\beta_n$ can be derived.
As derivability and underivability are mutually dependent,
there is circularity in the definition of what is derivable in default logic.
Unlike in monotonic logics, where the consequences of a set of formulae
is defined as the formulae that can be derived by using the axioms
of the logic and the inference rules,
the conclusions of a default theory $\Delta =\langle D,W\rangle$
are defined as fixpoints of a nonmonotonic operator.
The operator may have several fixpoints, none of which is the least
fixpoint, and different fixpoints can be seen as a result of applying
different mutually incompatible sets of default rules.
The fixpoints of the operator for a default theory are the {\em extensions}
of the default theory.

Informally, the construction of each extension of a default theory
starts from the objective facts $W$, and proceeds by adding conclusions
of default rules the preconditions of which have already been derived,
and the justifications of which have not been and will not later be contradicted.
The construction ends when no more defaults can be applied.

\newcommand{\male}{\ms{man}}
\newcommand{\priest}{\ms{priest}}
\newcommand{\drinksvodka}{\ms{drinks-vodka}}
\newcommand{\drinksvodkaII}{\ms{drinks-vodka}} % was adore babes
\newcommand{\drinksvodkaIII}{\ms{like-rock-n-roll}}

\begin{example}\label{ex:vodka}
Define $\Delta = \langle D,W\rangle$ by
\begin{eqnarray*}
D & = & \left\{ \ndefr{\priest}{\neg\drinksvodkaII}, \ndefr{\male}{\drinksvodkaII}, \ndefr{\priest}{\male} \right\}, \mbox{ and} \\
W & = & \{ \priest \}.
\end{eqnarray*}
A default $\ndefr{\alpha}{\beta}$ can be interpreted as saying that an
individual who has property $\alpha$, can be assumed to also have 
the property $\beta$ if this is consistent with what else is known.
The default theory $\Delta$ has two extensions, $E = \Cn{\{\priest,\male,\neg\drinksvodkaII\}}$ and $E' = \Cn{\{\priest,\male,\drinksvodkaII\}}$, that
represent the two possibilities of resolving the conflict between the first
two defaults in $D$. The extension $E$ corresponds to the choice to apply
the first default, and the extension $E'$ to the choice to apply the second.
\end{example}

The fixpoint definition of extensions is given next.
The language of the propositional logic is denoted by $\langcl$.
The closure of a set of formulae $S$ under logical consequence is
$\Cn{S} = \{ \phi\in\langcl | S\models\phi\}$.
The set $\{ \defaultr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma} | n\geq 0, \{\alpha,\beta_1,\ldots,\beta_n,\gamma\}\subseteq\langcl\}$
of default rules is denoted by $\langd$.
The {\em size} of a default theory $\langle D, W\rangle$
is the sum of the lengths of the formulae in $W$ and in defaults in $D$.
A default theory is finite if $D$ and $W$ are finite.


\begin{definition}[Reiter, 1980]\label{de:extension}
Let $\Delta = \langle D, W\rangle$ be a default theory.
For any set of formulae $S\subseteq\langcl$, let $\Gamma(S)$ be the smallest
set such that $W\subseteq \Gamma(S)$, $\Cn{\Gamma(S)} = \Gamma(S)$,
and if $\defaultr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}\in D$
and $\alpha\in \Gamma(S)$ and $\{\neg\beta_1,\ldots,\neg\beta_n\}\cap S=\emptyset$, then $\gamma\in \Gamma(S)$.
A set of formulae $E\subseteq\langcl$ is {\em an extension for} $\Delta$
if and only if $\Gamma(E) = E$.
\end{definition}

More procedural is the {\em semiconstructive} definition,
so called because it suggests a nondeterministic procedure
for computing extensions.

\begin{theorem}[Reiter, 1980]\label{th:semiconstructive}
Let $E\subseteq\langcl$ be a set of formulae, and
let $\Delta = \langle D,W\rangle$ be a default theory.
Define $E_0 = W$ and for all $i\geq 0$,
$E_{i+1} = \Cn{E_i}\cup\{ \gamma | \defr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma} \in D, \alpha\in E_i, \{\neg\beta_1,\ldots,\neg\beta_n\}\cap E=\emptyset\}$.
Then $E$ is an extension of $\Delta$ if and only if $E = \bigcup_{i\geq 0} E_i.$
\end{theorem}

The set of {\em generating defaults} of an extension identifies
the extension uniquely, and is of finite size whenever the number of
defaults is finite.

\begin{definition}[Reiter, 1980]\label{de:generatingdefaults}
Suppose $\Delta = \langle D, W\rangle$ is a default theory and $E$
is an extension of $\Delta$. The set of {\em generating defaults}
of $E$ with respect to $\Delta$ is
\[ \GD{E}{\Delta} = \left\{\left. \defaultr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}\in D \right| \alpha\in E \mbox{ and } \{\neg\beta_1,\ldots,\neg\beta_n\}\cap E=\emptyset\right\}. \]
\end{definition}

\begin{theorem}[Reiter, 1980]\label{th:generatingdefaults}
Suppose $E$ is an extension of a default theory $\Delta = \langle D,W\rangle$.
Then $E = \Cn{W\cup\{\gamma|\defaultr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}\in\GD{E}{\Delta}\}}$.
\end{theorem}

The standard consequence relations of default logic are
{\em cautious reasoning} $\models_c$ and {\em brave reasoning} $\models_b$.

\begin{definition}
Let $\Delta = \langle D,W\rangle$ be a default theory and $\phi\in\langcl$
a formula.
Then $\Delta\models_c\phi$ if and only if $\phi\in E$ for all extensions $E$
of $\Delta$,
and $\Delta\models_b\phi$ if and only if $\phi\in E$ for some extension $E$
of $\Delta$.
\end{definition}

The following terminology is used in referring to default rules of certain
syntactic forms.
Defaults of the form $\ndefaultr{\alpha}{\beta}$,  $\defaultr{\alpha}{\beta\conj\gamma}{\gamma}$,  $\defaultr{\top}{\beta_1,\ldots,\beta_n}{\gamma}$
are respectively {\em normal},
{\em seminormal}, and
{\em prerequisite-free}.
The symbol $\top$ denotes a valid formula.
Prerequisite-free defaults are often written without prerequisites as
$\defaultr{}{\beta_1,\ldots,\beta_n}{\gamma}$.
We shall sometimes denote sequences 
$\beta_1,\ldots,\beta_n$ of justifications
by $\sigma,\sigma',\sigma_1$ and so on.

Not all seminormal default theories have extensions,
but all {\em ordered} default theories do.
In some cases, a decision problem for a class of default theories is intractable,
but for the subclass in which the default theories are ordered,
it is tractable \cite{Kautz91}. In later sections we analyze the complexity
of decision problems both with and without the orderedness condition.

\begin{definition}[Etherington, 1987]
Let $\Delta = \langle D,W\rangle$ be a seminormal default theory.
Without loss of generality assume that all formulae are in clausal form.
The relations $\ll$ and $\underline{\ll}$ are defined as follows.
\begin{enumerate}
\item If $\alpha\in W$, then $\alpha = \alpha_1\disj\cdots\disj\alpha_n$ for
some $n\geq 1$. For all $\alpha_i,\alpha_j\in\{\alpha_1,\ldots,\alpha_n\}$
such that $\alpha_i\neq\alpha_j$, let $\neg\alpha_i\underline{\ll}\alpha_j$.
\item If $\delta\in D$, then $\delta = \defr{\alpha}{\beta\conj\gamma}{\beta}$.
Let $A$, $B$ and $G$ be the sets of literals of the clausal forms of
$\alpha$, $\beta$ and $\gamma$, respectively.
  \begin{enumerate}
  \item If $\alpha_i\in A$ and $\beta_j\in B$, let $\alpha_i\underline{\ll}\beta_j$.
  \item If $\gamma_i\in G$ and $\beta_j\in B$, let $\neg\gamma_i\ll\beta_j$.
  \item Also, $\beta = \beta_1\conj\cdots\conj\beta_m$ for some $m\geq 1$.
For each $i\leq m$, $\beta_i = \beta_{i,1}\disj\cdots\disj\beta_{i,m_i}$ where $m_i\geq 1$. Thus if $\beta_{i,j},\beta_{i,k}\in\{\beta_{1,1},\cdots,\beta_{m,m_m}\}$ and $\beta_{i,j}\neq\beta_{i,k}$, let $\neg\beta_{i,j}\underline{\ll}\beta_{i,k}$.
  \end{enumerate}
\item The following transitivity relations hold for $\ll$ and $\underline{\ll}$.
  \begin{enumerate}
  \item If $\alpha\underline{\ll}\beta$ and $\beta\underline{\ll}\gamma$, then $\alpha\underline{\ll}\gamma$.
  \item If $\alpha\ll\beta$ and $\beta\ll\gamma$, then $\alpha\ll\gamma$.
  \item If $\alpha\ll\beta$ and $\beta\underline{\ll}\gamma$ or $\alpha\underline{\ll}\beta$ and $\beta\ll\gamma$, then $\alpha\ll\gamma$.
  \end{enumerate}
\end{enumerate}

The default theory $\Delta$ is {\em ordered} if and only if
$\alpha\ll\alpha$ for no $\alpha$.
\end{definition}

According to Theorem 1 in \cite{Etherington87}, ordered default theories,
like normal default theories and unlike seminormal default theories in general,
have at least one extension.

\newcommand{\NPH}{{\small NP-hard}}
\newcommand{\coNPH}{{\small co-NP-hard}}
\newcommand{\PTIME}{{\small PTIME}}
\newcommand{\dleNPH}{{\small\bf NP-hard}}
\newcommand{\dlecoNPH}{{\small\bf co-NP-hard}}
\newcommand{\dlePTIME}{{\small\bf PTIME}}

\newcommand{\LPDL}{LPDL} % for lexicographic prioritized DL
\newcommand{\ksDLcoNPC}{K\&S}
\newcommand{\ksDLNPC}{K\&S}
\newcommand{\sDLcoNPC}{S}
\newcommand{\sDLNPC}{S}
\newcommand{\TPDLNPC}{total \LPDL}
\newcommand{\PDLPTIME}{\LPDL in P}

\newcommand{\prerequisitefree}{prerequisite-free }

\section{Prioritized Default Logics by Brewka and by Baader and Hollunder}\label{se:sncomplexity}

% These logics do not always have extension even when Reiter's default logic
% has: :a/c, :-c/-c, :-a/-a

Priorities in default logic have been investigated
by Baader and Hollunder \citeyear{BH95:jar} and Brewka \citeyear{Brewka94:jelia}.
They view priorities as information that selects which defaults
are applied next when constructing an extension.
Priorities are strict partial orders, that is, transitive and asymmetric
relations ${\cal P}$ on the defaults.
If $\delta{\cal P}\delta'$,
then the application of $\delta$ is more desirable than the application
of $\delta'$, and
the default $\delta$ is more significant or has a higher priority.
Brewka, as well as Baader and Hollunder, give a definition of preferred
extensions by modifying the semiconstructive definition of extensions
(Theorem \ref{th:semiconstructive}.)
The construction of an extension starts from the set $W$ of objective facts,
and proceeds in stages by repeatedly applying the highest priority applicable
defaults.
In this section we analyze the complexity of the associated decision problems.

\begin{definition}
A default $\defr{\alpha}{\beta}{\gamma}$ is {\em active} in $E\subseteq\langcl$
if $E\models\alpha$ and $E\not\models\neg\beta$ and $E\not\models\gamma$.
\end{definition}

\begin{definition}[Baader and Hollunder, 1995]\label{de:bh93}
Let $\langle D,W\rangle$ be a default theory and ${\cal P}$ a strict
partial order on $D$.
Let $E\subseteq\langcl$ be a set of formulae.
Define for all $i\geq 0$,
\begin{eqnarray*}
E_0 & = & W \\
E_{i+1} & = & E_i\cup\left\{ \gamma \left| \defr{\alpha}{\beta}{\gamma}\in D, E_i\models\alpha, E\not\models\neg\beta, \mbox{ no } \delta{\cal P}\defr{\alpha}{\beta}{\gamma} \mbox{ is active in } E_i\right.\right\}.
\end{eqnarray*}
Then $E$ is a ${\cal P}$-preferred$^{\ms{BH}}$ extension of $\langle D,W\rangle$ if and only if $E = \bigcup_{i\geq 0}\Cn{E_i}$.
\end{definition}

Brewka's definition is syntactically similar. We have expressed it in a way
that highlights the differences to Baader and Hollunder's definition.
The main difference is that the construction of a preferred extension
proceeds by applying defaults in an order specified by some strict total
order that extends the priorities.
Furthermore, Brewka gives his definition for normal default theories only, and
the consistency of justifications is tested against the sets $E_i$
instead of the set $E$.

\begin{definition}[Brewka, 1994]\label{de:b94}
Let $\langle D,W\rangle$ be a normal default theory and ${\cal P}$
a strict partial order on $D$.
Then $E\subseteq\langcl$ is a ${\cal P}$-preferred$^B$ extension of $\langle D,W\rangle$
if there is a strict total order ${\cal T}$ on $D$
such that ${\cal P}\subseteq{\cal T}$
and $E = \bigcup_{i\geq 0}\Cn{E_i}$ where for all $i\geq 0$,
\begin{eqnarray*}
E_0 & = & W \\
E_{i+1} & = & E_i\cup\left\{ \beta \left| \ndefr{\alpha}{\beta}\in D, E_i\models\alpha, E_i\not\models\neg\beta, \mbox{ no } \delta{\cal T}\ndefr{\alpha}{\beta} \mbox{ is active in } E_i \right.\right\}.
\end{eqnarray*}
We say that $E$ is generated by ${\cal T}$.
\end{definition}

The purpose of both of these definitions of preferred extensions is
to introduce a mechanism for resolving conflicts between defaults on
the basis of the priorities.
Different extensions represent different ways of resolving the conflicts.
The preferred extensions are a subset of all extensions of a default theory.

\begin{example}\label{ex:pvodka}
Let $\Delta = \langle D,W\rangle$ be a default theory
and ${\cal P}$ a strict partial order on $D$, where
\begin{eqnarray*}
D & = & \left\{ \ndefr{\priest}{\neg\drinksvodkaIII}, \ndefr{\male}{\drinksvodkaIII}, \ndefr{\priest}{\male} \right\},  \\
W & = & \{ \priest \}, \mbox{ and} \\
{\cal P} & = & \left\{ \left\langle\ndefr{\priest}{\neg\drinksvodkaIII}, \ndefr{\male}{\drinksvodkaIII}\right\rangle\right\}.
\end{eqnarray*}
The priorities ${\cal P}$ state that when reasoning about male priests,
information specific to priests should override information concerning
men in general.
Of the extensions $E = \Cn{\{\priest,\male,\neg\drinksvodkaIII\}}$ and $E' = \Cn{\{\priest,\male,\drinksvodkaIII\}}$
only $E$ is ${\cal P}$-preferred$^{\ms{B}}$ and ${\cal P}$-preferred$^{\ms{BH}}$.
In the Baader and Hollunder definition it is obtained as $E = \bigcup_{i\geq 0}\Cn{E_i}$ where $E_0 = \{ \priest \}, E_1 = \{ \priest, \male, \neg\drinksvodkaIII \}$ and $E_i = E_1$ for all $i\geq 2$.
In this extension, the conflict between the first two defaults is resolved
in favor of the first one.
\end{example}

The definitions are not equivalent, as demonstrated by the following example
given by Baader and Hollunder \citeyear{BH95:jar}.
Baader and Hollunder also show that some extensions are
preferred$^{\ms{BH}}$ but not preferred$^B$.

\begin{example}
Let $D = \{ \pfdefr{a}, \pfdefr{b}, \ndefr{b}{c}, \ndefr{a}{\neg c} \}$
and ${\cal P} = \{ \langle \ndefr{b}{c}, \ndefr{a}{\neg c} \rangle \}$.
The extension $E = \Cn{\{a,b,\neg c\}}$ is ${\cal P}$-preferred$^B$ but not
${\cal P}$-preferred$^{\ms{BH}}$.
The extension $E$ cannot be obtained with the Baader and Hollunder definition.
For $E' = \Cn{\{a,b,c\}}$
the Baader and Hollunder definition produces the sets $E'_0 = \emptyset$,
$E'_1 = \{ a, b\}$, $E'_2 = \{ a,b,c\}$ and $E'_i = E'_2$ for all $i\geq 3$,
and the unique ${\cal P}$-preferred$^{\ms{BH}}$ extension is $E' = \bigcup_{i\geq 0}E'_i$.
In Brewka's definition we can bypass the higher priority default
$\ndefr{b}{c}$ by using a total ordering where $\pfdefr{b}$ follows
$\pfdefr{a}$ and $\ndefr{a}{\neg c}$.
This way we obtain the sets
$E_0 = \emptyset$, $E_1 = \{ a\}$, $E_2 = \{ a,\neg c\}$, $E_3 = \{a,\neg c,b\}$ and $E_i = E_3$ for all $i\geq 4$.
\end{example}

Consequence relations that correspond to cautious
reasoning in Reiter's default logic are defined as follows.

\begin{definition}
The consequence relations
$\models^B$ and
$\models^{\ms{BH}}$
are defined by
$\Delta\models^B_{\cal P}\phi$ if and only if the formula $\phi$ is
in all ${\cal P}$-preferred$^B$ extensions of $\Delta$, and
$\Delta\models^{\ms{BH}}_{\cal P}\phi$ if and only if the formula $\phi$ is
in all ${\cal P}$-preferred$^{\ms{BH}}$ extensions of $\Delta$.
\end{definition}

\begin{lemma}\label{le:BBHnormalcoincide}
Let $\langle D,W\rangle$ be a normal default theory and ${\cal T}$
a strict total order on $D$.
Then for all $E\subseteq\langcl$, $E$ is 
a ${\cal T}$-preferred$^{\ms{B}}$ extension of $\langle D,W\rangle$
if and only if $E$ is a ${\cal T}$-preferred$^{\ms{BH}}$ extension of
$\langle D,W\rangle$.
\end{lemma}

\begin{proof}
If $W$ is inconsistent, then the inconsistent extension $\langcl$
is the unique ${\cal T}$-preferred$^B$ and ${\cal T}$-preferred$^{\ms{BH}}$
extension of $\Delta$.
So assume $W$ is consistent.
$(\Rightarrow)$
Assume that $E$ is a ${\cal T}$-preferred$^B$ extension of $\langle D,W\rangle$.
By definition $E = \bigcup_{i\geq 0}\Cn{E_i}$, where $E_i$ are as
in Definition \ref{de:b94}.
Let $E'_i, i\geq 0$ be the sets $E_i$ in Definition \ref{de:bh93}.
We show that $E_i = E'_i$ for all $i\geq 0$, and
hence $E = \bigcup_{i\geq 0}\Cn{E'_i}$ is a ${\cal T}$-preferred$^{\ms{BH}}$
extension of $\Delta$.
\IH $E_i = E'_i$.
\BC{$i=0$} Immediate.
\IC{$i\geq 1$}
Assume that for $\ndefr{\alpha}{\beta}\in D$, $E_{i-1}\models\alpha$,
$E_{i-1}\not\models\neg\beta$ and no $\delta{\cal T}\ndefr{\alpha}{\beta}$
is active in $E_{i-1}$.
Hence $\beta\in E_i$.
By the induction hypothesis $E'_{i-1}\models\alpha$
and no $\delta{\cal T}\ndefr{\alpha}{\beta}$ is active in $E'_{i-1}$.
To show $\beta\in E'_i$ it remains to show that $E\not\models\neg\beta$.
Because $E$ is consistent and $E_i\subseteq E$ and $\beta\in E_i$,
$E\not\models\neg\beta$.
Hence $\beta\in E'_i$ and $E_i\subseteq E'_i$.
Proof of $E'_i\subseteq E_i$ is similar. It suffices to point out that
$E\not\models\neg\beta$ implies $E_{i-1}\not\models\neg\beta$ simply
because $E_{i-1}\subseteq E$.

$(\Leftarrow)$
Let $E$ be a ${\cal T}$-preferred$^{\ms{BH}}$ extension of $\langle D,W\rangle$.
Hence $E = \bigcup_{i\geq 0}\Cn{E'_i}$, where $E'_i, i\geq 0$ are
the sets in Definition \ref{de:bh93}.
Let $E_i, i\geq 0$ be the sets in Definition \ref{de:b94}.
We show by induction that $E = \bigcup_{i\geq 0}E_i$.
\IH $E_i = E'_i$.
\BC{$i=0$} Immediate.
\IC{$i\geq 1$}
Assume that for $\ndefr{\alpha}{\beta}\in D$, $E'_{i-1}\models\alpha$,
$E\not\models\neg\beta$ and no $\delta{\cal T}\ndefr{\alpha}{\beta}$
is active in $E'_{i-1}$.
Hence $\beta\in E'_i$.
By the induction hypothesis $E_{i-1}\models\alpha$
and no $\delta{\cal T}\ndefr{\alpha}{\beta}$
is active in $E_{i-1}$.
To show $\beta\in E_i$ it remains to show that $E_{i-1}\not\models\neg\beta$.
Because $E'_{i-1}\subseteq E$ and $E\not\models\neg\beta$,
$E'_{i-1}\not\models\neg\beta$.
By the induction hypothesis $E_{i-1} = E'_{i-1}$.
Hence $E_{i-1}\not\models\neg\beta$. Therefore $E'_i\subseteq E_i$.
Proof of $E_i\subseteq E'_i$ proceeds similarly.
Assume that for $\ndefr{\alpha}{\beta}\in D$, $E_{i-1}\models\alpha$,
$E_{i-1}\not\models\neg\beta$ and no $\delta\mathcal{T}\ndefr{\alpha}{\beta}$
is active in $E_{i-1}$.
By the induction hypothesis
$E'_{i-1}\models\alpha$ and no $\delta\mathcal{T}\ndefr{\alpha}{\beta}$
is active in $E'_{i-1}$.
It remains to show that $E\not\models\neg\beta$.
So assume $E\models\neg\beta$.
Because $\ndefr{\alpha}{\beta}$ is the $\mathcal{T}$-least active default
and $E\models\neg\beta$, $E'_i = E'_{i-1}$, and further $E'_j = E'_{i-1}$
for all $j\geq i$.
Therefore $E = \Cn{E'_{i-1}}$.
This leads to a contradiction with the assumption $E\models\neg\beta$
and the fact $E'_{i-1}\not\not\models\neg\beta$ obtained with
the induction hypothesis.
Therefore the assumption is false, and $E\not\models\neg\beta$.
Therefore $\beta\in E'_i$ and $E_i\subseteq E'_i$.
\end{proof}

\subsection{Complexity in the General Case}

With no restrictions on the form of defaults, both the Brewka and
the Baader and Hollunder prioritized default logics are
complete for the second level of the polynomial hierarchy.
This means that there are polynomial time translations between
cautious reasoning in Reiter's default logic and the prioritized versions
of cautious reasoning in both of these logics.

\begin{theorem}
Testing $\Delta\models^{B}_{\cal P}\phi$ for normal default theories $\Delta$,
strict partial orders ${\cal P}$ and formulae $\phi$
is $\Pi^p_2$-complete.
\end{theorem}

\begin{proof}
The $\Pi^p_2$-hardness is because with an empty priority relation
Brewka's logic coincides with Reiter's default logic
(Proposition 6 in \cite{Brewka94:jelia}),
which is $\Pi^p_2$-hard even with the restriction to normal defaults
\cite{Gottlob92}.
We show that the complement of the problem is in $\Sigma^p_2$, which
directly implies that the problem is in $\Pi^p_2$.
The complementary problem is the existence of a $\mathcal{P}$-preferred$^B$
extension $E$ such that $\phi\not\in E$.
The guessing of a strict total order ${\cal T}$ that generates
an extension $E$ such that $\phi\not\in E$
can be done by a nondeterministic Turing machine in a polynomial number
of steps: guess ${\cal T}$, and guess the conclusions of generating defaults
of $E$.
The verification that $E$ fulfills Brewka's definition takes a polynomial
number of steps with an NP oracle for propositional satisfiability.
\end{proof}

\begin{theorem}
Testing $\Delta\models^{\ms{BH}}_{\cal P}\phi$ for default theories $\Delta$,
strict partial orders ${\cal P}$ and formulae $\phi$
is $\Pi^p_2$-complete.
\end{theorem}

\begin{proof}
Like the proof of the previous theorem except that no strict total orders
need to be guessed.
\end{proof}

\subsection{Complexity in Syntactically Restricted Cases}\label{se:semirestricted}

In this section we investigate the complexity of the prioritized default logics
in syntactically restricted cases.
This subject is related to the research on the boundary between tractability
and intractability of default logic without priorities by Kautz and Selman
\citeyear{Kautz91} and Stillman \citeyear{Stillman90}.
First we analyze the case in which the priorities
are strict total orders.
Then we complete the complexity analysis by extending the results to
arbitrary strict partial orders.

Kautz and Selman analyze the complexity of determining
the existence of extensions, cautious reasoning, and brave reasoning
for default theories with defaults of the form listed in
Table \ref{ta:formofdefaults} (excluding the prerequisite-free classes) and
with objective parts that are sets of literals.
\begin{table}
\begin{tabular}{rl|l}
& class of default theories & form of defaults \\
\hline
1 &
disjunction-free &
$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$
\\

2 &
unary &
$\odefr{p}{q}{q}$
$\odefr{p}{q \conj\neg r}{q}$
$\odefr{p}{\neg q}{\neg q}$
\\

3 &
disjunction-free ordered &
$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ 
\\

4 &
ordered unary &
$\odefr{p}{q}{q}$
$\odefr{p}{q\conj\neg r}{q}$
$\odefr{p}{\neg q}{\neg q}$
\\

5 &
disjunction-free normal &
$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$
\\

6 &
Horn &
$\odefr{p_1\conj\cdots\conj p_n}{q}{q}$
$\odefr{p_1\conj\cdots\conj p_n}{\neg q}{\neg q}$
\\

7 &
normal unary &
$\odefr{p}{q}{q}$
$\odefr{p}{\neg q}{\neg q}$
\\

8 &
prerequisite-free &
$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$
\\

9 &
prerequisite-free ordered &
$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$
\\

10 &
prerequisite-free unary &
$\odefr{}{q}{q}$
$\odefr{}{q\conj\neg r}{q}$
$\odefr{}{\neg q}{\neg q}$
\\

11 &
prerequisite-free ordered unary &
$\odefr{}{q}{q}$
$\odefr{}{q\conj\neg r}{q}$
$\odefr{}{\neg q}{\neg q}$
\\

12 &
prerequisite-free normal &
$\odefr{}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$
\\

13 &
prerequisite-free normal unary &
$\odefr{}{q}{q}$
$\odefr{}{\neg q}{\neg q}$
\\

14 &
prerequisite-free positive normal unary &
$\odefr{}{q}{q}$
\\
\end{tabular}
\caption{Form of defaults in a number of classes of default theories}\label{ta:formofdefaults}
\end{table}
In Table \ref{ta:formofdefaults}, the letters $a,b,c$ -- possibly subscripted -- denote literals,
and the letters $p,q,r$ denote propositional variables.
Stillman considers only the problem of brave reasoning, but considers
a wider range of classes. He analyzes default theories the objective
parts of which are sets of Horn clauses or sets of 2-literal
clauses, and also the case where defaults are
prerequisite-free.\footnote{Stillman's
definition of prerequisite-free unary and
prerequisite-free ordered unary classes includes only default rules
of the forms $\pfdefr{\neg q}$ and $\defr{}{p\conj\neg q}{p}$.
We, however, consider also default rules of the form $\pfdefr{p}$
in order to have a closer correspondence with
the Kautz and Selman definition of unary classes.
This change does not sacrifice generality, as the default
$\pfdefr{p}$ works like $\defr{}{p\conj\neg q}{p}$
whenever $q$ does not occur elsewhere in the default theory.}
The most general tractable classes in default logic without priorities
are the following.
\begin{itemize}
\item If the objective part $W$ may contain Horn clauses, none of the
restrictions on the form of default rules is sufficient for achieving
tractability in brave reasoning \cite{Stillman90}.
Cautious reasoning has not been investigated.
\item If $W$ consists of 2-literal clauses, brave reasoning for
the prerequisite-free normal class is tractable \cite{Stillman90}.
Cautious reasoning has not been investigated.
\item
If $W$ consists of literals, brave reasoning for the prerequisite-free
normal class and the Horn class are tractable \cite{Kautz91,Stillman90}.
Cautious reasoning is tractable for the normal unary class \cite{Kautz91}.
Cautious reasoning for the prerequisite-free classes has not been
investigated.
\end{itemize}

We present a similar analysis for the same classes of prioritized default
logics starting with the case where priorities totally order the defaults.
We present for each class either a polynomial time decision procedure,
or an NP-hardness or a co-NP-hardness result.

\subsubsection{Summary}

Because of the constructive nature of the definitions of
preferred extensions in the prioritized default logics by Brewka and by Baader
and Hollunder,
constructing the unique preferred extensions
of default theories with total priorities is tractable whenever
the logical consequence tests in propositional logic are tractable
(Theorem \ref{th:spdlttractable}.)
This is because there is always a unique default that is applied next, and
this default cannot be defeated by any default applied later.
So with total priorities, these prioritized default logics
are computationally much easier than Reiter's default logic.

For unrestricted priorities,
Table \ref{ta:BBBHsummary} summarizes the complexity of
$\models^B$ and $\models^{\ms{BH}}$ with various syntactic restrictions.
As Brewka does not consider non-normal default theories, complexity results
on seminormal classes concern the consequence relation $\models^{\ms{BH}}$ only.
In cases where Reiter's default logic is tractable and a prioritized
default logic is not, or vice versa, the complexity characterization
is set in boldface.

Table \ref{ta:BBBHsummaryrefs} gives references to the theorems and
corollaries where the results are stated.
We use the notation $n\subseteq$ to indicate that the intractability
of the class
is directly implied by the intractability of the subclass $n$ in the same
column, and
the notation $\subseteq n$ to indicate that the tractability is
implied by the tractability of the superclass $n$ in the same column.
When the complexity is directly implied by the complexity of
an unprioritized class of default theories investigated
by Kautz and Selman \citeyear{Kautz91} we indicate this by \ksDLNPC.

When looking at Table \ref{ta:BBBHsummary}
it is slightly surprising that the favorable computational properties
in the totally ordered case are in no way reflected in the complexity
of reasoning with arbitrary priorities.
With arbitrary priorities, for almost all classes of default theories in
the Kautz-Selman-Stillman hierarchy
the complexity is the same as the complexity of Reiter's default logic and
the lexicographic prioritized default logic that is discussed in 
Section \ref{se:lexcomplexity}.

% SUMMARY FOR ARBITRARY PRIORITIES AND SEMICONSTRUCTIVE PRIORITIES
\begin{table}
\begin{tabular}{rl|lll}
& class of default theories & \multicolumn{3}{l}{complexity when clauses in W are} \\
& & Horn & 2-literal & 1-literal \\ \hline

1 &
disjunction-free &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

2 &
unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{q \conj\neg r}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

3 &
disjunction-free ordered &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

4 &
ordered unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{q\conj\neg r}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

5 &
disjunction-free normal &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

6 &
Horn &
%$\odefr{p_1\conj\cdots\conj p_n}{q}{q}$
%$\odefr{p_1\conj\cdots\conj p_n}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

7 &
normal unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \dlecoNPH \\

8 &
prerequisite-free &
%$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

9 &
prerequisite-free ordered &
%$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

10 &
prerequisite-free unary &
%$\odefr{}{q}{q}$
%$\odefr{}{q\conj\neg r}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

11 &
prerequisite-free ordered unary &
%$\odefr{}{q}{q}$
%$\odefr{}{q\conj\neg r}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

12 &
prerequisite-free normal &
%$\odefr{}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

13 &
prerequisite-free normal unary &
%$\odefr{}{q}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \PTIME \\

14 &
prerequisite-free positive normal unary &
%$\odefr{}{q}{q}$ &
\coNPH & \coNPH & \PTIME \\
\end{tabular}
\vskip5mm
\caption{Complexity of the consequence relations $\models^B$ and $\models^{\ms{BH}}$}\label{ta:BBBHsummary}
\end{table}

\begin{table}
\begin{tabular}{rl|lll}
& class of default theories & \multicolumn{3}{l}{reference}  \\
& & Horn & 2-literal & 1-literal \\ \hline
1 & disjunction-free & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
2 & unary & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
3 & disjunction-free ordered & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
4 & ordered unary & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
5 & disjunction-free normal & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
6 & Horn & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
7 & normal unary & $14\subseteq$ & $14\subseteq$ & T\ref{th:semnucoNPC} \\
8 & \prerequisitefree & $14\subseteq$ & $14\subseteq$ & $12\subseteq$ \\
9 & \prerequisitefree ordered & $14\subseteq$ & $14\subseteq$ & $12\subseteq$ \\
10 & \prerequisitefree unary & $14\subseteq$ & $14\subseteq$ & $11\subseteq$ \\
11 & \prerequisitefree ordered unary & $14\subseteq$ & $14\subseteq$ & T\ref{th:sn} \\
12 & \prerequisitefree normal & 14 $\subseteq$ & $14\subseteq$ & T\ref{th:pf2t} \\
13 & \prerequisitefree normal unary & 14 $\subseteq$ & $14\subseteq$ & T\ref{th:semicpfnu} \\
14 & \prerequisitefree positive normal unary & T\ref{th:pfpnu2h} & T\ref{th:pfpnu2h} & $\subseteq 13$
\end{tabular}
\vskip5mm
\caption{References to theorems on the complexity of $\models^B$ and $\models^{\ms{BH}}$}\label{ta:BBBHsummaryrefs}
\end{table}

\subsubsection{Tractable Classes}

The following theorem shows that 
with the restriction to priorities that totally order the defaults,
both the Baader and Hollunder and the Brewka definition of preferred
extensions yield an efficient decision procedure for the respective
prioritized default logic.

\begin{theorem}\label{th:spdlttractable}
Let $\langle D,W\rangle$ be a finite default theory and ${\cal T}$
a strict total order on $D$.
The unique ${\cal T}$-preferred$^{\ms{BH}}$ extension
(if preferred$^{\ms{BH}}$ extensions exist)
of $\langle D,W\rangle$ can be computed in polynomial time if all
the membership tests in $\Cn{E_i}$ in the definition of $E$ are
for a polynomial time subset of the propositional logic.
\end{theorem}

\begin{proof}
Unlike the definition of preferred$^B$ extensions,
the definition of preferred$^{\ms{BH}}$ extensions does not directly
yield a polynomial time decision procedure for total priorities
and tractable classical reasoning. This is because the test that
the justifications of defaults to be applied do not belong to the extension
being constructed cannot be performed before the extension
is fully known. However, if a simple test for justifications of defaults
is added, the algorithm that works with preferred$^B$ extensions
works also with preferred$^{\ms{BH}}$ extensions.
Compute sets $E'_i$ as follows.
\begin{eqnarray*}
E'_0 & = & W \\
E'_{i+1} & = & E'_i\cup\left\{ \gamma \left| \defr{\alpha}{\beta}{\gamma}\in D, E'_i\models\alpha, E'_i\not\models\neg\beta, \mbox{ no } \delta{\cal T}\defr{\alpha}{\beta}{\gamma} \mbox{ is active in } E'_i \right.\right\}
\end{eqnarray*}
If $E'_i\models\neg\beta$ for some $\defr{\alpha}{\beta}{\gamma}\in D$
such that for some $j < i$, $E'_j\models\alpha, E'_j\not\models\neg\beta$ and
no $\delta{\cal T}\defr{\alpha}{\beta}{\gamma}$ is active in $E'_j$,
then the algorithm returns {\em false}.
If $E'_i = E'_{i+1}$ for some $i\geq 0$, then return $\Cn{E'_i} = \bigcup_{j\in\{0,\ldots,i\}}\Cn{E'_j}$ and define $E'_j = E'_i$ for all $j > i$.

Let $E$ be a ${\cal T}$-preferred$^{\ms{BH}}$ extension of
$\langle D,W\rangle$.
Hence $E = \bigcup_{i\geq 0}\Cn{E_i}$, where $E_i, i\geq 0$ are
the sets in Definition \ref{de:bh93}.
We show by induction that $E = \bigcup_{i\geq 0}E'_i$ and that
the value {\em false} is not returned.
\IH $E'_i = E_i$.
\BC{$i=0$} Immediate.
\IC{$i\geq 1$}
We first show that $E_i\subseteq E'_i$.
Assume that for $\defr{\alpha}{\beta}{\gamma}\in D$, $E_{i-1}\models\alpha$,
$E\not\models\neg\beta$ and no $\delta{\cal T}\defr{\alpha}{\beta}{\gamma}$
is active in $E_{i-1}$.
Hence $\gamma\in E_i$.
By the induction hypothesis $E'_{i-1}\models\alpha$
and no $\delta{\cal T}\defr{\alpha}{\beta}{\gamma}$
is active in $E'_{i-1}$.
To show $\gamma\in E'_i$ it remains to show that $E'_{i-1}\not\models\neg\beta$.
Because $E_{i-1}\subseteq E$ and $E\not\models\neg\beta$,
$E_{i-1}\not\models\neg\beta$.
By the induction hypothesis $E'_{i-1} = E_{i-1}$.
Hence $E'_{i-1}\not\models\neg\beta$.
Therefore $\gamma\in E'_i$ and $E_i\subseteq E'_i$.
Proof of $E'_i\subseteq E_i$ proceeds similarly.
Assume that for $\defr{\alpha}{\beta}{\gamma}\in D$, $E'_{i-1}\models\alpha$,
$E'_{i-1}\not\models\neg\beta$ and no $\delta\mathcal{T}\defr{\alpha}{\beta}{\gamma}$
is active in $E'_{i-1}$.
By the induction hypothesis
$E_{i-1}\models\alpha$ and no $\delta\mathcal{T}\defr{\alpha}{\beta}{\gamma}$
is active in $E_{i-1}$.
It remains to show that $E\not\models\neg\beta$.
So assume $E\models\neg\beta$.
Because $\defr{\alpha}{\beta}{\gamma}$ is the $\mathcal{T}$-least default
and $E\models\neg\beta$, $E_i = E_{i-1}$, and further $E_j = E_{i-1}$
for all $j\geq i$.
Therefore $E = \Cn{E_{i-1}}$.
This leads to a contradiction with the assumption $E\models\neg\beta$
and the fact $E_{i-1}\not\not\models\neg\beta$ obtained with
the induction hypothesis.
Therefore the assumption is false, and $E\not\models\neg\beta$.
Therefore $\gamma\in E_i$ and $E'_i\subseteq E_i$.
That the algorithm does not return {\em false} goes similarly.
Assume that for some $\defr{\alpha}{\beta}{\gamma}\in D$,
$E'_i\models\neg\beta$ and for some $j < i$,
$E'_j\models\alpha$ and no $\delta{\cal T}\defr{\alpha}{\beta}{\gamma}$ is active in $E'_j$.
We have to show that $E'_j\not\models\neg\beta$.
This is implied by the fact $E\not\models\neg\beta$ shown above because $E'_j\subseteq E$.

Assume that the algorithm yields $E = \bigcup_{i\geq 0}\Cn{E'_i}$.
We claim that $E$ is a ${\cal P}$-preferred$^{\ms{BH}}$ extension
of $\langle D,W\rangle$.
Because the algorithm did not return {\em false} and
$E=\bigcup_{i\geq 0}\Cn{E'_i}$, 
$E\not\models\neg\beta$ for all $\defr{\alpha}{\beta}{\gamma}\in D$
such that for some $j$, $E'_j\models\alpha, E'_j\not\models\neg\beta$ and
no $\delta{\cal T}\defr{\alpha}{\beta}{\gamma}$ is active in $E'_j$.
It is straightforward to show that $E'_i = E_i$ for all $i\geq 0$, where
$E_i$ are the sets in Definition \ref{de:bh93}.
Therefore
$E$ is a ${\cal T}$-preferred$^{\ms{BH}}$ extension of $\langle D,W\rangle$.
\end{proof}

This theorem indicates that with a restriction to total priorities ${\cal T}$,
testing the membership of a literal in all ${\cal T}$-preferred$^{\ms{BH}}$
extensions of default theories in
all the classes of the Kautz and Selman and Stillman hierarchy is in P.

\begin{corollary}
Testing $\langle D,W\rangle\models^{\ms{BH}}_{\cal P}\phi$
for disjunction-free default theories $\langle D,W\rangle$, where $W$ is
a set of Horn clauses or 2-literal clauses, ${\cal P}$ is
a strict total order on $D$, and $\phi$ is a literal,
can be done in polynomial time.
\end{corollary}

\begin{corollary}
Testing $\langle D,W\rangle\models^B_{\cal P}\phi$
for disjunction-free normal default theories $\langle D,W\rangle$,
where $W$ is a set of Horn clauses or 2-literal clauses,
${\cal P}$ is a strict total order on $D$, and $\phi$ is a literal,
can be done in polynomial time.
\end{corollary}

\begin{proof}
Brewka gives a definition of preferred extensions for
normal default theories only.
By Lemma \ref{le:BBHnormalcoincide} the preferred extensions in this case
coincide with the Baader and Hollunder preferred extensions whenever
the priorities are a strict total order.
\end{proof}

For unrestricted priorities
the class of prerequisite-free normal unary default theories is tractable.
The remaining classes in the hierarchy are intractable.

\begin{theorem}\label{th:semicpfnu}
For literals $l$ and
prerequisite-free normal unary theories $\langle D,W\rangle$
where $W$ is a set of literals, testing $\langle D,W\rangle\models^{\ms{BH}}_{\cal P}l$
and  $\langle D,W\rangle\models^B_{\cal P}l$ can be done in polynomial time.
\end{theorem}

\begin{proof}
The algorithm in Figure \ref{fi:pfnualgorithm} tests
$\langle D,W\rangle\models^B_{\cal P}l$
and $\langle D,W\rangle\models^{\ms{BH}}_{\cal P}l$.
\begin{figure}
\zeroc{{\rwprocedure} decide($l,D,W$)}
\twoc{{\rwif} $W\models l$ {\rwthen} {\rwreturn} true;}
\twoc{{\rwif} $\compl{l}\in W$ {\rwthen} {\rwreturn} false;}
\twoc{{\rwif} $\pfdefr{l}\not\in D$ {\rwthen} {\rwreturn} false;}
\twoc{{\rwif} $\pfdefr{\compl{l}}\not\in D$ {\rwthen} {\rwreturn} true;}
\twoc{{\rwif} $\pfdefr{l}{\cal P}\pfdefr{\compl{l}}$ {\rwthen} {\rwreturn} true;}
\twoc{{\rwreturn} false}
\zeroc{\rwend}
\caption{A decision procedure for prioritized prerequisite-free normal unary theories}\label{fi:pfnualgorithm}
\end{figure}
The correctness of the algorithm for $\models^{\ms{BH}}_{\cal P}$
is as follows. For $\models^B_{\cal P}$ the proof is similar.
We analyze the {\em if}-statements in sequence. In each case we may use
the negations of the assumptions of the previous cases.

1. Assume that $W\models l$. Now $l$ is in all ${\cal P}$-preferred$^{\ms{BH}}$
extensions $E$ of $\Delta$ because by definition $W\subseteq E$.
Hence it is correct to return {\em true}.
2. Assume that $\compl{l}\in W$.
Because $W$ is consistent (as $W\not\models l$),
all extensions are consistent, and no extension contains $l$.
Hence it is correct to return {\em false}.
3. Assume that $\pfdefr{l}\not\in D$.
Because $l\not\in W$ and all extensions are consistent, no extension
contains $l$.
Hence it is correct to return {\em false}.
4. Assume that $\pfdefr{\compl{l}}\not\in D$.
Because $\compl{l}\not\in W$, no extension contains $\compl{l}$,
and hence $\pfdefr{l}$ is applied in all extensions, and $l$ is in all
extensions.
Hence it is correct to return {\em true}.
5. Assume that $\pfdefr{l}{\cal P}\pfdefr{\compl{l}}$.
Assume that there is a preferred$^{\ms{BH}}$ extension $E$ such that
$\compl{l}\in E$. Now $\compl{l}\in E_i\setd E_{i-1}$ for some $i$.
Hence $\l\not\in E_{i-1}$ and $\pfdefr{l}$ is not active in $E_{i-1}$.
Hence $\neg l\in E_{i-1}$, which however contradicts
the fact that $\compl{l}\not\in E_{i-1}$.
Hence $\compl{l}$ in no ${\cal P}$-preferred$^{\ms{BH}}$ extension of $\Delta$,
and $\Delta\models^{\ms{BH}}_{\cal P}l$.
Hence it is correct to return {\em true}.
6. In the remaining case not $\pfdefr{l}{\cal P}\pfdefr{\compl{l}}$.
If $\pfdefr{\compl{l}}{\cal P}\pfdefr{l}$, then by an argument similar to
the previous case all ${\cal P}$-preferred$^{\ms{BH}}$ extensions
-- by assumption there is at least one --
contain $\compl{l}$, and hence it is correct to return {\em false}.
If neither $\pfdefr{\compl{l}}{\cal P}\pfdefr{l}$ nor
$\pfdefr{l}{\cal P}\pfdefr{\compl{l}}$, then by symmetry there is an extension
not containing $l$, and hence it is correct to return {\em false}.

Therefore the algorithm returns true if and only if $l$ is in
all ${\cal P}$-preferred$^{\ms{BH}}$ extensions of $\Delta$.
The algorithm obviously runs in polynomial time.
\end{proof}

\subsubsection{Intractable Classes}

Intractability of all remaining classes except the normal unary class
is directly implied by the intractability of the same classes in
Reiter's default logic,
as shown by Kautz and Selman \citeyear{Kautz91} and
Theorems \ref{th:pfpnu2h}, \ref{th:pf2t} and \ref{th:sn}.

Stillman \citeyear{Stillman90} analyzes the complexity of prerequisite-free
default theories, and claims that brave reasoning for the prerequisite-free
normal class with 2-literal clauses is solvable in polynomial time.
However, he does not analyze the complexity of cautious reasoning.
It turns out that even with the restriction to prerequisite-free normal
defaults with propositional variables in justifications and conclusions,
reasoning is intractable.

\begin{theorem}\label{th:pfpnu2h}
Testing $\langle D,W\rangle\models_c l$ for literals $l$
and prerequisite-free positive normal unary default theories
with objective parts that consist of 2-literal Horn clauses, is co-NP-hard.
\end{theorem}

\begin{proof}
We give a many-one reduction from propositional satisfiability to
the complement of the problem.
Let $C$ be a set of clauses and $P$ the set of propositional variables
that occur in $C$.
Let $N$ be an injective function that maps each clause $c\in C$ to
a propositional variable $n = N(c)$ such that $n\not\in P$.
Let
\begin{eqnarray*}
D & = & \left\{\left. \pfdefr{p'} \right| p\in P\right\} \cup \left\{\left. \pfdefr{p''} \right| p\in P \right\} \cup \left\{\left. \pfdefr{n} \right| c\in C, n = N(c) \right\}, \mbox{and} \\
W & = & \{ p'\impl p | p\in P \} \cup \{ p''\impl\neg p | p\in P \} \\
&& \cup \{ p\impl\neg n | p\in c\in C, n = N(c) \} \cup \{ \neg p\impl\neg n | \neg p\in c\in C, n = N(c) \} \\
&& \cup \{ n\impl\ms{false} | c\in C, n = N(c) \}.
\end{eqnarray*}
We claim that $\langle D,W\rangle\not\models_c\ms{false}$ if and only if
$C$ is satisfiable.

Assume that $C$ is satisfiable; that is, there is a model $M$
such that $M\models C$. We show that there is an extension of
$\langle D,W\rangle$ that does not contain $\ms{false}$.
Let $E = \Cn{
\{p'|p\in P, M\models p\}
\cup\{p''|p\in P, M\not\models p\}
%\cup\{p\in P | M\models p\}
%\cup\{\neg p|p\in P, M\not\models p\}
%\cup\{\neg n| c\in C, n = N(c)\}
\cup W}$.
To show that $E$ is an extension of $\langle D,W\rangle$,
it suffices to show that $E$ is consistent and
for all $\pfdefr{\phi}\in D$, $\neg\phi\in E$ if and only if $\phi\not\in E$.
Let $M'$ be a model such that for all $p\in P$, $M'\models p$ iff $M\models p$,
$M'\models p'$ iff $M\models p$, and $M'\models p''$ iff $M\not\models p$,
and $M'\not\models n$ for all $n$ such that $n = N(c)$ for some $c\in C$.
It is straightforward to show that $M'\models E$,
and $E$ is therefore consistent.
Take any $\pfdefr{\phi}\in D$.
Assume that $\neg\phi\in E$. Because $E$ is consistent, $\phi\not\in E$.
Assume that $\phi\not\in E$.
If $\phi = p'$, then by definition $p''\in E$, and as $\{ p''\impl\neg p, p'\impl p\}\subseteq E$, $\neg p'\in E$.
Similarly for $\phi = p''$.
If $\phi = n$ such that $n = N(c)$ for some $c\in C$,
then because $M\models c$, there is disjunct $l\in \{p,\neg p\}$ of $c$
such that $M\models l$, and hence by definition $l\in E$,
and as $l\impl\neg n\in E$, $\neg n\in E$.
Therefore $E$ is an extension of $\langle D,W\rangle$.

Assume that $\langle D,W\rangle\not\models_c\ms{false}$; that is, there is
an extension $E$ of $\langle D,W\rangle$ such that $\ms{false}\not\in E$.
Let $M$ be a model such that for all $p\in P$,
$M\models p$ iff $p\in E$.
We show that $M\models C$, and hence $C$ is satisfiable.
Because $\ms{false}\not\in E$ and $n\impl\ms{false}\in E$ for all
$n$ such that $n = N(c)$ for some $c\in C$, $n\in E$ for no
$n$ such that $n = N(c)$ for some $c\in C$.
Because $\pfdefr{n}\in D$ for all such $n$,
$\neg n\in E$ for all such $n$,
which means that for every clause in $C$, one of its disjuncts is in $E$.
By definition this disjunct is true in $M$.
Hence every clause in $C$ is true in $M$.
\end{proof}

An alternative way of obtaining the intractability of cautious reasoning
for all classes with a Horn objective part is
to apply Theorem 8.2 in \cite{Kautz91} -- that reduces brave reasoning
to cautious reasoning by adding a default $\pfdefr{l}$ --
and the intractability result for brave reasoning in Horn classes \cite{Stillman90}.
This is not applicable to the 2-literal case because in it brave reasoning
is tractable.

\begin{theorem}\label{th:pf2t}
Testing $\langle D,\emptyset\rangle\models_cl$ for literals $l$ and sets $D$
of prerequisite-free normal defaults with
conclusions that are conjunctions of literals,
is co-NP-hard.
\end{theorem}

\begin{proof}
Let $C$ be a set of clauses.
We show that there is a default theory $\langle D,\emptyset\rangle$
such that $\langle D,\emptyset\rangle\not\models_c\ms{false}$ if and only
if $C$ is satisfiable.
Let $P$ be the set of propositional variables that occur in $C$.
Let $N$ be an injective function that maps each clause $c\in C$ to
a propositional variable $n = N(c)$ such that $n\not\in P$.
Define the set of defaults $D$ as follows.
\begin{eqnarray*}
D & = & \left\{\left. \pfdefr{l\conj n} \right| c\in C, l\in c, n=N(c)\right\}\cup\left\{\left. \pfdefr{\neg n\conj\ms{false}} \right| c\in C, n=N(c)\right\}
\end{eqnarray*}

Assume that $C$ is satisfiable.
Let $M$ be a model such that $M\models C$.
Let
\begin{eqnarray*}
E' & = & \Cn{\{l\conj n | c\in C, l\in c, n=N(c), M\models l\}}.
\end{eqnarray*}
Obviously $E'$ is consistent and it does not contain \emph{false}.\footnote{$E'$ is not necessarily an extension of $\langle D,\emptyset\rangle$.
Consider the satisfiable formula $a\disj b$ the clausal form of which is
$C = \{ \{a, b\} \}$,
and the model $M$ that assigns {\em true} to $a$ and {\em false} to $b$.
Now $E' = \Cn{\{ a\conj n\}}$. However, there is the set $E = \Cn{\{a\conj n,b\conj n\}}$
that extends $E'$ and is an extension of $\langle D,\emptyset\rangle$.}
Clearly $E'$ is an extension of $\langle\{\pfdefr{l\conj n}\in D | c\in C, l\in c, n=N(c), l\conj n\in E'\},\emptyset\rangle$.
By Theorem 3.2 in \cite{Reiter80} there is an extension $E$ of $\langle D,\emptyset\rangle$
such that $E'\subseteq E$.
Because $n\in E'\subseteq E$ for all $n = N(c)$ with $c\in C$,
$\ms{false}\not\in E$.

Assume that there is an extension $E$ of $\langle D,\emptyset\rangle$ such
that $\ms{false}\not\in E$.
Let $M$ be a model such that for all propositional variables $p$,
$M\models p$ if and only if $p\in E$.
Because $\ms{false}\not\in E$,
$\pfdefr{\neg n\conj\ms{false}}\in\GD{E}{\langle D,\emptyset\rangle}$ for no $n=N(c), c\in C$.
Take any $c\in C$.
Now $n=N(c)\in E$ and hence $\pfdefr{l\conj n}\in\GD{E}{\langle D,\emptyset\rangle}$ for some $l\in c$.
Hence $l\conj n\in E$ and $M\models c$.
Because this holds for all $c\in C$, finally $M\models C$.
\end{proof}

\begin{theorem}\label{th:sn}
Testing $\langle D,\emptyset\rangle\models_cl$ for literals $l$ and
sets $D$ of prerequisite-free ordered unary defaults is co-NP-hard.
\end{theorem}

\begin{proof}
Proof is by many-one reduction from propositional satisfiability
to testing $\langle D,\emptyset\rangle\not\models_cl$.
Let $C$ be any set of clauses, and let $P$ be the set of propositional
variables occurring in $C$.
Let $N$ be an injective function that maps each clause $c\in C$ to
a propositional variable $n = N(c)$ such that $n\not\in P$.
Let
\begin{eqnarray*}
D & = & \left\{\left. \pfdefr{p} \right| p\in P \right\} 
\cup\left\{\left. \pfdefr{\neg p} \right| p\in P \right\} 
\cup\left\{\left. \defr{}{p'\conj\neg p}{p'} \right| p\in P \right\} \\
&& \cup\left\{\left. \defr{}{n\conj\neg p}{n} \right| c\in C, n = N(c), \neg p\in c \right\} \\
&& \cup\left\{\left. \defr{}{n\conj\neg p'}{n} \right| c\in C, n = N(c), p\in c \right\} 
\cup\left\{\left. \defr{}{\ms{false}\conj\neg n}{\ms{false}} \right| c\in C, n = N(c) \right\}.
\end{eqnarray*}
The orderedness condition is fulfilled because the relation
$\ll\subseteq(P\times\{N(c)|c\in C\})\cup(\{p'|p\in P\}\times\{N(c)|c\in C\})\cup(\{N(c)|c\in C\}\times\{\ms{false}\})\cup (P\times \{p'|p\in P\})$ is irreflexive.

We claim that $C$ is satisfiable if and only if $\langle D,\emptyset\rangle\not\models_c\ms{false}$.
Assume that $C$ is satisfiable; that is, there is a model $M$ such that
$M\models C$.
We construct an extension $E$ of $\langle D,\emptyset\rangle$ such that
$\ms{false}\not\in E$.
Let 
\begin{eqnarray*}
A & = & \left\{\left. \pfdefr{p} \right| p\in P, M\models p\right\}
\cup \left\{\left. \pfdefr{\neg p} \right| p\in P, M\not\models p\right\} \\
&& \cup \left\{\left. \defr{}{p'\conj\neg p}{p'} \right| p\in P, M\not\models p\right\} \\
&& \cup \left\{\left. \defr{}{n\conj\neg p}{n} \right| c\in C, n = N(c), \neg p\in c, M\not\models p\right\} \\
&& \cup \left\{\left. \defr{}{n\conj\neg p'}{n} \right| c\in C, n = N(c), p\in c, M\models p\right\}.
\end{eqnarray*}
Define $E = \Cn{\{\phi|\defr{}{\psi}{\phi}\in A\}}$.
To verify that $E$ is an extension of $\langle D,\emptyset\rangle$ it suffices
to check that for every $\defr{}{\phi}{\psi}\in A$, $\neg\phi\not\in E$,
and for every $\defr{}{\phi}{\psi}\in D\setd A$, $\neg\phi\in E$,
and this is straightforward.
Hence $\langle D,\emptyset\rangle\not\models_c\ms{false}$.

Assume that $\langle D,\emptyset\rangle\not\models_c\ms{false}$; that is,
there is an extension $E$ of $\langle D,\emptyset\rangle$ such that
$\ms{false}\not\in E$.
Let $M$ be a model such that for all propositional variables $p$,
$M\models p$ if and only if $p\in E$.
We show that $M\models C$.
Because $\ms{false}\not\in E$, $\defr{}{\ms{false}\conj\neg n}{\ms{false}}\not\in\GD{E}{\Delta}$ for all $n$ such that $n = N(c)$ for some $c\in C$.
Hence $n\in E$ for all such $n$.
Hence for every $n$, there is $\defr{}{n\conj\neg p}{n}\in\GD{E}{\Delta}$
or $\defr{}{n\conj\neg p'}{n}\in\GD{E}{\Delta}$.
Hence for every clause $l_1\disj\cdots\disj l_n\in C$,
$p\not\in E$ for some $\neg p\in\{l_1,\ldots,l_n\}$, or
$p'\not\in E$ for some $p\in\{l_1,\ldots,l_n\}$.
In the first case by definition $M\models\neg p$.
In the second case $p\in E$ and hence by definition $M\models p$.
Hence every clause in $C$ is true in $M$,
and $C$ is satisfiable.
\end{proof}

Ben-Eliyahu and Dechter \citeyear{B-ED96} show that testing $\models_c$
for a class of default theories that subsumes all classes in the Kautz and
Selman and Stillman hierarchy that have a 2-literal objective part
is co-NP-complete.
Hence the problems in Theorems \ref{th:pfpnu2h}, \ref{th:pf2t} and \ref{th:sn}
are in co-NP, and consequently co-NP-complete.
The Ben-Eliyahu and Dechter result, however, has no direct implications on
the complexity of the prioritized versions of these problems.

\begin{theorem}\label{th:semnucoNPC}
Both testing $\Delta\models^{B}_{\cal P}l$
and $\Delta\models^{\ms{BH}}_{\cal P}l$ for
normal unary default theories $\Delta$,
strict partial orders ${\cal P}$
and literals $l$, is co-NP-hard.
\end{theorem}

\begin{proof}
We give the proof for preferred$^{\ms{B}}$ extensions only.
The proof for preferred$^{\ms{BH}}$ extensions is similar.
The proof is by reduction from propositional satisfiability
to the complement of the problem.
Let $C = \{ c_1,\ldots,c_m\}$ be a set of propositional clauses and $P$
the set of propositional variables occurring in $C$.
Let $N$ be an injective function that maps each clause $c\in C$ to
a propositional variable $n = N(c)$ such that $n\not\in P$.
Define the default theory $\Delta = \langle D,\emptyset\rangle$ and
priorities ${\cal P}$ on $D$ as follows.
\begin{eqnarray*}
D_1 & = & \left\{\left.\pfdefr{p}\right| p\in P \right\}\cup\left\{\left.\pfdefr{\neg p}\right| p\in P \right\} \\
D_2 & = & \left\{\left.\pfdefr{p'}\right| p\in P \right\}\cup\left\{\left.\ndefr{p}{\neg p'}\right| p\in P \right\} \\
D_3 & = & \left\{\left. \ndefr{p}{n} \right| p\in c\in C, n = N(c)\right\} \cup \left\{\left. \ndefr{p'}{n} \right| \neg p\in c\in C, n = N(c)\right\} \\
&& \cup\left\{\left.\pfdefr{n'}\right| c\in C, n = N(c) \right\}\cup\left\{\left.\ndefr{n}{\neg n'}\right| c\in C, n = N(c) \right\} \\
&& \cup\left\{\left.\ndefr{n'}{\ms{false}}\right| c\in C, n = N(c) \right\} \\
D & = & D_1\cup D_2\cup D_3 \\
{\cal P} & = &
\left\{\left.\left\langle \ndefr{p}{\neg p'},\pfdefr{p'}\right\rangle\right| p\in P\right\} \cup (D_1\times(D_2\cup D_3))
\end{eqnarray*}
Priorities are needed to guarantee that $p\in E$ if and only if $p'\not\in E$, and total priorities cannot be used because we cannot restrict to those
models that correspond to preferred extensions
(with respect to some ordering on the variables),
as they are not necessarily models of $C$ even if $C$ is satisfiable.
\begin{figure}
\centerline{\epsfig{figure=translation.eps}}
\caption{A translation from satisfiability to prioritized default logic}\label{fi:SATtoNUDL}
\end{figure}
The default theory is depicted in Figure \ref{fi:SATtoNUDL}.
Defaults $\ndefr{p}{q}$ are shown as arrows $p\rightarrow q$, and
defaults $\ndefr{p}{\neg q}$ as broken arrows $p\not\rightarrow q$.
Only some of defaults $\ndefr{p}{n}$ and $\ndefr{p'}{n}$
for propositions $p\in P$ and $n, n=N(c)$ for $c\in C$, are in $D$,
and therefore they are shown as dashed arrows.
We claim that $C$ is satisfiable if and only if
there is a ${\cal P}$-preferred$^{\ms{B}}$ extension of $\Delta$
that does not contain {\em false}.

Assume that $C$ is satisfiable; that is, there is a model $M$
such that $M\models C$.
We show that there is a ${\cal P}$-preferred$^{B}$ extension $E$ of 
$\Delta$ such that $\ms{false}\not\in E$.
Let $E = \Cn{\{ p\in P | M\models p \}\cup\{p'|p\in P, M\not\models p\}
\cup \{ \neg p | p\in P, M\not\models p \}\cup\{\neg p'|p\in P, M\models p\}
\cup \{ n | c\in C, n = N(c)\}
\cup\{\neg n'|c\in C, n = N(c)\}}$.
Let ${\cal T}$ be a strict total order on $D$ such that
${\cal P}\subseteq{\cal T}$
and for all $p\in P$, $\pfdefr{p}{\cal T}\pfdefr{\neg p}$ if $M\models p$
and $\pfdefr{\neg p}{\cal T}\pfdefr{p}$ otherwise,
and
$\ndefr{n}{\neg n'}{\cal T}\pfdefr{n}$ for all $c\in C$, $n = N(c)$.
It is straightforward to verify that $E$ is
a ${\cal P}$-preferred$^{B}$ extension of $\Delta$ generated by ${\cal T}$.
Clearly $\ms{false}\not\in E$.

Assume that $E$ is a ${\cal P}$-preferred$^{B}$ extension such that
$\ms{false}\not\in E$.
Let $M$ be a model such that for all $p\in P$,
$M\models p$ if and only if $p\in E$.
Because $\ms{false}\not\in E$, no default $\ndefr{n'}{\ms{false}}$
is applied in $E$, where $n = N(c)$ for some $c\in C$.
Therefore $n'\not\in E$ for all $n = N(c)$ such that $c\in C$.
Therefore $\neg n'\in E$ and $n\in E$ for all such $n$.
Hence a disjunct $p$ is in $E$ or $p'$ is in $E$ for a disjunct $\neg p$
for every $c\in C$.
In the first case by definition of $M$, $M\models c$.
In the second case $p\not\in E$, because otherwise $\neg p'$ would be in
$E$ as $\ndefr{p}{\neg p'}{\cal P}\pfdefr{p'}$.
Hence $M\models\neg p$ and $M\models c$.
Because this holds for all $c\in C$, finally $M\models C$.
\end{proof}

\section{Lexicographic Prioritized Default Logic}\label{se:lexcomplexity}

A definition of prioritized default logic is used by Rintanen
\citeyear{Rintanen97:pdl}. This definition is based on an earlier one
for autoepistemic logic \cite{Rintanen94:jelia}.
The priority mechanism uses lexicographic comparison and
the preferred extensions in this approach do not in general coincide
with the preferred extensions in the prioritized default logics discussed
in Section \ref{se:sncomplexity}.
Lexicographic comparison has earlier been used in the context of
nonmonotonic reasoning by several researchers \cite{Lifschitz85,GP92,Ryan92}.
Comparing two extensions is based on whether the defaults are generating
defaults of the extensions, that is, 
whether their prerequisites belong to the extension and
the negations of the justifications do not belong to the extension.
We say that a generating default of an extension is {\em applied} in
the extension.

\begin{definition}[Application]
A default $\defaultr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}$ is
{\em applied in} $E\subseteq\langcl$
if $E\models\alpha$ and $\{\neg\beta_1,\ldots,\neg\beta_n\}\cap\Cn{E} = \emptyset$.
This is denoted by $\applied{\defaultr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}}{E}$.
\end{definition}

We abbreviate $\applied{\delta}{E}$ and not $\applied{\delta}{E'}$
by the notation $\appliet{\delta}{E}{E'}$.

\begin{definition}[Preferredness]\label{de:preferredness}
Let $\Delta = \langle D,W\rangle$ be a default theory and
${\cal P}$ a strict partial order on $D$.
Let $E$ be an extension of $\Delta$.
Then $E$ is a {\em ${\cal P}$-preferred$^L$ extension} of $\Delta$
if there is a strict total order
${\cal T}$ on $D$ such that ${\cal P}\subseteq{\cal T}$ and
for all extensions $E'$ of $\Delta$ and $\delta\in D$,
\[ \appliet{\delta}{E'}{E} \mbox{ implies that for some } \epsilon\in D, \prefer{\epsilon}{\delta}{\cal T} \mbox{ and } \appliet{\epsilon}{E}{E'}.\]
Such a strict total order is a {\em $\Delta,{\cal P}$-ordering} for $E$.
\end{definition}

Our investigation on lexicographic prioritization in default reasoning
was motivated by earlier work on the topic \cite{TT92,BH95:jar}.
These definitions of priorities for default logic are procedural,
as they are given as extensions of (nondeterministic)
decision procedures for default logic.
This procedural nature of prioritization is sensitive to
the lengths of sequences of defaults involved in deriving certain facts:
among two conflicting defaults the one with the lower priority may become
applied solely because the sequence of defaults needed for deriving
its prerequisite is shorter \cite{BE98}.
Approaches to prioritizing defaults that are based on lexicographic comparison
\cite{Lifschitz85,Brewka89,GP92,Ryan92} do not exhibit that kind of behavior.

Lexicographic comparison has properties that are favorable from
the point of view of knowledge representation.
Extensions of a default theory are possible interpretations
of the default theory, representing different ways of
resolving the conflicts between default rules.
Priorities express the plausibility of different ways of resolving
the conflicts, and consequently act as an implicit representation
of preferences between the extensions.
One useful property of lexicographic comparison is that
every finite default theory has at least one preferred extension
whenever it has at least one Reiter extension. It does not seem plausible
that the priorities could contain information that indicates that none of
the extensions is a plausible meaning of the default theory.
Another useful property is that every extension of a default theory is
a ${\cal P}$-preferred$^L$ extension for a suitably chosen ${\cal P}$.
In other words, the way priorities are used in ranking the extensions
should not per se rule out the possibility that a certain extension
is preferred or that it is the unique preferred extension.

A distinguishing difference between the lexicographic prioritized default logic
and other work on priorities in default logic is that
the highest priority default -- if there is one -- is applied in all
preferred$^L$ extensions if there is an extension where it is applied.
Preferred$^B$ and preferred$^{\ms{BH}}$ extensions
do not always apply the applicable highest priority defaults.

\begin{example}[Brewka, 1994]\label{ex:brewkafailure}
Consider the default theory $\Delta = \langle D, W\rangle$ where
$W = \{ a \}$ and $D = \{ \ndefaultr{b}{c}, \ndefaultr{a}{\neg c}, \ndefaultr{a}{b}\}$.
Define the relation
\[ {\cal P} = \left\{ \left\langle\ndefaultr{b}{c},\ndefaultr{a}{\neg c}\right\rangle,\left\langle\ndefaultr{a}{\neg c},\ndefaultr{a}{b}\right\rangle,\left\langle\ndefaultr{b}{c},\ndefaultr{a}{b}\right\rangle \right\}. \]
According to Definitions \ref{de:bh93} and \ref{de:b94}
the sets $E_i$ are as follows,
and the unique
${\cal P}$-preferred$^{\ms{B}}$ and ${\cal P}$-preferred$^{\ms{BH}}$
extension of $\Delta$ is $E = \bigcup_{i\geq 1}\Cn{E_i}$.
\begin{eqnarray*}
E_0 & = & \{ a\} \\
E_1 & = & \{ a, \neg c \} \\
E_2 & = & \{ a, \neg c, b \} \\
E_i & = & E_2 \mbox{ for all } i\geq 3
\end{eqnarray*}
In other words, initially the highest priority default $\ndefaultr{b}{c}$
is not applicable, and hence the second default $\ndefaultr{a}{\neg c}$
is applied, and $\neg c$ is obtained.
The highest priority default is still not applicable, and hence the
third default $\ndefaultr{a}{b}$ is applied, and $b$ is obtained.
Now $\ndefaultr{b}{c}$ were applicable if the contradicting default
$\ndefaultr{a}{\neg c}$ would not have been applied first.
\end{example}

The application of the highest priority default -- whenever possible -- would
seem a useful declarative property for nonmonotonic reasoning with priorities.
The satisfaction of this property leads to lexicographic prioritization.
Also, the behavior of lexicographic prioritized default logic is
more consistent for default theories with normal defaults
$\ndefr{\alpha}{\beta}$ and closely related default theories with
prerequisite-free normal defaults $\pfdefr{\alpha\impl\beta}$.
The latter defaults allow reasoning by contraposition with the implications,
and the former do not, but otherwise they represent related patterns of
reasoning.
The logics by Brewka and by Baader and Hollunder order extensions
lexicographically for the latter kind of default theories,
but not for the former.

\begin{definition}
The consequence relation $\models^L$ is defined by
$\Delta\models^L_{\cal P}\phi$ if and only if the formula $\phi$ is
in all ${\cal P}$-preferred$^L$ extensions of $\Delta$.
\end{definition}

\begin{example}\label{ex:penguintechnical}
Let $\langle D,W\rangle$ be a default theory where
$D = \{ \ndefr{p}{q}, \ndefr{p}{\neg r}, \ndefr{q}{r} \}$
and $W = \{ p\}$.
Let
${\cal P} = \left\{ \left\langle\defaultr{p}{\neg r}{\neg r},\defaultr{q}{r}{r}\right\rangle \right\}$
be a strict partial order on $D$.
The default theory has two extensions,
$E_1 = \Cn{\{p,q,\neg r\}}$ where the defaults
$\ndefr{p}{\neg r}$ and $\ndefr{p}{q}$ are applied, and
$E_2 = \Cn{\{p,q,r\}}$ where $\ndefr{p}{q}$ and $\ndefr{q}{r}$ are applied.
These extensions and all strict total orders ${\cal T}$ on $D$
such that ${\cal P}\subseteq{\cal T}$ are depicted below.
The most significant defaults are the lowest.
The symbol $\bullet$ signifies that the default is applied and $\circ$
that it is not applied.

\medskip
\medskip
\begin{small}
\centerline{
\begin{tabular}{lll}
\begin{diagram}[size=4mm]
&& E_1 & E_2 \\
\ndefr{p}{q} & & \bullet & \bullet \\
&& \uLine & \uLine  \\
\ndefr{q}{r} & & \circ & \bullet \\
&& \uLine & \uLine  \\
\ndefr{p}{\neg r} & & \bullet & \circ \\
\end{diagram}
&
\begin{diagram}[size=4mm]
&& E_1 & E_2 \\
\ndefr{q}{r} & & \circ & \bullet \\
&& \uLine & \uLine  \\
\ndefr{p}{q} & & \bullet & \bullet \\
&& \uLine & \uLine  \\
\ndefr{p}{\neg r} & & \bullet & \circ \\
\end{diagram}
&
\begin{diagram}[size=4mm]
&& E_1 & E_2 \\
\ndefr{q}{r} & & \circ & \bullet \\
&& \uLine & \uLine  \\
\ndefr{p}{\neg r} & & \bullet & \circ \\
&& \uLine & \uLine  \\
\ndefr{p}{q} & & \bullet & \bullet \\
\end{diagram}
\end{tabular}}
\end{small}
\medskip

The extension $E_1$ is a ${\cal P}$-preferred$^L$ extension because
the leftmost strict total order ${\cal T}_1$ is a $\Delta,{\cal P}$-ordering  for $E_1$:
$\ndefr{q}{r}$ is the only default $\delta$ such that $\appliet{\delta}{E_2}{E_1}$, and
$\appliet{\ndefr{p}{\neg r}}{E_1}{E_2}$ and
$\ndefr{p}{\neg r}{\cal T}_1\ndefr{q}{r}$.
The extension $E_2$ is not a ${\cal P}$-preferred$^L$ extension because
none of the three strict total orders ${\cal T}_1,{\cal T}_2,{\cal T}_3$
is a $\Delta,{\cal P}$-ordering for $E_2$:
for all $i\in\{1,2,3\}$,
there is the default $\ndefr{p}{\neg r}$ such that
$\appliet{\ndefr{p}{\neg r}}{E_1}{E_2}$ and
there is no default $\delta$ such that $\delta{\cal T}_i\ndefr{p}{\neg r}$
and $\appliet{\delta}{E_2}{E_1}$.
\end{example}

%\begin{lemma}[Monotonicity]\label{le:monotonicity}
%Let $\Delta = \langle D, W\rangle$ be a default theory.
%Let $E$ be a ${\cal P}$-preferred$^L$ extension of
%$\Delta$ for some strict partial order ${\cal P}$ on $D$.
%Let ${\cal P}'$ be a strict partial order on $D$ such that
%${\cal P}'\subseteq{\cal P}$.
%Then $E$ is a ${\cal P}'$-preferred$^L$
%extension of $\Delta$.
%\end{lemma}
%
%\begin{proof}
%If $E$ is a ${\cal P}$-preferred$^L$ extension of $\Delta$,
%there is a $\Delta,{\cal P}$-ordering ${\cal T}$ for $E$.
%Because ${\cal P'}\subseteq{\cal P}$, ${\cal T}$ is also
%a $\Delta,{\cal P}'$-ordering for $E$, and
%hence $E$ is a ${\cal P}'$-preferred$^L$ extension.
%\end{proof}

\begin{lemma}\label{le:texistence}
Let $\Delta = \langle D, W\rangle$ be a default theory where $D$ is
finite,
and let ${\cal P}$ be a strict total order on $D$.
Let $\Delta$ have at least one extension.
Then there is exactly one ${\cal P}$-preferred$^L$ extension of $\Delta$.
\end{lemma}

\begin{proof}
We show that there is an extension $E$ of $\Delta$ such that ${\cal P}$
is the $\Delta,{\cal P}$-ordering for $E$.
Let $\delta_1,\ldots,\delta_n$ be the ordering ${\cal P}$ of $D$.
Define $D_i = \{\delta_1,\ldots,\delta_i\}$ for all $i\in\{0,\ldots,n\}$.
Define for all $i\in\{1,\ldots,n-1\}$,
\begin{eqnarray*}
X_0 & = & \{ E\subseteq\langcl | E \mbox{ is an extension of } \Delta \}, \mbox{ and} \\
X_{i+1} & = & \left\{
   \begin{array}{ll}
   \{E\in X_i | \applied{\delta_{i+1}}{E} \} & \mbox{ if } \applied{\delta_{i+1}}{E} \mbox{ for some } E\in X_i, \\
   X_i & \mbox{ otherwise.}
   \end{array}
   \right.
\end{eqnarray*}
\IH For $j\in\{0,\ldots,i\}$,
(1) the set $X_j$ is non-empty,
(2) for all $E\in X_j$ and $E'\in X_j$ and $\delta\in D_j$,
$\applied{\delta}{E}$ iff $\applied{\delta}{E'}$, and
(3) for all $E\in X_j$ and $E'\in X_0\setd X_j$ there is
$\delta\in D_j$ such that $\appliet{\delta}{E}{E'}$ and there is no $\delta'\in D$ such that $\delta'{\cal P}\delta$ and $\appliet{\delta'}{E'}{E}$.

The proofs of both the base case and the inductive case are straightforward.

The claim of the lemma is obtained from the facts established in the induction
proof as follows.
By (1) the set $X_n$ is non-empty.
By (2) and Theorems 2.4 and 2.5 in \cite{Reiter80} $|X_n|\leq 1$.
Hence $X_n$ is a singleton $\{E\}$.
Let $E'$ be any extension of $\Delta$.
Assume that there is $\delta'\in D$ such that $\appliet{\delta'}{E'}{E}$.
Hence $E'\neq E$ and $E'\in X_0\setd X_n$.
Now by (3) there is $\delta\in D_n = D$ such that $\appliet{\delta}{E}{E'}$
and there is no $\delta''$ such that $\delta''{\cal P}\delta$ and
$\appliet{\delta''}{E'}{E}$. Therefore not $\delta'{\cal P}\delta$,
and because ${\cal P}$ is a strict total order, it is the case that
$\delta{\cal P}\delta'$. Because this holds for all $\delta'\in D$ and 
all extensions $E'$ of $\Delta$,
${\cal P}$ is a $\Delta,{\cal P}$-ordering for $E$.
Therefore $E$ is a ${\cal P}$-preferred$^L$ extension of $\Delta$.
Let $E'$ be any extension such that $E\neq E'$.
Now $E\in X_n$ and $E'\not\in X_n$, and therefore by (3) there
is $\delta\in D$ such that $\appliet{\delta}{E}{E'}$ and there is
no $\delta'\in D$ such that $\delta'{\cal P}\delta$ and $\appliet{\delta'}{E'}{E}$.
Hence $E$ is the only ${\cal P}$-preferred$^L$ extension of $\Delta$.
\end{proof}

%\begin{theorem}\label{th:extensionexistence}
%Let $\Delta = \langle D, W\rangle$ be a default theory where $D$ is
%finite.
%If $\Delta$ has extensions, it has at least one ${\cal P}$-preferred$^L$
%extension for any strict partial order ${\cal P}$ on $D$.
%\end{theorem}
%
%\begin{proof}
%Let ${\cal P}$ be any strict partial order on $D$.
%Let ${\cal T}$ be a strict total order on $D$ such that
%${\cal P}\subseteq{\cal T}$.
%By Lemma \ref{le:texistence} there is a ${\cal T}$-preferred$^L$ 
%extension $E$ of $\Delta$.
%By Lemma \ref{le:monotonicity} $E$ is also ${\cal P}$-preferred$^L$.
%\end{proof}

\subsection{Complexity in the General Case}\label{se:pdlcomplexity}

The language that corresponds to the consequence relation $\models$ 
of the classical propositional logic is denoted by CN and is defined as
the set of pairs $\langle\Sigma,\phi\rangle\in 2^\langcl\times\langcl$
such that $\Sigma\models\phi$.
Some of the complexity results use the procedure in
Figure \ref{fi:pextension} that is directly based on the semiconstructive
definition of extensions given in Theorem \ref{th:semiconstructive}.
\begin{figure}
\zeroc{{\rwprocedure} extension($D,W,E$);}
\twoc{$E'$ := $W$;}
\twoc{{\rwrepeat}}
\fourc{$E''$ := $E'$;}
\fourc{{\rwforeach} $\defr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}\in D$ {\rwdo}}
\sixc{{\rwif} $\langle E',\alpha\rangle\in$ CN and $\langle E,\neg\beta\rangle\not\in$ CN for all $\beta\in\{\beta_1,\ldots,\beta_n\}$}
\sixc{{\rwthen} $E'$ := $E'\cup\{ \gamma \}$}
\fourc{{\rwend}}
\twoc{{\rwuntil} $E' = E''$;}
\twoc{{\rwif} $\langle E,\phi\rangle\in $ CN for all $\phi\in E'$ and $\langle E', \phi\rangle\in$ CN for all $\phi\in E$}
\twoc{{\rwthen} {\rwreturn} true {\rwelse} {\rwreturn} false}
\zeroc{\rwend}
\caption{A procedure for recognizing extensions}\label{fi:pextension}
\end{figure}
\begin{lemma}\label{le:pextension}
For the procedure in Figure \ref{fi:pextension},
the call extension($D,W,E$) returns
{\em true} if and only if $\Cn{E}$ is an extension of the default
theory $\langle D,W\rangle$.
Excluding the tests of membership in CN the procedure runs in polynomial time
on the size of $\langle D,W\rangle$.
\end{lemma}

Our decision procedure for the lexicographic prioritized default logic
is based on a reduction to the language ENC, which in
turn is reducible to CN in nondeterministic polynomial time.
There are three kinds of questions ENC can answer:
is the logical closure of a set of formulae an extension of a
default theory, is a strict total order a $\Delta,{\cal P}$-ordering for
an extension, and is a formula a logical consequence of a set of formulae.
The language ENC$\subseteq \{0,1,2\}\times 2^\langd\times 2^\langcl\times 2^\langcl\times (2^{\langd\times\langd}\cup\langcl)$
is defined as the set of quintuples
\begin{itemize}
\item $\langle 0,D,W,E,{\cal T} \rangle$ where $D$ is a set of defaults,
$W\subseteq\langcl$ is a set of formulae, and $\Cn{E}$ is an extension of $\langle D,W\rangle$,
\item $\langle 1,D,W,E,{\cal T} \rangle$ where $D$ is a set of defaults,
$W\subseteq\langcl$ is a set of formulae, $E$ is a set of formulae,
${\cal T}$ is a strict total order on $D$,
and ${\cal T}$ is not a $\langle D,W\rangle,{\cal T}$-ordering  for $\Cn{E}$, and
\item $\langle 2,D,W,E,\phi\rangle$ where $\langle E,\phi\rangle\in$ CN.
\end{itemize}

\begin{lemma}\label{le:ENC}
ENC is Turing reducible to CN in nondeterministic polynomial time.
\end{lemma}

\begin{proof}
The language ENC is accepted by a nondeterministic Turing machine given
as the procedure in Figure \ref{fi:ENC}.
The executions of the procedure have a polynomial length.
\begin{figure}
\zeroc{{\rwprocedure} ENC($n,D,W,E,{\cal T}$);}
\twoc{{\rwcase} $n$ {\rwof}}
\twoc{$0$: {\rwif} extension($D,W,E$) {\rwthen} accept {\rwelse} reject}
\twoc{$1$: guess nondeterministically a subset $E'$ of conclusions of $D$;}
\fourc{$E'$ := $E'\cup W$;}
\fourc{{\rwif} not extension($D,W,E'$) or not extension($D,W,E$)}
\sixc{{\rwthen} reject}
\fourc{{\rwelse} {\rwif} compare($E,E',{\cal T}$) = true {\rwthen} reject}
\tenc{{\rwelse} accept}
\twoc{$2$: {\rwif} $\langle E,{\cal T}\rangle\in$ CN {\rwthen} accept {\rwelse} reject}
\twoc{otherwise: reject}
\zeroc{\rwend}
\emptyline
\zeroc{{\rwprocedure} applied($\defr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma},E$);}
\twoc{{\rwif} $\langle E,\alpha\rangle\in$ CN and $\langle E,\neg\beta\rangle\not\in$ CN for all $\beta\in\{\beta_1,\ldots,\beta_n\}$}
\twoc{{\rwthen} {\rwreturn} true {\rwelse} {\rwreturn} false}
\zeroc{{\rwend}}
\emptyline
\zeroc{{\rwprocedure} compare($E,E',{\cal T}$);}
\twoc{let ${\cal T}$ be the ordering $\delta_0{\cal T}\delta_1{\cal T}\cdots{\cal T}\delta_n$;}
\twoc{{\rwfor} i := 0 {\rwto} n {\rwdo}}
\fourc{{\rwif} not applied($\delta_i, E$) and applied($\delta_i, E'$) {\rwthen} {\rwreturn} false;}
\fourc{{\rwif} applied($\delta_i, E$) and not applied($\delta_i, E'$) {\rwthen} {\rwreturn} true}
\twoc{{\rwend}}
\twoc{{\rwreturn} true}
\zeroc{\rwend}
\caption{A decision procedure for ENC}\label{fi:ENC}
\vskip1cm
\end{figure}
\end{proof}

\begin{theorem}\label{th:cautiouspdl}
The complement of the problem of testing whether a formula belongs to all
preferred$^L$ extensions of a default theory is Turing reducible to ENC in
nondeterministic polynomial time.
\end{theorem}

\begin{proof}
The question is answered by a Turing machine described by the procedure
in Figure \ref{fi:cocautiouspdl}.
The Turing machine uses an oracle for the language ENC.
First the machine guesses a candidate extension $\Cn{E\cup W}$
of $\langle D,W\rangle$
and a strict total order ${\cal T}$ on $D$ that extends the relation ${\cal P}$.
Then the machine verifies that $\Cn{E\cup W}$ is in fact an extension
(the first consultation of the oracle for ENC),
that ${\cal T}$ is a $\langle D,W\rangle,{\cal P}$-ordering
for $\Cn{E\cup W}$ (the second consultation),
and that $\phi\not\in\Cn{E\cup W}$ (the third consultation.)
If all these verifications succeed, the Turing machine accepts.
Because the guesses of $E$ and ${\cal T}$ are nondeterministic,
the machine accepts whenever there is an extension that contains $\phi$
and has a $\langle D,W\rangle,{\cal P}$-ordering.

The only parts of the procedure that do not run in constant time
are the nondeterministic guessing of the set $E$,
guessing of a strict total order ${\cal T}$,
and verifying that it extends ${\cal P}$.
Because the sizes of $E$ and ${\cal T}$ are polynomial in $\langle D,W\rangle$,
the number of steps needed to guess them is polynomial in $\langle D,W\rangle$.
Verification of ${\cal P}\subseteq{\cal T}$ takes polynomial time.
\begin{figure}
\zeroc{{\rwprocedure} co-cautious($D,W,{\cal P},\phi$);}
\twoc{guess nondeterministically a subset $E$ of conclusions of $D$;}
\twoc{guess nondeterministically a strict total order ${\cal T}$ on $D$;}
\twoc{{\rwif} ${\cal P}\not\subseteq{\cal T}$ {\rwthen} reject;}
\twoc{{\rwif} $\langle 0,D,W,E\cup W,\emptyset\rangle\in$ ENC}
\fourc{{\rwand} $\langle 1,D,W,E\cup W,{\cal T}\rangle\not\in$ ENC}
\fourc{{\rwand} $\langle 2,\emptyset,\emptyset,E\cup W,\phi\rangle\not\in$ ENC}
\twoc{{\rwthen} accept}
\twoc{{\rwelse} reject}
\zeroc{{\rwend}}
\caption{A decision procedure for prioritized cautious reasoning}\label{fi:cocautiouspdl}
\end{figure}
\end{proof}

We give an upper and a lower bound for the location of the decision problem
in the polynomial hierarchy.
Because ENC is Turing reducible to CN in nondeterministic
polynomial time, the following lemma is immediate.

\begin{lemma}
The language ENC is in $\Sigma^p_2$.
\end{lemma}

By Theorem \ref{th:cautiouspdl} we get an upper bound
for the location of the decision problem in the polynomial hierarchy.
The result is immediate by the definition of the polynomial hierarchy.

\begin{theorem}
The problem of
whether a formula belongs to all preferred$^L$ extensions
of a default theory is in $\Pi^p_3$.
\end{theorem}

Next we show that the decision problem is $\Delta^p_3$-hard,
thereby obtaining a lower bound on the location in the polynomial hierarchy.
This result is based on a theorem by Krentel \citeyear{Krentel92} that identifies
$\Delta^p_k$-complete problems for $k\geq 1$.
The theorem concerns lexicographically maximal valuations of
quantified Boolean formulae,
and for the prefix $\exists\forall$ it is as follows.

\begin{theorem}[Krentel, 1992]
The problem of computing a given component of $X^1$ is $\Delta^p_3$-complete,
where $X^1$ is defined as follows.
\begin{quote}
{\sc Maximum $2$-quantified formula} \\
{\em Instance:} Boolean formula $C\lbrack X^1,X^2\rbrack$
where $X^i$ is an abbreviation for an $n$-tuple of Boolean variables that
corresponds to a valuation of $x^i_1,\ldots,x^i_n$. \\
{\em Output:} Lexicographically maximal $X^1\in\{0,1\}^n$ that satisfies
\[ \exists X^1\forall X^2 (C\lbrack X^1,X^2\rbrack = 1). \]
\end{quote}
\end{theorem}

The following lemma points out a connection between
quantified Boolean formulae with a universal quantifier as
the outermost quantifier
and the logical consequence relation in propositional logic.

\begin{lemma}\label{le:EAqbf}
Let $X$ be a set containing exactly one of $x$ and $\neg x$ for
every $x\in\{ x^1_1,\ldots,x^1_n\}$.
Let $X^1 =  \langle x'^1_1,\ldots,x'^1_n\rangle$ where
$x'^1_i = 1$ if $x^1_i\in X$ and $x'^1_i = 0$ otherwise.
Then $X^1$ satisfies $\forall X^2(C\lbrack X^1,X^2\rbrack)$
if and only if $X\models C\lbrack X^1,X^2\rbrack$.
\end{lemma}

\begin{proof}
Assume that $X^1$ satisfies $\forall X^2(C\lbrack X^1,X^2\rbrack)$.
Hence for the choice of truth values for $x^1_1,\ldots,x^1_n$ indicated
by $X^1$ and any choice of truth values for $x^2_1,\ldots,x^2_n$,
$C\lbrack X^1,X^2\rbrack$ is true.
Now let $M$ be any model such that $M\models X$.
Hence $M$  assigns the same truth values to $x^1_1,\ldots,x^1_n$ as $X^1$.
Now $M\models C\lbrack X^1,X^2\rbrack$, and by the definition of
logical consequence $X\models C\lbrack X^1,X^2\rbrack$.

Assume that $X\models C\lbrack X^1,X^2\rbrack$. Hence for all models $M$
such that $M\models X$ and $M$ assigns any truth-values to
$x^2_1,\ldots,x^2_n$, $M\models C\lbrack X^1,X^2\rbrack$.
By definition of quantified Boolean formulae,
for $X^1$ and any $X^2$ the formula $C\lbrack X^1,X^2\rbrack$ is true,
that is, $X^1$ satisfies $\forall X^2(C\lbrack X^1,X^2\rbrack)$.
\end{proof}

The proof of the next lemma uses the same translation of quantified Boolean
formulae to default theories as Gottlob's proof of $\Pi^p_2$-hardness
of cautious reasoning in Reiter's default logic \cite{Gottlob92}.

\begin{lemma}\label{le:m2qcreduction}
Computing a given component of $X^1$ in {\sc Maximum $2$-quantified formula}
is polynomial time many-one reducible to the problem of testing
whether a formula belongs to all ${\cal T}$-preferred$^L$ extensions of
a default theory for strict total orders ${\cal T}$.
\end{lemma}

\begin{proof}
We construct a default theory $\Delta = \langle D,\emptyset\rangle$ and define
a strict partial order ${\cal P}$ on $D$ so that
the $k$th component of $X^1$ is 1 if and only if
$\Delta\models^L_{\cal P}x^1_k$.
The value of a given component of $X^1$ in {\sc Maximum 2-quantified formula}
is defined only if $\exists X^1\forall X^2(C\lbrack X^1,X^2 \rbrack)$
is satisfiable, so assume it is.
Let $a$ be a propositional variable that is not in
$\{x^1_1,\ldots,x^1_n,x^2_1,\ldots,x^2_n\}$. Define
\begin{eqnarray*}
D & = & \left\{ \pfdefr{x^1_1}, \pfdefr{\neg x^1_1},\ldots,\pfdefr{x^1_n}, \pfdefr{\neg x^1_n}, \ndefr{C\lbrack X^1,X^2\rbrack}{a}\right\}, \mbox{ and}\\
{\cal P} & = &
\left\{\ndefr{C\lbrack X^1,X^2\rbrack}{a}\right\}\times\left(D\setd\left\{\ndefr{C\lbrack X^1,X^2\rbrack}{a}\right\}\right)\\
& \cup &
\left\{\left.\left\langle\pfdefr{x^1_i},\pfdefr{x^1_j}\right\rangle\right| 1\leq i<j\leq n\right\}
\\
& \cup &
\left\{\pfdefr{x^1_1},\ldots,\pfdefr{x^1_n}\right\}\times\left\{\pfdefr{\neg x^1_1},\ldots,\pfdefr{\neg x^1_n}\right\}.
\end{eqnarray*}
Let ${\cal T}$ be any strict total order on $D$ that extends ${\cal P}$.
The sizes of the default theory $\langle D,\emptyset\rangle$ and the
strict total order ${\cal T}$ are linearly proportional to the size
of $C\lbrack X^1,X^2\rbrack$, and they can be constructed in polynomial time.

First we show that for each extension $E$ of $\langle D,\emptyset\rangle$
that contains $a$ there is $X^1$ such that 
$X^1$ satisfies $\forall X^2(C\lbrack X^1,X^2\rbrack)$
and for all $i\in\{1,\ldots,n\}$, $p_i(X^1) = 1$ iff $x^1_i\in E$
(the function $p_i$ selects the $i$th element of an $n$-tuple.)
Let $E$ be an extension of $\langle D,\emptyset\rangle$ and $a\in E$.
Because defaults in $D$ are normal, $E$ is consistent.
Hence $\applied{\ndefr{C\lbrack X^1,X^2\rbrack}{a}}{E}$ because
the only default where $a$ occurs in the conclusion
is $\ndefr{C\lbrack X^1,X^2\rbrack}{a}$.
Hence $C\lbrack X^1,X^2\rbrack\in E$; that is,
$C\lbrack X^1,X^2\rbrack$ is a logical consequence of the conclusions
of generating defaults of $E$.
Because $a$ does not occur in $C\lbrack X^1,X^2\rbrack$,
$X\models C\lbrack X^1,X^2\rbrack$ for
$X = E\cap\{x^1_1,\neg x^1_1,\ldots,x^1_n,\neg x^1_n\}$.
By Lemma \ref{le:EAqbf} $X^1$,
defined as $p_i(X^1) = 1$ if $x^1_i\in X$ and $p_i(X^1) = 0$ otherwise,
satisfies $\forall X^2(C\lbrack X^1,X^2\rbrack)$.

Then we show that for each $X^1$ that satisfies
$\forall X^2(C\lbrack X^1,X^2\rbrack)$,
there is an extension $E$ of $\langle D, \emptyset\rangle$ such that
$a\in E$ and $p_i(X^1) = 1$ iff $x^1_i\in E$.
Assume that $X^1$ satisfies $\forall X^2(C\lbrack X^1,X^2\rbrack)$.
Let $X=\{x^1_i|p_i(X^1)=1,1\leq i\leq n\}\cup\{\neg x^1_i|p_i(X^1)=0,1\leq i\leq n\}$.
It is straightforward to verify that $E$ is an extension of $\langle D,\emptyset\rangle$.
Because the extension $E$ is consistent, $\applied{\ndefr{C\lbrack X^1,X^2\rbrack}{a}}{E}$.
Because $\ndefr{C\lbrack X^1,X^2\rbrack}{a}$ is the ${\cal P}$-least
default in $D$, all ${\cal T}$-preferred$^L$ extensions apply
$\ndefr{C\lbrack X^1,X^2\rbrack}{a}$.

The counterpart of the ${\cal T}$-preferred$^L$ extension is the lexicographically maximal $X^1$, and vice versa. This is by the construction of ${\cal T}$,
where the defaults $\pfdefr{x^1_1},\ldots,\pfdefr{x^1_n}$ are
ordered as $\pfdefr{x^1_i}{\cal T}\pfdefr{x^1_j}$ whenever $i<j$.
Therefore $p_i(X^1) = 1$ for the maximal $X^1$ satisfying
$\forall X^2(C\lbrack X^1,X^2\rbrack)$ iff
$x^1_i$ belongs to the ${\cal T}$-preferred$^L$ extension of $\langle D,\emptyset\rangle$.
\end{proof}

Notice that Lemma \ref{le:m2qcreduction} cannot be
reconstructed in the prioritized default logics by Brewka and by Baader
and Hollunder
because the construction is based on a highest priority default that
becomes applicable only after a number of lower priority defaults
have been applied, and in these cases those logics
do not work like the lexicographic prioritized default logic.
While testing $\models^L_{{\cal T}}$ for strict total orders ${\cal T}$
is higher in the polynomial hierarchy
than cautious reasoning in unprioritized default logic, 
testing $\models^{\ms{B}}_{\cal T}$ and $\models^{\ms{BH}}_{\cal T}$
is one level lower.

\begin{theorem}\label{th:delta3hard}
For default theories $\Delta = \langle D, W\rangle$,
strict total orders ${\cal T}$ on $D$, and formulae $\phi$,
the problem of testing $\Delta\models^L_{\cal T}\phi$ is $\Delta^p_3$-hard.
\end{theorem}

\begin{proof}
All problems in $\Delta^p_3$ are polynomial time many-one reducible to
{\sc Maximum 2-quantified formula}, which by Lemma \ref{le:m2qcreduction}
is polynomial time many-one reducible to our problem.
\end{proof}

Testing $\models^L_{\cal T}$ for strict total orders ${\cal T}$
is in $\Delta^p_3$.
The proof of this fact is based on computing the unique preferred
extensions step by step, at each step determining whether
there is an extension in which one of the defaults is applied
in addition to those defaults which we have already committed to.

\begin{figure}
\zeroc{{\rwprocedure} exists($D$,$W$,$A$);}
\twoc{guess a subset $G$ of conclusions of defaults in $D$;}
\twoc{$E$ := $G\cup W$;}
\twoc{{\rwif} not extension($D,W,E$) {\rwthen} {\rwreturn} false;}
\twoc{{\rwforeach} $\defr{\alpha}{\beta_1,\ldots,\beta_n}{\gamma}\in A$ {\rwdo}}
\fourc{{\rwif} $\langle E,\alpha\rangle\not\in$ CN or $\langle E,\neg\beta\rangle\in$ CN for some $\beta\in\{\beta_1,\ldots,\beta_n\}$}
\fourc{{\rwthen} {\rwreturn} false}
\twoc{{\rwend};}
\twoc{{\rwreturn} true}
\zeroc{{\rwend}}
\caption{A procedure that tests for the existence of extensions}\label{fi:d3texists}
\end{figure}
\begin{lemma}\label{le:d3texists}
For the procedure in Figure \ref{fi:d3texists}, 
the call exists($D,W,A$) returns true if and only if
there is an extension $E$ of $\langle D,W\rangle$ such that
$\applied{\delta}{E}$ for all $\delta\in A$.
The procedure runs in nondeterministic polynomial time given an NP oracle
for CN.
\end{lemma}

\begin{proof}
First the procedure guesses a set of conclusions $G$
that possibly are the conclusions of the generating defaults
of the possible extension $\Cn{G\cup W}$.
The call to extension($D,W,E$) with $E = G\cup W$ tests if this is
indeed the case (Lemma \ref{le:pextension}.)
Next the procedure tests whether defaults in $A$ are applied in $\Cn{G\cup W}$,
and returns true if and only if this is the case.
Because the procedure represents a nondeterministic Turing machine,
the procedure returns true if and only if it is possible to guess $G$
so that $\Cn{G\cup W}$ is an extension where members of $A$ is applied.
Hence {\em exists}($D,W,A$) returns true if and only if
there is an extension $E$ of $\langle D,W\rangle$ such that
$\applied{\delta}{E}$ for all $\delta\in A$.

The procedure runs in non-deterministic polynomial time and
uses an NP oracle for propositional satisfiability.
Hence the problem solved by it is in $\Sigma^p_2$.
\end{proof}

\begin{theorem}\label{th:delta3total}
For default theories $\Delta = \langle D, W\rangle$, formulae $\phi$,
and strict total orders ${\cal T}$ on $D$,
the problem of testing $\Delta\models^L_{\cal T}\phi$ is in $\Delta^p_3$.
\end{theorem}

\begin{proof}
We give a decision procedure for the problem that runs in deterministic
polynomial time and uses an oracle for a problem that belongs to $\Sigma^p_2$.
This demonstrates that the problem is in $\Delta^p_3$.
The procedure {\em decide} is given in Figure \ref{fi:delta3}
and the $\Sigma^p_2$ oracle procedure {\em exists} is given in
Figure \ref{fi:d3texists} and its correctness is stated in
Lemma \ref{le:d3texists}.
\begin{figure}
\zeroc{{\rwprocedure} decide($D$,$W$,${\cal T}$,$\phi$);}
\twoc{{\rwif} not exists($D,W,\emptyset$) {\rwthen} {\rwreturn} true;}
\twoc{$A$ := $\emptyset$;}
\twoc{let $\delta_1, \ldots,\delta_n$ be the ordering ${\cal T}$;}
\twoc{{\rwfor} $i$ := $1$ {\rwto} $n$ {\rwdo}}
\fourc{{\rwif} exists($D,W,A\cup\{\delta_i\}$) {\rwthen} $A$ := $A\cup\{\delta_i\}$}
\twoc{{\rwend}}
\twoc{$E$ := $W\cup\{ \gamma | \defr{\alpha}{\sigma}{\gamma}\in A \}$;}
\twoc{{\rwif} $E\models\phi$ {\rwthen} {\rwreturn} true {\rwelse} {\rwreturn} false}
\zeroc{{\rwend}}
\caption{A decision procedure for total priorities}\label{fi:delta3}
\end{figure}
The correctness of the procedure {\em decide} is as follows.
Let $\langle D,W\rangle$ be a finite default theory with $|D| = n$,
${\cal T}$ a strict total order on $D$, and $\phi$ a formula.
Assume that $\langle D,W\rangle$ has no extensions. In this case the first
statement in the procedure {\em decide} returns true which is correct
because $\phi$ trivially belongs to all extensions of $\langle D,W\rangle$.
Assume that $\langle D,W\rangle$ has at least one extension.
The correctness proof in this case proceeds by induction on
$i\in\{1,\ldots,n\}$.
The value of the program variable $A$ after the $i$th iteration is
denoted by $A_i$.
Let $\delta_1,\ldots,\delta_n$ be the ordering ${\cal T}$.
Because
${\cal T}$ is a strict total order on $D$,
by Lemma \ref{le:texistence} there is exactly one
${\cal T}$-preferred$^L$ extension $E$ of $\langle D,W\rangle$.

\IH
for all $j\in\{1,\ldots,i\}$, $\applied{\delta_j}{E}$ if and only if
$\delta_j\in A_i$.

\BC{$i=0$} Now $A_0 = \emptyset$ and $\{1,\ldots,i\}=\emptyset$.
Hence the hypothesis is true.

\IC{$i\geq 1$}
We analyze the value $b$ returned by exists($D,W,A_{i-1}\cup\{\delta_i\}$)
by cases.
Assume that $b = $ true.
Hence $A_i = A_{i-1}\cup\{\delta_i\}$.
By the correctness of the procedure {\em exists},
there is an extension $E'$ such that
$\applied{\delta}{E'}$ for all $\delta\in A_{i-1}\cup\{\delta_i\}$.
Assume that $E$ is not such an extension.
Hence $\appliet{\delta_i}{E'}{E}$.
By induction hypothesis $\applied{\delta_j}{E}$ iff $\delta_j\in A_{i-1}$
for all $j\in\{1,\ldots,i-1\}$.
Now because $\applied{\delta}{E}$ implies $\applied{\delta}{E'}$ for all
$\delta{\cal T}\delta_i$ there are no $\delta''{\cal T}\delta_i$
such that $\appliet{\delta''}{E}{E'}$.
Hence $E$ could not be ${\cal T}$-preferred$^L$, and the assumption that not
$\applied{\delta_i}{E}$ was wrong.
Assume that $b = $ false.
As there is no extension $E'$ such that $\applied{\delta}{E'}$ for all
$\delta\in A_{i-1}\cup\{\delta_i\}$,
and $\applied{\delta}{E}$ for all $\delta\in A_{i-1}$,
not $\applied{\delta_i}{E}$.
Now $A_i = A_{i-1}$, and the induction hypothesis is fulfilled.
This finishes the induction proof.

Now $A_n$ is the set of generating defaults of the unique ${\cal T}$-preferred$^L$
extension $E$ of $\langle D,W\rangle$.
The execution of the program continues at the last statement of the procedure.
By Theorem \ref{th:generatingdefaults}
$E = \Cn{W\cup\{ \gamma | \defr{\alpha}{\sigma}{\gamma}\in A_n\}}$.
Hence $\phi\in E$ if and only if
$W\cup\{\gamma|\defr{\alpha}{\sigma}{\gamma}\in A_n\}\models\phi$.
\end{proof}

\begin{corollary}
For default theories $\Delta = \langle D, W\rangle$,
strict total orders ${\cal P}$ on $D$, and formulae $\phi$,
the problem of testing $\Delta\models^L_{\cal P}\phi$ is $\Delta^p_3$-complete.
\end{corollary}

\begin{proof}
Directly by Theorems \ref{th:delta3hard} and \ref{th:delta3total}.
\end{proof}

For the problem of membership of formulae all preferred extensions
of a default theory without the restriction to total priorities,
the membership in $\Delta^p_3$ as well as its $\Pi^p_3$-hardness remain open. 

\subsection{Complexity in Syntactically Restricted Cases}\label{se:tractability}

As in Section \ref{se:semirestricted},
we analyze the complexity of the consequence relation
of the lexicographic prioritized default logic
under syntactic restrictions.

\subsubsection{Summary}

The results on the boundary between tractability and intractability for
$\models^L_{\cal P}$ with strict total orders ${\cal P}$
are summarized in Table \ref{ta:tsummary}.
In cases where the complexity of the lexicographic prioritized default logic
differs from Reiter's default logic, the complexity is set in boldface.
Table \ref{ta:tsummaryrefs} indicates where the proofs of the complexity
results can be found.
The impact of priorities on the complexity of the decision problems is
strongest in the prerequisite-free normal classes.
When the default rules in these classes are totally ordered, the unique
preferred extensions can be easily found by applying the default rules
in the given order.
A more complicated polynomial time decision procedure exists for
Horn defaults with 1-literal objective facts (Theorem \ref{th:totalnormalhorn}).
For this class, the existence of an extension that applies a given set of
defaults can be determined in polynomial time, and this together
with the stepwise construction of preferred extensions given as
the procedure in Figure \ref{fi:delta3} yields a fast decision procedure.

% SUMMARY OF COMPLEXITY RESULTS FOR TOTAL PRIORITIES
\begin{table}
\begin{tabular}{rl|lll}
& class of default theories & \multicolumn{3}{l}{complexity when clauses in W are} \\
& & Horn & 2-literal & 1-literal \\ \hline

1 &
disjunction-free &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\NPH & \NPH & \NPH \\

2 &
unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{q \conj\neg r}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\NPH & \NPH & \NPH \\

3 &
disjunction-free ordered &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\NPH & \NPH & \NPH \\

4 &
ordered unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{q\conj\neg r}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\NPH & \NPH & \NPH \\

5 &
disjunction-free normal &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$ &
\NPH & \NPH & \NPH \\

6 &
Horn &
%$\odefr{p_1\conj\cdots\conj p_n}{q}{q}$
%$\odefr{p_1\conj\cdots\conj p_n}{\neg q}{\neg q}$ &
\NPH & \NPH & \dlePTIME \\

7 &
normal unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\NPH & \NPH & \PTIME \\

8 &
prerequisite-free &
%$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\NPH & \NPH & \NPH \\

9 &
prerequisite-free ordered &
%$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\NPH & \NPH & \NPH \\

10 &
prerequisite-free unary &
%$\odefr{}{q}{q}$
%$\odefr{}{q\conj\neg r}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\NPH & \NPH & \NPH \\

11 &
prerequisite-free ordered unary &
%$\odefr{}{q}{q}$
%$\odefr{}{q\conj\neg r}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\NPH & \NPH & \NPH \\

12 &
prerequisite-free normal &
%$\odefr{}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$ &
\dlePTIME & \dlePTIME & \dlePTIME \\

13 &
prerequisite-free normal unary &
%$\odefr{}{q}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\dlePTIME & \dlePTIME & \PTIME \\

14 &
prerequisite-free positive normal unary &
%$\odefr{}{q}{q}$ &
\dlePTIME & \dlePTIME & \PTIME \\
\end{tabular}
%\vskip1cm
%\begin{tabular}{rlrl}
%1 & disjunction-free & 8 & prerequisite-free \\
%2 & unary & 9 & prerequisite-free ordered \\
%3 & disjunction-free ordered & 10 & prerequisite-free unary \\
%4 & ordered unary & 11 & prerequisite-free ordered unary \\
%5 & disjunction-free normal & 12 & prerequisite-free normal \\
%6 & Horn & 13 & prerequisite-free normal unary \\
%7 & normal unary & 14 & prerequisite-free positive normal unary 
%\end{tabular}
\vskip5mm
\caption{Complexity of the consequence relation $\models^L$ with total priorities}\label{ta:tsummary}
\end{table}

\begin{table}
\begin{tabular}{rl|lll}
& class of default theories & \multicolumn{3}{l}{reference}  \\
& & Horn & 2-literal & 1-literal \\ \hline
1 & disjunction-free & $4\subseteq$ & $4\subseteq$ & $4\subseteq$ \\
2 & unary & $4\subseteq$ & $4\subseteq$ & $4\subseteq$ \\
3 & disjunction-free ordered & $5\subseteq$ & $5\subseteq$ & $5\subseteq$ \\
4 & ordered unary & C\ref{co:Aintractability2} & C\ref{co:Aintractability2} & C\ref{co:Aintractability2} \\
5 & disjunction-free normal & C\ref{co:Aintractability1}  & C\ref{co:Aintractability1}  & C\ref{co:Aintractability1} \\
6 & Horn & $7\subseteq$ & $7\subseteq$ & T\ref{th:totalnormalhorn} \\
7 & normal unary & C\ref{co:Aintractability2} & C\ref{co:Aintractability2} & $\subseteq$ 6 \\
8 & \prerequisitefree & $11\subseteq$ & $11\subseteq$ & $11\subseteq$ \\
9 & \prerequisitefree ordered & $11\subseteq$ & $11\subseteq$ & $11\subseteq$ \\
10 & \prerequisitefree unary & $11\subseteq$ & $11\subseteq$ & $11\subseteq$ \\
11 & \prerequisitefree ordered unary & C\ref{co:Aintractability2} & C\ref{co:Aintractability2} & C\ref{co:Aintractability2} \\
12 & \prerequisitefree normal & T\ref{th:totalpfreenormal}& T\ref{th:totalpfreenormal}& T\ref{th:totalpfreenormal} \\
13 & \prerequisitefree normal unary & $\subseteq$ 12 & $\subseteq$ 12 & $\subseteq$ 12 \\
14 & \prerequisitefree positive normal unary & $\subseteq$ 12 & $\subseteq$ 12 & $\subseteq$ 12
\end{tabular}
\vskip5mm
\caption{References to theorems on the complexity of $\models^L$ with total priorities}\label{ta:tsummaryrefs}
\end{table}

\subsubsection{Intractable Classes with Total Priorities}\label{se:intractableclasses}

The next theorems are based on reductions from intractable problems
of brave reasoning in Reiter's default logic to prioritized default
logic with total priorities.

\begin{theorem}\label{th:braveAreduction}
Let ${\cal F}$ be a class of formulae and ${\cal C}$ a class of
finite default theories such that
\begin{itemize}
\item if $\langle D,W\rangle\in {\cal C}$, then
$\langle D\cup\{ \ndefr{\phi}{p}\},W\rangle\in{\cal C}$ where
$\phi\in{\cal F}$ and $p$ is a propositional variable that does not occur in
$D$ or $W$, and
\item each member of ${\cal C}$ has at least one extension.
\end{itemize}
The problem of testing $\Delta\models_b\phi$ for
$\Delta\in{\cal C}$ and $\phi\in{\cal F}$
is polynomial time many-one reducible to the problem of testing
$\Delta'\models^L_{\cal P}p$ where
$\Delta'\in{\cal C}$, $p$ is a propositional variable, and
${\cal P}$ is a strict total order on defaults in $\Delta'$.
\end{theorem}

\begin{proof}
Let $\langle D, W\rangle\in{\cal C}$ be a default theory,
$\phi\in{\cal F}$ a formula, and $k$ a propositional variable that does
not occur in $\langle D,W\rangle$ or $\phi$.
Let ${\cal P}$ be any strict partial order on $D\cup\{ \ndefr{\phi}{k} \}$
such that $\ndefr{\phi}{k}$ is the ${\cal P}$-least element.
We claim that $\langle D, W\rangle\models_b\phi$ if and only if
$\langle D\cup\{ \ndefr{\phi}{k}\}, W\rangle\models^L_{\cal P} k$.
This is directly because the highest priority default is applied
in all preferred$^L$ extensions if it is possible to apply it, and
$k$ belongs to those extensions if and only if $\phi$ belongs to them.
\end{proof}

As a corollary, together with a theorem that shows the intractability
of brave reasoning of the class in Reiter's default logic \cite{Kautz91},
we obtain the following result.

\begin{corollary}\label{co:Aintractability1}
Testing $\langle D,W\rangle\models^L_{\cal P}l$
for strict total orders ${\cal P}$, literals $l$,
and disjunction-free normal default theories $\langle D,W\rangle$
where $W$ is a set of literals, is NP-hard.
\end{corollary}

\begin{theorem}\label{th:braveAreduction2}
Let ${\cal C}$ be a class of finite default theories such that
the conclusion of each default is a literal
and each member of ${\cal C}$ has at least one extension.
The problem of testing $\Delta\models_b l$ for
$\Delta\in{\cal C}$ and literals $l$
is polynomial time many-one reducible to the problem of testing
$\Delta\models^L_{\cal T}l$ where
${\cal T}$ is a strict total order on defaults in $\Delta$.
\end{theorem}

\begin{proof}
Let $\Delta = \langle D,W\rangle$ be a default theory in ${\cal C}$.
We reduce testing $\Delta\models_bl$ to $\Delta\models^L_{\cal T}l$ as
follows.
Let $D'$ be the set of defaults with $l$ as the conclusion.
Let ${\cal T}$ be a strict total order on $D$ such
that $D'\times(D\setd D')\subseteq{\cal T}$.
We claim that $\Delta\models_bl$ if and only if $\Delta\models^L_{\cal T}l$.

Assume that $\Delta\not\models_bl$.
Because by assumption there is at least one extension of $\Delta$,
by Lemma \ref{le:texistence} there is exactly one 
${\cal T}$-preferred$^L$ extension $E$ of $\Delta$.
Clearly $l\not\in E$.
Therefore $\Delta\not\models^L_{\cal T}l$.

Assume that $\Delta\models_bl$.
Then there is an extension $E$ of $\Delta$ such that $l\in E$.
If $W\models l$, then clearly $\Delta\models^L_{\cal T}l$.
Assume that $W\not\models l$.
Now $\applied{\delta}{E}$ for some $\delta\in D'$.
Assume that $E'$ is an extension of $\Delta$ such that $l\not\in E$.
Now $\appliet{\delta}{E}{E'}$.
As $\delta'\in D'$ for all $\delta'{\cal T}\delta$ and
not $\applied{\delta'}{E'}$ for all $\delta'\in D'$,
there is no $\delta'{\cal T}\delta$ such that $\appliet{\delta'}{E'}{E}$.
Hence $E'$ is not ${\cal T}$-preferred$^L$.
Therefore $l$ belongs to all ${\cal T}$-preferred$^L$ extensions of $\Delta$
and $\Delta\models^L_{\cal T}l$.
\end{proof}

The following corollary is obtained with
the intractability results of brave reasoning
by Kautz and Selman \citeyear{Kautz91} and Stillman \citeyear{Stillman90}
for the classes mentioned.

\begin{corollary}\label{co:Aintractability2}
Testing $\langle D,W\rangle\models^L_{\cal P}l$
for strict total orders ${\cal P}$ and literals $l$
in any of the classes of default theories below is NP-hard.

\begin{tabular}{ll}
$D$ & $W$ \\ \hline
normal unary & Horn clauses \\
normal unary & 2-literal clauses \\
ordered unary & literals \\
prerequisite-free ordered unary & literals
\end{tabular}
\end{corollary}

\subsubsection{Tractable Classes}\label{se:tractableclasses}

Next we give a restricted tractable class of prioritized
default theories for which the unique ${\cal P}$-preferred$^L$
extensions can be computed by using ${\cal P}$ as the order in which
the application of defaults is attempted.
Exhaustive search is avoided because there is no need to retract
a decision to apply a default.
The theorem is given in a general form for any tractable subset of
classical propositional logic, like Horn clauses, 2-literal clauses,
or 1-literal clauses.
The theorem and the algorithm are part of the folklore of nonmonotonic
reasoning.

\begin{theorem}\label{th:totalpfreenormal}
Let ${\cal F}$ be a class of formulae such that satisfiability testing
for $S\subseteq {\cal F}$ takes polynomial time in the size of $S$.
Let ${\cal C}$ be a class of default theories $\langle D,W\rangle$ such
that $D = \{ \pfdefr{\phi} | \phi\in F\}$ for some finite set
$F\subseteq{\cal F}$ and $W\subseteq{\cal F}$ is finite.
Then for $\Delta\in{\cal C}$, $\phi\in{\cal F}$, and strict total orders
${\cal P}$ on the defaults in $\Delta$, the problem of testing
$\Delta\models^L_{\cal P}\neg\phi$
is solvable in polynomial time on the size of $D\cup W\cup\{ \neg\phi \}$.
\end{theorem}

\begin{proof}
By Lemma \ref{le:texistence} there is at most one ${\cal P}$-preferred$^L$
extension for each member of ${\cal C}$,
and because the defaults in members of ${\cal C}$ are normal,
there is at least one extension for each member
of ${\cal C}$ by Theorem 3.1 in \cite{Reiter80}.
Therefore there is exactly one ${\cal P}$-preferred$^L$ extension for each
member of ${\cal C}$.
A decision procedure for the class of default theories stated in the theorem
is given in Figure \ref{fi:prfreenormal}.
The procedure computes a set $E$ that consists of $W$ and the conclusions of
the generating defaults of the extension $\Cn{E}$ of $\langle D,W\rangle$,
and returns {\em true} if and only if $E\models\phi$.

Let $\pfdefr{\phi_1},\ldots,\pfdefr{\phi_n}$ be the ordering
${\cal P}$ of defaults in $D$.
If $W$ is inconsistent the procedure returns {\em true}.
In this case $\Cn{W} = \langcl$ is the only extension of $\langle D,W\rangle$
which agrees with the statement of the lemma.
Otherwise extensions of $\langle D,W\rangle$ are consistent.
Define $D_i = \{ \pfdefr{\phi_1},\ldots,\pfdefr{\phi_i}\}$
and $\Pi_i = \{ \phi_1,\ldots,\phi_i\}$ for all $i\in\{0,\ldots,n\}$.
The correctness proof is by induction on $i$ and we obtain
the ${\cal P}$-preferredness$^L$ of $\Cn{E}$ as the case $i = n$.

\IH for all $j\in\{0,\ldots, i\}$,
if $W$ is consistent, $E_j$ is a maximal consistent subset
of $\Pi_j\cup W$ such that $W\subseteq E_j$,
and $\Cn{E_i}$ is a ${\cal P}\cap(D_i\times D_i)$-preferred$^L$
extension of $\langle D_i,W\rangle$.

\begin{figure}
\zeroc{{\rwprocedure} decide($D,W,{\cal P},\phi$)}
\twoc{{\rwlet} $\pfdefr{\phi_1},\pfdefr{\phi_2},\ldots,\pfdefr{\phi_n}$ be the ordering ${\cal P}$ on $D$;}
\twoc{$E_0 := W$;}
\twoc{{\rwfor} $i := 1$ {\rwto} $n$ {\rwdo}}
\fourc{{\rwif} $E_{i-1}\cup\{ \phi_i \}$ is consistent (equivalently, $E_{i-1}\not\models\neg\phi_i$)}
\fourc{{\rwthen} $E_i := E_{i-1}\cup\{ \phi_i \}$}
\twoc{{\rwend};}
\twoc{$E := E_n$;}
\twoc{{\rwif} $E\models\phi$}
\twoc{{\rwthen} {\rwreturn} true {\rwelse} {\rwreturn} false}
\zeroc{{\rwend}}
\caption{A decision procedure for a class of prerequisite-free normal default theories}\label{fi:prfreenormal}
\end{figure}
The induction proof is straightforward. That the procedure
runs in polynomial time on the size of $\langle D,W\rangle$ is also
obvious.
Thus any polynomial time subset ${\cal C}$ of classical propositional logic
produces a tractable class of default theories.
\end{proof}

Without priorities reasoning with prerequisite-free normal default rules
and Horn clauses is NP-complete \cite{Stillman90}.
For normal defaults, tractability can be obtained also for defaults
with prerequisites if suitable restrictions
are imposed on the prerequisites, conclusions, and the objective
parts of the default theories. Next we present such a class that is neither
subsumed by nor subsumes the tractable prerequisite-free classes.
The idea behind the result is the same as the one used in the proof of
Theorem \ref{th:delta3total}.
Corollary \ref{co:Aintractability1} indicates that the result cannot be
generalized (assuming P$\neq$NP) to any of the classes higher
in the Kautz and Selman hierarchy.

\begin{theorem}\label{th:totalnormalhorn}
Let ${\cal C}$ be the class of Horn default theories $\langle D,W\rangle$ where
$W$ is a finite set of literals and defaults in $D$ are of the form
$\ndefr{p_1\conj\cdots\conj p_n}{l}$ where $l$ is a literal and $p_1,\ldots,p_n$ are propositional variables.
For $\Delta\in{\cal C}$, negated Horn clauses $\phi$,
and strict total orders ${\cal P}$ on the defaults in $\Delta$,
the problem of testing
$\Delta\models^L_{\cal P}\neg\phi$
is solvable in polynomial time on the size of $D\cup W\cup\{ \neg\phi \}$.
\end{theorem}

\begin{proof}
The body of the decision procedure is given in Figure \ref{fi:delta3}
and its correctness proof is included in the proof of Theorem
\ref{th:delta3total}.
Here we use the subprocedure {\em exists}
in Figure \ref{fi:normaltractableexists}.
The procedure {\em exists} runs in polynomial time on the size of
$D\cup W\cup A$ because the number of iterations in the repeat-until loop
is at most $|D'| \leq |D|$ and logical consequence tests
with propositional Horn clauses can be performed in polynomial time.
Next we prove that the procedure {\em exists} called with arguments $(D,W,A)$
returns {\em true} if and only if there is an extension $E$ of
$\Delta=\langle D, W\rangle$ such that $A\subseteq\GD{E}{\Delta}$.
The correctness proof and the algorithm are based on the idea that to derive
the prerequisites of defaults in $A$, defaults in $D\setd A$ with a negative
conclusion are not needed.
\begin{figure}
\zeroc{{\rwprocedure} exists($D,W,A$)}
\twoc{{\rwif} $A\neq\emptyset$ and $W\cup\{\pi|\ndefr{\alpha}{\pi}\in A\}\models\bot$ {\rwthen} {\rwreturn} false;}
\twoc{$D' := A\cup\{\ndefr{\alpha}{p}\in D|\neg p\not\in W, \ndefr{\alpha'}{\neg p}\not\in A, p\mbox{ is atomic}\}$;}
\twoc{$E$ := $W$;}
\twoc{{\rwrepeat}}
\fourc{$E'$ := $E$;}
\fourc{{\rwforeach} $\ndefr{\alpha}{\pi}\in D'$ {\rwdo}}
\sixc{{\rwif} $E'\models\alpha$ {\rwthen} $E$ := $E\cup\{\pi\}$}
\fourc{{\rwend}}
\twoc{{\rwuntil} $E = E'$;}
\twoc{{\rwif} $E\not\models\alpha$ for some $\ndefr{\alpha}{\pi}\in A$
      {\rwthen} {\rwreturn} false}
\twoc{{\rwelse} {\rwreturn} true}
\zeroc{{\rwend}}
\caption{A subprocedure of a decision procedure}\label{fi:normaltractableexists}
\end{figure}

First we show that {\em exists} returns true if and only if there is an
extension $E'$ of $\Delta' = \langle D',W\rangle$ such that
$A\subseteq\GD{E'}{\Delta'}$, where
$D'=A\cup\{\ndefr{\alpha}{p}\in D|\neg p\not\in W,\ndefr{\alpha'}{\neg p}\not\in A, p\mbox{ is atomic}\}$.
If $W\cup\{\pi|\ndefr{\alpha}{\pi}\in A\}$ is inconsistent and
$A\neq\emptyset$, then there are no extensions that apply $A$, and hence
it is correct to return {\em false}.
So assume $W\cup\{\pi|\ndefr{\alpha}{\pi}\in A\}$ is consistent.
Now the set $U = W\cup \{\pi|\ndefr{\alpha}{\pi}\in D'\}$
is consistent by definition of $D'$.
Any extension $E'$ of $\Delta'$ satisfies $E'\subseteq\Cn{U}$,
and because all defaults in $D'$ are normal,
no negation of a justification of a default in $D'$ is in $\Cn{U}$.
Therefore exactly those defaults are applied in extensions of $\Delta'$
for which the prerequisite is derivable. It is straightforward to show
that the procedure computes the union $E$ of $W$ and the set of conclusions
of the unique such set of defaults,
and hence $\Cn{E}$ is the unique extension of $\Delta'$.
Finally,
the procedure returns false if and only if $\alpha\not\in E$
for some $\ndefr{\alpha}{\pi}\in A$.
This is equivalent to the fact that $\delta\not\in\GD{E}{\Delta'}$ for some
$\delta\in A$, and hence $A\not\subseteq\GD{E}{\Delta'}$.

Then we show that there is an extension $E'$ of $\Delta'$ such that
$A\subseteq\GD{E'}{\Delta'}$ if and only if there is an extension
$E$ of $\Delta$ such that $A\subseteq\GD{E}{\Delta}$.
The ``only if'' direction directly follows from Theorem 3.2 in \cite{Reiter80}
because $D'\subseteq D$ and $D$ is normal.
Assume that there is an extension $E$ of $\Delta$ such that
$A\subseteq\GD{E}{\Delta}$.
It is straightforward to show that
$E$ is an extension of $\langle \GD{E}{\Delta}, W\rangle$.
Next we remove defaults with negative conclusions that are
in $D$ but not in $A$:
an induction proof with Theorem \ref{th:semiconstructive}
and the induction hypothesis
$E''_i = \Cn{E_i\cap(\{\pi|\ndefr{\alpha}{\pi}\in A\}\cup\{p | \ndefr{\alpha}{p}\in\GD{E}{\Delta}, p\mbox{ is atomic} \}\cup W)}$
shows that
$E'' = \Cn{\{\pi|\ndefr{\alpha}{\pi}\in A\}\cup\{p\in E | \ndefr{\alpha}{p}\in D, p\mbox{ is atomic} \}\cup W}$
is an extension of $\langle\GD{E}{\Delta}\cap D',W\rangle$
and $A\subseteq\GD{E''}{\langle\GD{E}{\Delta}\cap D',W\rangle}$.
By Theorem 3.2 in \cite{Reiter80},
there is an extension $E'$ of $\Delta'$ such that $A\subseteq\GD{E'}{\Delta'}$.

Therefore the procedure returns {\em true} if and only if there is
an extension $E$ of $\langle D,W\rangle$ such that $A\subseteq\GD{E}{\Delta}$.
\end{proof}

The tractability result is related to the tractability of brave reasoning
of the same class as shown by Lemma 6.4 in \cite{Kautz91}.

\subsubsection{Results for Arbitrary Priorities}

The previous section restricts to the special case where priorities
are a strict total ordering on the defaults.
However, for instance in representing inheritance networks,
two defaults sometimes need to have an equal (or incomparable) priority.
Hence the possibility of tractable inference with less restricted
priorities is of interest.
The complexity results for unrestricted priorities are summarized
in Table \ref{ta:unrestrictedsummary}. Like in earlier sections,
references to theorems are given in Table \ref{ta:unrestrictedsummaryrefs}.
The results in the previous sections as well as results on
the complexity of cautious reasoning \cite{Kautz91} directly imply
the intractability of many classes of reasoning with arbitrary priorities,
because the former two are a special case of the latter.
Classes of default theories for which the tractability question remains
open are the prerequisite-free normal classes and the normal unary class
with literals.
For prerequisite-free normal unary theories with 1-literal clauses
reasoning is tractable, but the remaining classes are sufficiently
expressive to encode propositional satisfiability.
It turns out that the tractability of lexicographic prioritized default logic
coincides with the tractability of Reiter's default logic
for all but one class.
There may still be differences in the complexity of the intractable classes,
for example Reiter's default logic could be in co-NP and lexicographic
prioritized default logic could be $\Delta^p_2$-hard.
We have not analyzed the intractable classes in more detail.

% SUMMARY OF COMPLEXITY RESULTS FOR UNRESTRICTED PRIORITIES
\begin{table}
\begin{tabular}{rl|lll}
& class of default theories & \multicolumn{3}{l}{complexity when clauses in W are} \\
& & Horn & 2-literal & 1-literal \\ \hline

1 &
disjunction-free &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

2 &
unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{q \conj\neg r}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

3 &
disjunction-free ordered &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

4 &
ordered unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{q\conj\neg r}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

5 &
disjunction-free normal &
%$\odefr{a_1\conj\cdots\conj a_l}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

6 &
Horn &
%$\odefr{p_1\conj\cdots\conj p_n}{q}{q}$
%$\odefr{p_1\conj\cdots\conj p_n}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

7 &
normal unary &
%$\odefr{p}{q}{q}$
%$\odefr{p}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \dlecoNPH \\

8 &
prerequisite-free &
%$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

9 &
prerequisite-free ordered &
%$\odefr{}{b_1\conj\cdots\conj b_n\conj c_1\conj\cdots\conj c_m}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

10 &
prerequisite-free unary &
%$\odefr{}{q}{q}$
%$\odefr{}{q\conj\neg r}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH \\

11 &
prerequisite-free ordered unary &
%$\odefr{}{q}{q}$
%$\odefr{}{q\conj\neg r}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \coNPH  \\

12 &
prerequisite-free normal &
%$\odefr{}{b_1\conj\cdots\conj b_n}{b_1\conj\cdots\conj b_n}$ &
\coNPH & \coNPH & \coNPH \\

13 &
prerequisite-free normal unary &
%$\odefr{}{q}{q}$
%$\odefr{}{\neg q}{\neg q}$ &
\coNPH & \coNPH & \PTIME \\

14 &
prerequisite-free positive normal unary &
%$\odefr{}{q}{q}$ &
\coNPH & \coNPH & \PTIME \\
\end{tabular}
\vskip5mm
\caption{Complexity of the consequence relation $\models^L$ with arbitrary priorities}\label{ta:unrestrictedsummary}
\end{table}

\begin{table}
\begin{tabular}{rl|lll}
& class of default theories & \multicolumn{3}{l}{reference}  \\
& & Horn & 2-literal & 1-literal \\ \hline
1 & disjunction-free & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
2 & unary & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
3 & disjunction-free ordered & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
4 & ordered unary & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
5 & disjunction-free normal & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
6 & Horn & \ksDLNPC & \ksDLNPC & \ksDLNPC \\
7 & normal unary & $14\subseteq$ & $14\subseteq$ & T\ref{th:unarysponphard} \\
8 & \prerequisitefree & $14\subseteq$ & $14\subseteq$ & $11\subseteq$ \\
9 & \prerequisitefree ordered & $14\subseteq$ & $14\subseteq$ & $11\subseteq$ \\
10 & \prerequisitefree unary & $14\subseteq$ & $14\subseteq$ & $11\subseteq$ \\
11 & \prerequisitefree ordered unary & $14\subseteq$ & $14\subseteq$ & T\ref{th:sn} \\
12 & \prerequisitefree normal & $14\subseteq$ & $14\subseteq$ & T\ref{th:pf2t} \\
13 & \prerequisitefree normal unary & $14\subseteq$ & $14\subseteq$ & T\ref{th:pfnuptime} \\
14 & \prerequisitefree positive normal unary & T\ref{th:pfpnu2h} & T\ref{th:pfpnu2h} & $\subseteq$ 13
\end{tabular}
\vskip5mm
\caption{References to theorems on the complexity of $\models^L$ with arbitrary priorities}\label{ta:unrestrictedsummaryrefs}
\end{table}

\begin{theorem}\label{th:pfnuptime}
Let ${\cal C}$ be the class of default theories $\Delta = \langle D,W\rangle$
where $W$ is a set of literals and $D$ consists of defaults of
the form $\pfdefr{l}$ where $l$ is a literal.
Let ${\cal P}$ be a strict partial order on $D$ and let $l$ be a literal.
Testing $\Delta\models^L_{\cal P}l$ can be done in polynomial time
on the size of $\Delta$ and ${\cal P}$ and $l$.
\end{theorem}

\begin{proof}
The algorithm in Figure \ref{fi:pfnualgorithm} tests $\langle D,W\rangle\models^L_{\cal P}l$.
The correctness of the algorithm is as follows. We analyze
the {\em if}-statements in sequence. In each case we may use the negations
of the assumptions of the previous cases.
For the first four statements the proof is like the proof of
Theorem \ref{th:semicpfnu} as no priorities are involved.
5. Assume that $\pfdefr{l}{\cal P}\pfdefr{\compl{l}}$.
Now $\pfdefr{l}{\cal T}\pfdefr{\compl{l}}$ for all strict total orders ${\cal T}$ such that ${\cal P}\subseteq{\cal T}$.
We obtain the unique extension with the $\Delta,{\cal P}$-ordering ${\cal T}$
by the algorithm given in Figure \ref{fi:prfreenormal} and proven correct
in Theorem \ref{th:totalpfreenormal}.
Obviously, $l$ is in that extension, and consequently
in all ${\cal P}$-preferred$^L$ extensions.
Hence it is correct to return {\em true}.
6. In the remaining case not $\pfdefr{l}{\cal P}\pfdefr{\compl{l}}$.
Hence there is a strict total ordering on $D$
such that ${\cal P}\subseteq{\cal T}$ and $\pfdefr{\compl{l}}{\cal T}\pfdefr{l}$.
An argument similar to the one in the previous case shows that there is
a ${\cal P}$-preferred$^L$ extension with the $\Delta,{\cal P}$-ordering
${\cal T}$ that contains $\compl{l}$ and therefore does not contain $l$.
Hence it is correct to return {\em false}.

Therefore the algorithm returns true if and only if $l$ is in
all ${\cal P}$-preferred$^L$ extensions of $\Delta$.
Clearly, the algorithm runs in polynomial time.
\end{proof}

Without priorities, cautious and brave reasoning for normal unary theories
and 1-literal clauses is tractable \cite{Kautz91}.
We show that priorities increase the expressivity sufficiently
to make this class intractable.

\begin{theorem}\label{th:unarysponphard}
The problem of testing whether a literal $l$ belongs to all
${\cal P}$-preferred$^L$ extensions of $\Delta$, where $\Delta$ is
a normal unary default theory and ${\cal P}$ is a strict partial order
on defaults in $\Delta$, is co-NP-hard.
\end{theorem}

\begin{proof}
The proof is by reduction from propositional satisfiability to the complement of the problem.
Let $C = \{ c_1,\ldots,c_m\}$ be a set of propositional clauses and $P$
the set of propositional variables occurring in $C$.
Let $N$ be an injective function that maps each clause $c\in C$ to
a propositional variable $n = N(c)$ such that $n\not\in P$.
Define the default theory $\Delta = \langle D,\emptyset\rangle$ and
priorities on $D$ as in the proof of Theorem \ref{th:semnucoNPC}.
We claim that the set of clauses $C$ is satisfiable if and only if
$\Delta\not\models^L_{\cal P}\ms{false}$; that is,
there is a ${\cal P}$-preferred$^L$ extension of $\Delta$
that does not contain {\em false}.
In the proof we refer to the consistency of extensions of $\langle D,W\rangle$
which is by the consistency of $W$ and the fact that defaults in $D$
have justifications (Corollary 2.2 by Reiter \citeyear{Reiter80}).

($\Rightarrow$)
Assume that there is a model $M$ such that $M\models C$.
We show that there is a ${\cal P}$-preferred$^L$ extension $E$ of 
$\Delta$ such that $\ms{false}\not\in E$.
Let $E = \Cn{\{ p\in P | M\models p \}\cup\{p'|p\in P, M\not\models p\}
\cup \{ \neg p | p\in P, M\not\models p \}\cup\{\neg p'|p\in P, M\models p\}
\cup \{ n | c\in C, n = N(c)\}
\cup\{\neg n'|c\in C, n = N(c)\}}$.
It is straightforward to verify that $E$ is an extension of $\langle D,\emptyset\rangle$.
Let ${\cal T}$ be any strict total order on $D$ such that
${\cal P}\subseteq{\cal T}$ and
for all $\{\delta,\delta'\}\subseteq D_1$
and all $\{\delta,\delta'\}\subseteq D_3$,
$\delta{\cal T}\delta'$ if $\applied{\delta}{E}$ and not $\applied{\delta'}{E}$.
We show that ${\cal T}$ is a $\langle D,\emptyset\rangle,{\cal P}$-ordering for $E$.
Let $E'$ be any extension of $\langle D,\emptyset\rangle$ such that
there is $\delta\in D$ such that $\appliet{\delta}{E'}{E}$.
We show that there is $\delta'\in D$ such that
$\appliet{\delta'}{E}{E'}$.

Assume that $\delta\in D_1$.
Now $\delta = \pfdefr{l}$ for some literal $l$
and $l\in E'$ and $\compl{l}\in E$.
Because $E'$ is consistent, $\compl{l}\not\in E'$.
Hence $\appliet{\pfdefr{\compl{l}}}{E}{E'}$.
By definition $\pfdefr{\compl{l}}{\cal T}\pfdefr{l}$.

Assume that $\delta\in D_2$ and $\delta = \pfdefr{p'}$ for some $p\in P$.
Now by definition $p\in E$ and $\applied{\ndefr{p}{\neg p'}}{E}$.
Because $E'$ is consistent, $\neg p'\not\in E'$ and hence
$\appliet{\ndefr{p}{\neg p'}}{E}{E'}$.
By definition $\ndefr{p}{\neg p'}{\cal P}\pfdefr{p'}$.

Assume that $\delta\in D_2$ and $\delta = \ndefr{p}{\neg p'}$ for some $p\in P$.
Because $p\in E'$, $\applied{\pfdefr{p}}{E'}$.
Because not $\applied{\ndefr{p}{\neg p'}}{E}$
by definition $p\not\in E$, and hence not $\applied{\pfdefr{p}}{E}$.
Hence $\neg p\in E$ and $\applied{\pfdefr{\neg p}}{E}$.
Because $E$ is consistent, $\neg p\not\in E$ and $\appliet{\pfdefr{\neg p}}{E}{E'}$.
By definition $\pfdefr{\neg p}{\cal P}\ndefr{p}{\neg p'}$.

Assume that $\delta = \ndefr{p}{n}$.
Clearly $p\not\in E$, $\appliet{\pfdefr{\neg p}}{E}{E'}$ and
$\pfdefr{\neg p}{\cal T}\ndefr{p}{n}$.
Proof for $\delta = \ndefr{p'}{n}$ is similar.

Assume that $\delta = \pfdefr{n'}$.
Hence $\appliet{\ndefr{n}{\neg n'}}{E}{E'}$.
By definition $\ndefr{n}{\neg n'}{\cal T}\pfdefr{n'}$.
Proof for $\delta = \ndefr{n}{\neg n'}$ is similar.

Assume that $\delta = \ndefr{n'}{\ms{false}}$.
Hence $\appliet{\pfdefr{n'}}{E'}{E}$ and $\appliet{\pfdefr{\neg n'}}{E}{E'}$.
By definition $\pfdefr{\neg n'}{\cal T}\ndefr{n}{\ms{false}}$.

This exhausts all $\delta\in D$.
Therefore ${\cal T}$ is a $\langle D,\emptyset\rangle,{\cal P}$-ordering
for $E$ and $E$ is a ${\cal P}$-preferred$^L$ extension
of $\langle D,\emptyset\rangle$.

($\Leftarrow$)
Assume that $E$ is a ${\cal P}$-preferred$^L$ extension of $\Delta$
such that $\ms{false}\not\in E$.
We show that there is a model $M$ such that $M\models C$.
Define the model as
$M\models p$ iff $p\in E$, for all $p\in P$.
Let $c = \{ l_1,\ldots,l_n\}$ be any clause in $C$.
We show that $M\models c$. Let $n = N(c)$.
Because $\ms{false}\not\in E$,
not $\applied{\ndefr{n'}{\ms{false}}}{E}$.
Because $\neg\ms{false}$ is not in any conclusion of a default
in $D$, $n'\not\in E$.
Because not $\applied{\pfdefr{n'}}{E}$, $\neg n'\in E$.
Hence $\applied{\ndefr{n}{\neg n'}}{E}$.
Hence $n\in E$.
Because $E$ is consistent,
$\applied{\ndefr{q}{n}}{E}$ for some $q\in\{p,p'\}$
where $p\in c$ or $\neg p\in c$.
If $q = p$, then $p'\not\in E$ because of the following.
Assume that $p'\in E$.
Let $E_{12} = \Cn{E\cap(P\cup\{\neg p|p\in P\}\cup\{p'|p\in P\}\cup\{\neg p'|p\in P\})\setd \{p'\}\cup\{\neg p'\}}$.
It is easy to show that $E_{12}$ is an extension of $\langle D_1\cup D_2,\emptyset\rangle$.
By Theorem 3.2 in \cite{Reiter80} there is an extension $E'$
of $\langle D,\emptyset\rangle$ such that
$\GD{E_{12}}{\langle D_1\cup D_2,\emptyset\rangle}\subseteq\GD{E'}{\langle D,\emptyset\rangle}$.
Now $\appliet{\ndefr{p}{\neg p'}}{E'}{E}$ and there is no 
$\delta\in D$ such that $\appliet{\delta}{E}{E'}$
and $\delta{\cal T}\ndefr{p}{\neg p'}$ for some strict total order
${\cal T}$ such that ${\cal P}\subseteq{\cal T}$.
This contradicts the ${\cal P}$-preferredness$^L$ of $E$, and hence
it must be the case that $p'\not\in E$.
Hence by definition $M\models p$.
If $q = p'$, then clearly $p'\in E$.
Hence by definition $M\models\neg p$.
Therefore $M\models c$.
Because this holds for any clause $c\in C$, $M\models C$.
\end{proof}


\section{Related Work on Prioritized Default Reasoning}\label{se:related}

Marek and Truszczy\'nski \citeyear{MT93} introduce a prioritized default logic
that is similar to Brewka's \citeyear{Brewka94:jelia} logic.
The existence of preferred extensions
is not guaranteed in general, but for normal defaults it is.
We believe that for normal default theories, the complexity of
the Marek and Truszczy\'nski logic coincides with the complexity
of Brewka's logic.
Delgrande and Schaub \citeyear{DS97} present a translation
from prioritized default theories to unprioritized default theories,
so that the extensions of the resulting theories obey the priorities.
Their translation can be performed in polynomial time.
Buccafurri et al. \citeyear{BLR98} present a knowledge representation language
that extends logic programs with priorities, classical negation, and
disjunction.
They claim that brave reasoning for their language is in general
$\Sigma^p_2$-complete and without disjunction and classical negation
it is polynomial time.

Brewka and Eiter \citeyear{BE98} present the notion of
{\em preferred answer sets} for extended logic programs.
Their definition diverges from earlier work in that even with
a total ordering on the rules there may be more than one preferred answer set,
and preferred answer sets do not always exists for a given program
even if answer sets do.
Brewka and Eiter show that testing the membership of a literal in all
preferred answer sets of a program is co-NP-hard when
the rules are totally ordered.
Their motivation for introducing preferred answer sets is that
earlier accounts of priorities in logic programs and in default logic do not
fulfill two principles identified by them.
Principle I is violated by the prioritized default logics that are based
on the semiconstructive definition of extensions
\cite{BH95:jar,Brewka94:jelia,MT93}, but not by the lexicographic prioritized
default logic discussed in Section \ref{se:lexcomplexity}.
Principle II can be paraphrased as follows.
Let $E$ be a ${\cal P}$-preferred extension of $\langle D,W\rangle$
and $\defr{\alpha}{\beta}{\gamma}$ a default such that $\alpha\not\in E$.
Then $E$ is a ${\cal P}'$-preferred extension of $\langle D\cup\{\defr{\alpha}{\beta}{\gamma}\},W\rangle$ for all ${\cal P}'$ such that
${\cal P}'\cap(D\times D) = {\cal P}$.
Brewka and Eiter show that the prioritized default logic investigated in
Section \ref{se:lexcomplexity} violates this principle.
However, Principle II is not violated by a closely related prioritized
default logic that replaces application with non-defeat \cite{Rintanen97:pdl}.
A default $\defr{\alpha}{\beta}{\gamma}$ is {\em defeated in} $E$
if $E\models\alpha\conj\neg\beta$.
Therefore it is not in general the case that lexicographic definitions of
preferredness would violate Principle II.
However, we believe that Brewka and Eiter would nevertheless
find this definition of preferred extensions counterintuitive.
\begin{example}
Let $D = \{\ndefr{a}{b}, \pfdefr{a}, \pfdefr{\neg a}\}$ and $W = \{\neg b\}$.
Let ${\cal T}$ be a strict total order on $D$ such that
$\ndefr{a}{b}{\cal T}\pfdefr{a}$ and $\pfdefr{a}{\cal T}\pfdefr{\neg a}$.
The default theory $\langle D,W\rangle$ has two extensions,
$E_1 = \Cn{\{a, \neg b\}}$ and $E_2 = \Cn{\{\neg a, \neg b\}}$.
The extension $E_1$ defeats $\ndefr{a}{b}$ and $\pfdefr{\neg a}$,
and $E_2$ defeats $\pfdefr{a}$.
Because $E_1$ defeats the highest priority default $\ndefr{a}{b}$
and $E_2$ does not, only $E_2$ is a ${\cal T}$-preferred extension
of $\langle D,W\rangle$.
\end{example}
We believe that in this example,
Brewka and Eiter would want $E_1$ to be the only ${\cal T}$-preferred extension
because the only conflict is between $\pfdefr{a}$ and $\pfdefr{\neg a}$,
and the priority of $\pfdefr{a}$ is higher.
It seems that the question at hand is the meaning of priorities in cases
where defaults that are less directly derivable have a higher or equal priority.
Lexicographic comparison gives one meaning, a very natural one in our
opinion, but Brewka and Eiter seem to want to ignore the higher priority.
Instead of addressing Brewka and Eiter's concern by devising new definitions
of preferred extensions, it could be addressed by not using priorities
that produce unintended results.
If a restriction to defaults with literal prerequisites and conclusions
is made, this could be done simply by requiring
that $\defr{l}{m}{n}{\cal P}\defr{l'}{m'}{n'}$ whenever $n = l'$.
Priorities used in translating inheritance networks to prioritized
default logic fulfill this requirement \cite{Rintanen97:pdl}.

\section{Conclusions}

We have presented a thorough analysis of the complexity of three versions
of prioritized default logic, giving results that place these logics
in the polynomial hierarchy, and analyzing the question of intractability
versus tractability for syntactically restricted classes of default theories.

The main results place the propositional variants of three general
formalizations of prioritized default reasoning,
the logics by Brewka \citeyear{Brewka94:jelia} and Baader and Hollunder
\citeyear{BH95:jar} that are based on the semiconstructive definition
of extensions, and a formalization that is based on lexicographic comparison,
on the lower levels of the polynomial hierarchy.
As the first two formalizations closely resemble each other,
it is not surprising that polynomial time translations between
the decision problems of these two formalizations exist.
There are also polynomial time translations to and from Reiter's default
logic.
The third formalization, that uses lexicographic comparison
to select the preferred extensions, is not reducible to Reiter's
default logic in polynomial time
(under the standard complexity-theoretic assumptions.)

An analysis of the complexity of the decision problems in syntactically
restricted cases, following earlier work by Kautz and Selman \citeyear{Kautz91}
and Stillman \citeyear{Stillman90}, identifies the effect of priorities on
the boundary between tractability and intractability in the prioritized
versions of the decision problems.
With priorities that totally order the defaults and classical propositional
reasoning that is tractable, for example with Horn clauses or 2-literal clauses,
reasoning in Brewka's and in Baader and Hollunder's logics is polynomial time.
For the formalization of prioritized default reasoning that uses lexicographic
comparison, the same assumptions yield tractable reasoning only for
the so-called Horn defaults and background theories without disjunction,
as well as normal defaults without prerequisites and disjunction.
When arbitrary priorities are allowed, in all three logics reasoning is
tractable only when defaults are of the form $\pfdefr{l}$
for literals $l$ and the background theories are sets of literals.

\subsection*{Acknowledgements}

This research was mainly carried out at the Helsinki University of Technology and finished at the University of Ulm while funded by the SFB 527 of the Deutsche Forschungsgemeinschaft. We gratefully acknowledge the generous support of the Finnish Cultural Foundation and the Finnish Academy of Science and Letters that helped completing this work.

We thank the four anonymous reviewers for pointing out some errors and
for advice on restructuring the article and on including references
to related work in Section \ref{se:related}.
Holger Pfeifer provided valuable assistance in proof-reading.

\bibliography{bib/abbreviations,bib/ael,bib/misc,bib/logics,bib/atp,bib/logicprogramming}

\end{document}
