Define the reduction f as f(KB) = f1(KB, f3(KB)), where f3 **is the poly-size function**
that computes the size of its input. Since poly-size functions are closed under composition, f **is poly-size.**
Now, we show that f is a theorem-preserving reduction, i.e.,f **satisfies Def. 9. This**
amounts to proving that for each knowledge base KB in F1 **there exists a circuit** gKB,
whose size is poynomial wrt KB, such that for every formula ϕ **on the variables of** KB it holds that KB ⊢F1 ϕ iff f(KB) ⊢F2 gKB(ϕ).

We proceed as in the proof of Theorem 4: Given a KB in F1, let z = f2(KB, f3(KB)).

Since f2 and f3 are poly-size, z has polynomial size with respect to |KB|. Define gKB(ϕ) = g(z, ϕ) = g(f2(KB, f3(KB)), ϕ). Clearly, gKB **can be represented by a circuit of polynomial**
size wrt KB. From this construction, KB ⊢F1 ϕ iff f(KB) ⊢F2 gKB(ϕ**). Hence, the claim**
follows.

Theorem 7 Let F1 and F2 **be two PKR formalisms. If the polynomial hierarchy does not**
collapse, F1 is thm-C1-hard, F2 is in thm-C2, and C2 ⊂ C1**, then there is no poly-size**
reduction f : F1 7→ F2 **satisfying theorem preservation.**
Proof. We show that if such a reduction exists, then C1/poly ⊆ C2**/poly and the polynomial**
hierarchy collapses at some level (Yap, 1983). Let A **be a complete problem for class C**1.

Define the problem ǫA as in the proof of Theorem 5: this problem is k❀C1**-complete (Cadoli**
et al., 1996b, Thm. 6). Since inference in F1 is thm-C1-hard, ǫA is non-uniformly compreducible to inference in F1**. That is, (adapting Def. 6) there exist two poly-size binary**
functions f1 and f2, and a polynomial-time binary function g such that for every pair h**ǫ, y**i, hǫ, yi ∈ ǫA **if and only if** f1(ǫ, |y|) ⊢F1 g(f2(ǫ, |y|), y). Let |y| = n**. Clearly, the knowledge**
base f1(ǫ, |y|) depends just on n**, i.e., there is one knowledge base for each integer. Call**
it KBn. Moreover, also f2(ǫ, |y|) = f2(ǫ, n) depends just on n: call it On **(for Oracle).**
Observe that both KBn and On **have polynomial size with respect to** n.

If there exists a poly-size reduction f : F1 7→ F2 **satisfying theorem preservation, then**
given the knowledge base KBn there exists a poly-time function hn **such that** KBn ⊢F1 g(On, y) if and only if f(KBn) ⊢F2 hn(g(On, y)).

Therefore, the k❀C1-complete problem ǫA **can be non-uniformly reduced to a problem in**
k❀C2 as follows: Given y, from its size |y| = n **one obtains (with an arbitrary preprocessing)**
f(KBn) and On. Then one checks whether the formula hn(g(On, y)) (computable in polytime given y and On) is a theorem in F2 of f(KBn**). From the fact that inference in** F2 is in k❀C2, we have that k❀C1 ⊆ k❀C2. It follows that C1/poly ⊆ C2**/poly (Cadoli et al.,**
1996b, Thm. 9), which implies that the polynomial hierarchy **collapses (Yap, 1983).**
Theorems 4-7 show that compilability classes characterize **very precisely the relative**
capability of PKR formalisms to represent sets of models or sets of theorems. For example, as a consequence of Theorems 3 and 7 there is no poly-size reduction from PL to the syntactic restriction of PL allowing only Horn clauses that **preserves the theorems, unless** the polynomial hierarchy collapses. Kautz and Selman (1992) proved non-existence of such a reduction for a problem strictly related to pli **using a specific proof.**