(a) hhC1, pi, ∅i is a P-proof scheme of length 1 with conclusion p and empty support.

(b) hhC1, pi,hC2, qi, {r}i is a P-proof scheme of length 2 with conclusion q and support {r}.

(c) hhC1, pi,hC3, ri, {q}i is a P-proof scheme of length 2 with conclusion r and support {q}.

(d) hhC1, pi,hC2, qi,hC3, ri, {**q, r**}i is a P-proof scheme of length 3 with conclusion r and support {**q, r**}.

Proof scheme in (c) is an example of a proof scheme with unnecessary items (the first term). Proof scheme (d) is an example of a proof scheme which is not internally consistent in that r is in the support of its proof scheme and is also its conclusion. ✷
A P-proof scheme carries within itself its own applicability condition. In effect, a P-proof scheme is a *conditional* proof of its conclusion. It becomes applicable when all the constraints collected in the support are satisfied. Formally, for any set of atoms M, we say that a P-proof scheme S is M-*applicable* if M∩supp(S) = ∅.

We also say that M *admits* S if S is M-applicable.

The fundamental connection between proof schemes and stable models [MNR90a, MT93] is given by the following proposition.

Proposition 3.1 For every normal propositional program P and every set M of atoms, M is a stable model of P if and only if the following conditions hold.

(i) For every p ∈ M, there is a P-proof scheme S with conclusion p *such that* M *admits* S.

(ii) For every p /∈ M, there is no P-proof scheme S with conclusion p *such that* M *admits* S.

Proposition 3.1 says that the presence and absence of the atom p in a stable model depends *only* on the supports of proof schemes. This fact naturally leads to a characterization of stable models in terms of propositional satisfiability. Given p ∈ At, the *defining equation* for p w.r.t. P is the following propositional formula:

$$p\Leftrightarrow(\neg U_{1}\vee\neg U_{2}\vee\ldots)$$
p ⇔ (¬U1 ∨ ¬U2 ∨ **. . .**) (2)
where hU1, U2**, . . .**i is the list of all supports of P-proof schemes. Here for any finite set S = {s1**, . . . , s**n} of atoms, ¬S = ¬s1 **∧ · · · ∧ ¬**sn. If p is not the