Here |= is the propositional consequence relation. The effect of this observation is that not all the supports of proof schemes are important, only the inclusion-minimal ones.

Example 3.3 Let P be an infinite program consisting of clauses p ← ¬p1**, . . . ,**¬pi, for all i ∈ N. The defining equation for p in P is p ⇔ [¬p1 ∨ (¬p1 ∧ ¬p2) ∨ (¬p1 ∧ ¬p2 ∧ ¬p3) ∨ **. . .** ]
which is infinite. But our observation above implies that this formula is *equivalent* to the formula p ⇔ ¬p1
✷

Motivated by the Example 3.3, we define the *reduced defining equation* for p relative to P to be the formula

$$p\Leftrightarrow(\neg U_{1}\lor\neg U_{2}\lor\ldots)$$
p ⇔ (¬U1 ∨ ¬U2 ∨ **. . .**) (3)
where Ui range over *inclusion-minimal* supports of P-proof schemes for the atom p and U1 ≺ U2 **≺ · · ·** . Again, if p is not the conclusion of any proof scheme, then we set the defining equation of p to be p ⇔ ⊥. In the case, where there is a proof scheme of p with empty support, then we set the defining equation of p to be p ⇔ ⊤. We denote this formula as rEqP
p
, and define rΦP to be the theory consisting of rEqP
p for all p ∈ At. We then have the following strengthening of Proposition 3.2.

Proposition 3.3 Let P *be a normal propositional program. Then stable models of* P *are precisely the propositional models of the theory* rΦP .

In our example 3.3, the theory ΦP involved formulas with infinite disjunctions, but the theory rΦP contains only normal finite propositions.

Given a normal propositional program P, we say that P is a *finite support program* (FSP-program) if all the reduced defining equations for atoms with respect to P are finite propositional formulas. Equivalently, a program P is an FSP-program if for every atom p there is only finitely many inclusion-minimal supports of P-proof schemes for p.

## 4 Continuity Properties Of Operators And Proof Schemes

In this section we investigate continuity properties of operators and we will see that one of those properties characterizes the class of FSP programs.