Proof. **The proof is very similar to the proof for model checking of skeptical default logic.**
Indeed, both problems are k❀Σ
p 2 complete. Since the problem is in Σp 2
, as proved by Gottlob
(1992), it is also in k❀Σ
p 2
. Thus, what we have to prove is that is hard for that class.

We prove that the ∗∃∀**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 ∀X∃Y.¬F is valid if and only if Q **is derived by some extension of**
the default theory hD, Wi, where W and D **are defined as follows (Γ 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 Γ).

$$W=\emptyset$$ $$D=\bigcup_{c_{i}\in C}\left\{\frac{:c_{i}}{c_{i}},\frac{:\neg c_{i}}{\neg c_{i}}\right\}\cup\bigcup_{x_{i}\in X}\left\{\frac{:x_{i}}{x_{i}},\frac{:\neg x_{i}}{\neg x_{i}}\right\}\cup\left\{\frac{\neg(\bigwedge_{c_{i}\in C}c_{i}\to\gamma_{i}):}{w}\right\}$$ $$Q=\bigwedge_{\gamma_{i}\in F}c_{i}\wedge\bigwedge_{\gamma_{i}\notin F}\neg c_{i}\wedge w$$

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

$$\begin{array}{r l}{\neg}&{{}\bigwedge}\\ {}&{{}c_{i}{\mathrm{=true}}}\end{array}$$

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 ciis true if and only if γi ∈ F, and such that w **also holds. When**
the variables ci have the given value, the above formula is equivalent to ¬F**. As a result,**
such an extension exists if and only if there exists a truth evaluation of the variables X in which ¬F **is valid.**

## 6.4 Belief Revision

Many formalisms for belief revision have been proposed in the literature, here we focus on two of them: WIDTIO (When In Doubt Throw it Out) and SBR (Skeptical Belief Revision). Let K be a set of propositional formulae, representing an agent's **knowledge about the world.**
When a new formula A is added to K**, the problem of the possible inconsistency between** K and A arises. The first step is to define the set of sets of formulae W(K, A**) in the following** way:
W(K, A) = {K′ K′is a maximal consistent subset of K ∪ {A} **containing** A }