Discussion

Tables 1 and 2 summarize the results on space efficiency of PKR formalisms and where they were proved (a dash `` -'' denotes a folklore result).

Table 1: Complexity of model checking and Space Efficiency of Model Representations

	Time Complexity	Space Efficiency
Propositional	P	model-P
Logic	-	-
WIDTIO	$\Sigma^p_2$-complete	model-P
	[37]	Th. 16
Skeptical	coNP-complete	model-coNP-complete
Belief Revision	[37]	Th. 17
Circumscription	coNP-complete	model-coNP-complete
	[4]	Th. 9
GCWA	coNP-hard,	model-P
	in $\Delta^p_2$[$\log n$]	Th. 10
	[14]
Skeptical	$\Sigma^p_2$-complete	model-$\Sigma^p_{2}$-complete
Default Reasoning	[38]	Th. 13
Credulous	N/A	N/A
Default Reasoning
Stable Model	P	model-P
Semantics	-	-

Table 2: Complexity of inference and Space Efficiency of Theorem Representations

	Time Complexity	Space Efficiency
Propositional	coNP-complete	thm-coNP-complete
Logic	[12]	[10]
WIDTIO	$\Pi^p_2$-complete	thm-coNP-complete
	[13] & [44]	Th. 18
Skeptical	$\Pi^p_2$-complete	thm-$\Pi^p_{2}$-complete
Belief Revision	[13]	Th. 19
Circumscription	$\Pi^p_2$-complete	thm-$\Pi^p_{2}$-complete
	[14]	Th. 11
GCWA	$\Pi^p_2$-complete	thm-coNP-complete
	[14] & [44]	Th. 12
Skeptical	$\Pi^p_2$-complete	thm-$\Pi^p_{2}$-complete
Default Reasoning	[22]	Th. 14
Credulous	$\Sigma^p_2$-complete	thm-$\Sigma^p_{2}$-complete
Default Reasoning	[22]	Th. 15
Stable Model	coNP-complete	thm-coNP-complete
Semantics	[40]	Th. 8

First of all, notice that space efficiency is not always related to time complexity. As an example, we compare in detail WIDTIO and circumscription. From the table it follows that model checking is harder for WIDTIO than for circumscription, and that inference has the same complexity in both cases. Nevertheless, since circumscription is thm-$\Sigma^p_{2}$-complete and WIDTIO is thm-coNP-complete (and thus in thm-$\Sigma^p_{2}$), there exists a poly-size reduction from WIDTIO to circumscription satisfying theorem preservation. The converse does not hold: since circumscription is thm-$\Sigma^p_{2}$-complete and WIDTIO is thm-coNP, unless the Polynomial Hierarchy does not collapse there is no theorem-preserving poly-size reduction from the former formalism to the latter. Hence, circumscription is a more compact formalism than WIDTIO to represent theorems. Analogous considerations can be done for models. Intuitively, this is due to the fact that for WIDTIO both model checking and inference require a lot of work on the revised knowledge base alone--computing the intersection of all elements of $W(K,A)$. Once this is done, one is left with model checking and inference in PL. Hence, WIDTIO has the same space efficiency as PL, which is below circumscription.

Figures 3 and 4 contain the same information of Tables 1 and 2, but highlight existing reductions. Each figure contains two diagrams, the left one showing the existence of polynomial-time reductions among formalisms, the right one showing the existence of poly-size reductions. An arrow from a formalism to another denotes that the former can be reduced to the latter one. We use a bidirectional arrow to denote arrows in both directions and a dashed box to enclose formalisms that can be reduced one into another. Note that some formalisms are more appropriate in representing sets of models, while others perform better on sets of formulae. An interesting relation exists between skeptical default reasoning and circumscription. While there is no model-preserving poly-size reduction from circumscription to skeptical default reasoning [21], a theorem-preserving poly-size reduction exists, as shown by Theorem 14.

Figure 3: Complexity of Model Checking vs. Space Efficiency of Model Representation

Figure 4: Complexity of Inference vs. Space Efficiency of Theorem Representation