
## 6.3 Default Logic

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

Theorem 13 **The problem of model checking for skeptical default logic is** k❀Σ
p 2 complete, thus skeptical default logic is **model-Σ**p 2 complete.

Proof. **The proof of membership is straightforward: since model checking for skeptical**
default logic is in Σp 2
(Liberatore & Schaerf, 1998), it follows that it is also in k❀Σ
p 2
.

The proof of k❀Σ
p 2
-hardness is similar to the proof of Σp 2
-hardness (Liberatore & Schaerf, 1998). The reduction is from the problem ∗∃∀3QBF. Let hα, βi be an instance of ∗∃∀**3QBF,**
where β = ∃X∀Y.¬F represents a valid ∃∀3QBF formula, and α **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 Γ = {γ1, . . . , γ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 ∃X∀Y.¬F is valid if and only if M is a model of some extension of h**W, D**i, where

$$W=\emptyset$$ $$D=\bigcup_{\gamma_{i}\in\Gamma}\left\{\frac{:c_{i}}{c_{i}},\frac{:-c_{i}}{-c_{i}}\right\}\cup\bigcup_{x_{i}\in X}\left\{\frac{:w\wedge(w\to x_{i})}{w\to x_{i}},\frac{:w\wedge(w\to-x_{i})}{w\to-x_{i}}\right\}\cup\left\{\frac{:w\wedge\bigwedge_{\gamma_{i}\in\Gamma}c_{i}\to\gamma_{i}}{w}\right\}$$ $$M=\left\{c_{i}\mid\gamma_{i}\in F\right\}$$

The set {ci| 1 ≤ i ≤ k} **is a set of new variables, one-to-one with the elements of Γ.**
Note that W and D only depends on the size n of F, while M depends on F**. As a result,**
this is a ≤nu−comp **reduction.**
We now prove that the formula is valid if and only if M **is a model of some extension**
of the default theory hW, Di**. This is similar to an already published proof (Liberatore &**
Schaerf, 1998). Consider an evaluation C1 of the variables {ci} and an evaluation X1 **of the**
variables X. Let D′ **be the following set of defaults.**

$$D^{\prime}=\bigcup_{c_{i}\in C_{1}}\left\{{\frac{:c_{i}}{c_{i}}}\right\}\bigcup_{c_{i}\not\in C_{1}}\left\{{\frac{:\neg c_{i}}{\neg c_{i}}}\right\}\cup\bigcup_{x_{i}\in X_{1}}\left\{{\frac{:w\wedge(w\to x_{i})}{w\to x_{i}}}\right\}\bigcup_{x_{i}\to\in X_{1}}\left\{{\frac{:w\wedge(w\to\neg x_{i})}{w\to\neg x_{i}}}\right\}$$

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

$$\begin{array}{r l}{c_{i}\in C_{1}}&{{}\mathrm{iff}\quad R\models c_{i}}\\ {c_{i}\not\in C_{1}}&{{}\mathrm{iff}\quad R\models\neg c_{i}}\\ {x_{i}\in X_{1}}&{{}\mathrm{iff}\quad R\models w\to x_{i}}\\ {x_{i}\not\in X_{1}}&{{}\mathrm{iff}\quad R\models w\to\neg x_{i}}\end{array}$$
