Default Logic

In this subsection we present the results for default logic, in its two variants (credulous and skeptical). For more details on these two main variants of default logic, we refer the reader to the paper by Kautz and Selman [29]. Notice that model-compactness is only applicable to skeptical default logic.

Theorem 13   The problem of model checking for skeptical default logic is $\parallel\!\leadsto$$\Sigma^p_{2}$ complete, thus skeptical default logic is model-$\Sigma^p_{2}$ complete.

Proof. The proof of membership is straightforward: since model checking for skeptical default logic is in $\Sigma^p_2$ [38], it follows that it is also in $\parallel\!\leadsto$$\Sigma^p_{2}$.

The proof of $\parallel\!\leadsto$$\Sigma^p_{2}$-hardness is similar to the proof of $\Sigma^p_2$-hardness [38]. The reduction is from the problem $*\exists\forall$3QBF. Let $\langle \alpha,\beta \rangle$ be an instance of $*\exists\forall$3QBF, where $\beta = \exists X \forall Y . \neg F$ represents a valid $\exists\forall$3QBF formula, and $\alpha$ is any string.

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

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

$$\begin{eqnarray*} W &=& \emptyset \\ D &=& \bigcup_{\gamma_i\in\Gamma} \left\{ ... ...\gamma_i}{w} \right\} \\ M &=& \{ c_i ~\vert~ \gamma_i \in F \} \end{eqnarray*}$$

The set $\{ c_i ~\vert~ 1 \leq i \leq k \}$ is a set of new variables, one-to-one with the elements of $\Gamma$. Note that $W$ and $D$ only depends on the size $n$ of $F$, while $M$ depends on $F$. As a result, this is a $\leq_{nu-comp}$ reduction.

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

$$D' = \bigcup_{c_i \in C_1} \left\{ \frac{~:c_i}{c_i} \right\... ...ge (w \rightarrow \neg x_i)}{w \rightarrow \neg x_i} \right\}$$

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

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

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

1. the set of consequences of $D'$ is consistent; and

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

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

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

As a result, the only applicable default may be the last one, $\frac{:w \wedge \bigwedge_{\gamma_i\in\Gamma} c_i \rightarrow \gamma_i}{w}$ (recall that F is negated). This default is applicable if and only if, for the given evaluation of the $c_i$'s and $x_i$'s, the set of clauses is satisfiable. This amount to say: ``there is an extension in which the last default is not applicable if and only if the QBF formula is valid''. Now, if the last default is applicable, then $M$ is not a model of the extension because $w$ is the consequence of the last default while $w \not\models M$. The converse also holds: if the last default is not applicable then $M$ is a model of the default theory.

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

Theorem 14   The inference problem for skeptical default logic is $\parallel\!\leadsto$$\Pi^p_{2}$ complete, thus skeptical default logic is thm-$\Pi^p_{2}$ complete.

Proof. Since inference in skeptical default logic is in $\Pi^p_2$, it is also in $\parallel\!\leadsto$$\Pi^p_{2}$. $\parallel\!\leadsto$$\Pi^p_{2}$-hardness comes from a simple reduction from circumscription. Indeed, the circumscription of a formula $T$ is equivalent to the conjunction of the extensions of the default theory $\langle T,D \rangle$, where [15]:

$$D = \bigcup \left\{ \frac{~:\neg x_i}{\neg x_i} \right\}$$

As a result, $CI\!RC(T) \models Q$ if and only if $Q$ is implied by $\langle T,D \rangle$ under skeptical semantics. Since $\langle T,D \rangle$ only depends on $T$ (and not on $Q$) this is a $\leq_{nu-comp}$ reduction. Since inference for circumscription is $\parallel\!\leadsto$$\Pi^p_{2}$-complete (see Theorem 11), it follows that skeptical default logic is $\parallel\!\leadsto$$\Pi^p_{2}$-hard. 

Theorem 15   The inference problem for credulous default logic is $\parallel\!\leadsto$$\Sigma^p_{2}$ complete, thus credulous default logic is thm-$\Sigma^p_{2}$ complete.

Proof. The proof is very similar to the proof for model checking of skeptical default logic. Indeed, both problems are $\parallel\!\leadsto$$\Sigma^p_{2}$ complete. Since the problem is in $\Sigma^p_2$, as proved by Gottlob [22], it is also in $\parallel\!\leadsto$$\Sigma^p_{2}$. Thus, what we have to prove is that is hard for that class.

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

Namely, a formula $\forall X \exists Y . \neg F$ is valid if and only if $Q$ is derived by some extension of the default theory $\langle D, W \rangle$, where $W$ and $D$ are defined as follows ($\Gamma$ is the set of all the clauses of three literals over the alphabet of $F$, and $C$ is a set of new variables, one-to-one with $\Gamma$).

$$\begin{eqnarray*} W &=& \emptyset \\ D &=& \bigcup_{c_i \in C} \left\{ \frac{~... ...n F} c_i \wedge \bigwedge_{\gamma_i \not\in F} \neg c_i \wedge w \end{eqnarray*}$$

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

$$\neg \bigwedge_{c_i={\rm true}} \gamma_i$$

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

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