Applications

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 $\exists\forall$3QBF, that is, the problem of verifying whether a quantified Boolean formula $\exists X \forall Y. \neg F$ is valid, where $X$ and $Y$ are disjoint sets of variables, and $F$ is a set of clauses on the alphabet $X \cup Y$, each composed of three literals. As an example, a simple formula belonging to this class is: $\exists x_1,x_2 \forall y_1,y_2 ~~\neg ((x_1 \vee y_2) \wedge (\neg x_1 \vee \n... ... \wedge (\neg y_1 \vee \neg x_2 \vee \neg y_2) \wedge (\neg x_1 \vee \neg x_2))$.

The problem of deciding validity of a $\exists\forall$3QBF is complete for the class $\Sigma^p_2$. As a consequence, the corresponding problem $*\exists\forall$3QBF, that is deciding whether an input composed of any string ($*$) as the fixed part and a quantified Boolean formula $\exists X \forall Y. \neg F$ as the varying one, is complete for the class $\parallel\!\leadsto$$\Sigma^p_{2}$ [36]. Notice that in most of the hardness proofs we show in the sequel we use problems without any meaningful fixed part.