This section is devoted to the application of the theorems presented in the previous section. Using Theorems 4-7 and results previously known from the literature, we are able to asses model- and theorem-compactness of some PKR formalisms.
We assume that definitions of Propositional Logic, default logic [45], and circumscription [41] are known. Definitions of WIDTIO, SBR, GCWA, and stable model semantics are in the appropriate subsections.
In the following proofs we refer to the problem
3QBF,
that is, the problem of verifying whether a quantified Boolean formula
is valid, where 
and 
are
disjoint sets of variables, and 
is a set of clauses on the
alphabet 
, each composed of three literals. As an example, a
simple formula belonging to this class is:
.
The problem of deciding validity of a
3QBF is complete
for the class 
. As a consequence, the corresponding problem
3QBF, that is deciding whether an input composed of
any string (
) as the fixed part and a quantified Boolean formula
as the varying one, is complete for
the class
[36]. Notice that in most of the
hardness proofs we show in the sequel we use problems without any
meaningful fixed part.