atom p : Z is the conclusion of a guarded resolution proof P from g(P**) admitted** by M.

Proof: Let Q = PM and assume that p ∈ GLP (M**). Then by definition,** p ∈ T
ω Q
where TQ is the standard one-step provability operator for Q**. We claim that we**
can prove by induction on n ∈ N **that whenever** p ∈ T
n Q**, then there exists a set of**
atoms Z such that p : Z possesses a guarded resolution proof from g(P**) admitted** by M. If n = 1, then it must be the case that the p ← belongs to Q**. But then, for**
some r1**, . . . , r**m, p ← not r1**, . . . ,** not rm belongs to P and {r1, . . . , rm}∩M = ∅. Therefore the guarded atom p : {r1**, . . . , r**m}
is admitted by M and it possesses a guarded resolution proof from g(P**), namely,**
the one that consists of the root labeled by p : {r1, . . . , rm}**. Now, let us assume**
p ∈ T
n+1 Q . Then there is a clause C = p ← q1, . . . , qs in Q **such that** qi ∈ T
n Q
for i = 1, . . . , s. Thus by induction, there are sets of atoms Si, 1 ≤ i ≤ n**, such** that qi: Si possesses a guarded resolution proof from g(P) admitted by M**. As** p ← q1, . . . , qn belongs to Q, there must exist atoms r1, . . . , rm ∈/ M **such that**
p ← q1**, . . . , q**n, not r1**, . . . ,** not rm is a clause in P**. It is easy to combine the guarded resolution proofs of** qi: Si, 1 ≤ i ≤ n and the guarded clause p ← q1, . . . , qn : {r1, . . . , rm} **to obtain a guarded**
resolution proof from g(P**) of the following guarded atom:**
p : S1 ∪ . . . ∪ Sn ∪ {r1**, . . . , r**m}.

As all the sets occurring in the guard of this guarded atom are disjoint from M, the resulting guarded resolution proof is admitted by M**. This shows the inclusion** ⊆.

Conversely, suppose p : S has a guarded resolution proof P from g(P**) admitted**
by M. By the lemma, all the guards occurring in P are disjoint from M**. We can**
then prove by induction on the height of the tree P that p ∈ GLP (M**). If the height**
of P **is 0, then it must be the case that**
p ← not r1**, . . . ,** not rm belongs to P where S = {r1, . . . , rm}. But since M ∩S = ∅, the clause p ← **belongs**
to Q**. Hence** p ∈ GLP (M).

Now, for the inductive step, assume that whenever q : S **has a guarded resolution**
proof from g(P) that is admitted by M of height less than or equal to n**, then**
q ∈ GLP (M**). We now show that the same property holds for all guarded atoms**
p : U which have a guarded resolution proof from G(P**) that is admitted by** M of the height n **+ 1. What does such a guarded resolution proof look like? First the** root must be the result of a guarded unit resolution of the form p ← q : Z1 q : S0 p : Z1 ∪ S0.