1. M is a model of P**, and**
2. There is a function rk : M → Ord such that, for every p ∈ M**, there is a**
clause C **such that**
(a) p = head(C),
(b) M |= body(C**), and**
(c) For all q ∈ posBody(C), rk (q) < rk(p).

Clearly, the least model of a Horn program has levels since the function which assigns to an atom p ∈ M, the least integer n **such that** p ∈ T
n P
(∅**) is the desired**
rank function for condition (2).

We now prove the following proposition.

## Proposition 3.1

Let P be a propositional logic program and M ⊆ At. Then M **is a stable model of**
P if and only if M **has levels with respect to** P. Proof: Clearly, when M is a stable model of P, then M **has levels with respect to** P. Namely, the rank function whose existence is postulated in (2) is the **rank function**
inherited from the Horn program PM .

Converse implication can be proved in a variety of ways. Our proof, in **the spirit**
of the proof-theoretic approach of this paper, uses guarded resolution. That is, assume that M has levels with respect to P where rk **is the rank function in**
condition (2). Our goal is to prove that M = GLP (M**). First, let us observe that**
since M |= P, GLP (M) ⊆ M. Thus, all we need to show is that M ⊆ GLP (M**). By**
Corollary 2.1, we need only show that for given any p ∈ M, there is a Z **such that** p : Z possesses a guarded resolution proof from g(P) that is admitted by M**. We** construct the desired set Z **and guarded resolution proof by using the rank function**
rk. Let S = {rk(p) : p ∈ M}, i.e. S **is the range of rank function. We proceed by**
transfinite induction on the elements of S. Let p be an atom in M **such that** rk(p)
is the least element of S. By assumption, there must exist a clause C in P **such**
that M |= body(C), p = head(C**) and for all** q ∈ posBody(C), rk(q) < rk(p**). Since**
M |= body(C), there can be no q's in positive part of the body of C **because any**
such q must be in M and have rank strictly less than p. Thus the clause C **has the** following form:

## P ← Not R1**, . . .** Not Rm.

As M |= body(C), r1, . . . , rm ∈/ M. But then p : {r1, . . . , rm} **is a guarded atom**
admitted by M and so p : {r1, . . . , rm} **has a guarded resolution proof from** g(P)
which consists of a single node labeled with p : {r1**, . . . , r**m}.

Now, assume that whenever β ∈ S, β < α, and rk(q) = β**, then there is a guarded**
resolution proof of q : S from g(P) admitted by M for some set S**. Let us assume**
that p ∈ M and rk (p) = α**. By our assumption, there is a clause** C
p ← q1**, . . . , q**n, not r1**, . . .** not rm with M |= body(C) and rk(q1) < rk(p), . . . , rk(qn) < rk(p). By inductive assumption, for every qi, 1 ≤ i ≤ n, there is a finite set of atoms Zi such that there is