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


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 thmcomplete and WIDTIO is thmcoNPcomplete (and thus in thm), there exists a polysize reduction from WIDTIO to circumscription satisfying theorem preservation. The converse does not hold: since circumscription is thmcomplete and WIDTIO is thmcoNP, unless the Polynomial Hierarchy does not collapse there is no theorempreserving polysize 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 alonecomputing the intersection of all elements of . 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 polynomialtime reductions among formalisms, the right one showing the existence of polysize 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 modelpreserving polysize reduction from circumscription to skeptical default reasoning [21], a theorempreserving polysize reduction exists, as shown by Theorem 14.