
## 6. 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 (Reiter, 1980), and circumscription (McCarthy, 1980) 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 ∃X∀Y.¬F is valid, where X and Y **are disjoint sets of**
variables, and F is a set of clauses on the alphabet X ∪ Y **, each composed of three literals.**
As an example, a simple formula belonging to this class is: ∃x1, x2∀y1, y2 ¬((x1 ∨ y2) ∧
(¬x1 ∨ ¬x2 ∨ ¬y1) ∧ (¬y1 ∨ ¬x2 ∨ ¬y2) ∧ (¬x1 ∨ ¬x2)).

The problem of deciding validity of a ∃∀**3QBF is complete for the class Σ**p 2
. 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 ∃X∀Y.¬F **as the varying**
one, is complete for the class k❀Σ
p 2
(Liberatore, 1998). Notice that in most of the hardness proofs we show in the sequel we use problems without any meaningful fixed part.

## 6.1 Stable Model Semantics

Stable model semantics (SM**) was introduced by Gelfond and Lifschitz (1988) as a tool to**
provide a semantics for logic programs with negation. their **original proposal is now one** of the standard semantics for logic programs. We now recall the definition of propositional stable model.

Let P be a propositional, general logic program. Let M be a subset (i.e., an interpretation) of the atoms of P. Let P M be the program obtained from P **in the following way: if a**
clause C of P contains in its body a negated atom ¬A such that A ∈ M then C **is deleted;**
if a body of a clause contains a negated atom ¬A such that A 6∈ M then ¬A **is deleted from**
the body of the clause. If M is a least Herbrand model of P M then M **is a stable model of**
P.

For the formalism sm, we consider the program P **as the knowledge base. We write**
P |=sm Q to denote that query Q is implied by a logic program P **under Stable Model**
semantics.

In order to prove our result, we need to define the kernel of a graph.

Definition 12 (Kernel) Let G = (V, E) be a graph. A kernel of G is a set K ⊆ V **such**
that, denoting H = V − K**, it holds:**
1. H **is a vertex cover of** G
2. for all j ∈ H, there exists an i ∈ K such that (**i, j**) ∈ E.

We can now state the theorem on the compilability class of inference in the stable model semantics, and the corresponding theorem compactness class.

Theorem 8 The problem of inference for the Stable Model semantics is k❀coNP**-complete,**
thus Stable Model Semantics is thm-coNP**complete.**