We introduce two new compactness measures ( model and theorem compactness) and the corresponding classes ( model-C and thm-C, where C is a complexity class like P, NP, coNP, etc.). Such classes form two hierarchies that are isomorphic to the polynomial-time hierarchy [49]. We show that the relative space efficiency of a PKR formalism is directly related to such classes. In particular, the ability of a PKR formalism to compactly represent sets of models/theorems is directly related to the class of the model/theorem hierarchy it belongs to. Problems higher up in the model/theorem hierarchy can represent sets of models/theorems more compactly than formalisms that are in lower classes.
This classification is obtained through a general framework and not by making direct comparisons and specific translations between the various PKR formalisms. Furthermore, our approach also allows for a simple and intuitive notion of completeness for both model and theorem hierarchies. This notion precisely characterizes both the relation between formalisms at different levels, and the relations between formalisms at the same level. An interesting result is that two PKR formalisms in which model checking or inference belong to the same time complexity class may belong to different compactness classes. This may suggest a criterion for choosing between two PKR formalisms in which reasoning has the same time complexity--namely, choose the more compact one. Also, two PKR formalisms may belong to the same theorem compactness class, yet to different model compactness classes. This stresses the importance of clarifying whether one wants to represent models or theorems when choosing a PKR formalism.