next up previous
Next: Stable Model Semantics Up: Space Efficiency of Propositional Previous: Comparing the Space Efficiency


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.



Subsections
next up previous
Next: Stable Model Semantics Up: Space Efficiency of Propositional Previous: Comparing the Space Efficiency
Paolo Liberatore
2000-07-28