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 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.