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 . Notice that model-compactness is only applicable to skeptical default logic.
Proof. The proof of membership is straightforward: since model checking for skeptical default logic is in , it follows that it is also in .
The proof of -hardness is similar to the proof of -hardness . The reduction is from the problem 3QBF. Let be an instance of 3QBF, where represents a valid 3QBF formula, and is any string.
Let be the size of the formula . This implies that the variables in the formula are at most . Let be the set of all the clauses of three literals over this alphabet. The number of clauses of three literals over an alphabet of variables is less than , thus bounded by a polynomial in .
We prove that is valid if and only if is a model of some extension of , where
The set is a set of new variables, one-to-one with the elements of . Note that and only depends on the size of , while depends on . As a result, this is a reduction.
We now prove that the formula is valid if and only if is a model of some extension of the default theory . This is similar to an already published proof . Consider an evaluation of the variables and an evaluation of the variables . Let be the following set of defaults.
This set of defaults has been chosen so that the set of its consequences corresponds to the sets and . Namely, we have:
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:
Consistency of follows by construction: assigning to true for each , etc., we obtain a model of .
We have then to prove that no other default is applicable. If , the default is not applicable, and vice versa, if , then is not applicable. Moreover, none of the defaults , is applicable if , because in this case , thus would follow (while is a justification of the default). A similar statement holds for if .
As a result, the only applicable default may be the last one, (recall that F is negated). This default is applicable if and only if, for the given evaluation of the 's and '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 is not a model of the extension because is the consequence of the last default while . The converse also holds: if the last default is not applicable then is a model of the default theory.
As a result, the QBF is valid if and only if is a model of the given default theory.
Proof. Since inference in skeptical default logic is in , it is also in . -hardness comes from a simple reduction from circumscription. Indeed, the circumscription of a formula is equivalent to the conjunction of the extensions of the default theory , where :
As a result, if and only if is implied by under skeptical semantics. Since only depends on (and not on ) this is a reduction. Since inference for circumscription is -complete (see Theorem 11), it follows that skeptical default logic is -hard.
Proof. The proof is very similar to the proof for model checking of skeptical default logic. Indeed, both problems are complete. Since the problem is in , as proved by Gottlob , it is also in . 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 is valid if and only if is derived by some extension of the default theory , where and are defined as follows ( is the set of all the clauses of three literals over the alphabet of , and is a set of new variables, one-to-one with ).
Informally, the proof goes as follows: for each truth evaluation of the variables in and 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
is valid, then the last default is applicable, thus the extension also contains . The converse also holds: if the formula is not valid in the evaluation, then the variable is not in the extension.
As a result, there exists an extension in which holds if and only if there exists an extension in which each is true if and only if , and such that also holds. When the variables have the given value, the above formula is equivalent to . As a result, such an extension exists if and only if there exists a truth evaluation of the variables in which is valid.