The following is immediate, see [Ap90] for unexplained notions.

Proposition 2.1 For every program P and every set M *of atoms the operator* TP,M
is monotone and continuous.

Thus the operator TP,M like all monotonic continuous operators, possesses a least fixed point FP,M.

Given program P and M ⊆ At, we define the *Gelfond-Lifschitz reduct* of P, PM,
as follows. For every clause C = p ← q1, . . . , qm,¬r1**, . . . ,**¬rn of P, execute the following operations.

(1) If some atom ri, 1 ≤ i ≤ n, belongs to M, then eliminate C altogether.

(2) In the remaining clauses that have not been eliminated by operation (1), eliminate all the negated atoms.

The resulting program PM is a Horn propositional program. The program PM possesses a least Herbrand model. If that least model of PM coincides with M, then M is called a *stable model* for P. This gives rise to an operator GLP which associates to each M ⊆ At, the least fixed point of TP,M. We will discuss the operator GLP and its proof-theoretic connections in section 4.2.

## 3 Proof Schemes And Reduced Defining Equations

In this section we recall the notion of a *proof scheme* as defined in [MNR90a, MT93] and introduce a related notion of *defining equations*.

Given a propositional logic program P, a proof scheme is defined by induction on its length. Specifically, a proof scheme w.r.t. P (in short P-proof scheme) is a sequence S = hhC1, p1i, . . . ,hCn, pni, Ui subject to the following conditions: (I) when n = 1, hhC1, p1i, Ui is a P-proof scheme if C1 ∈ P, p1 = **head**(C1), posBody(C1) = ∅, and U = **negBody**(C1) and
(II) when hhC1, p1i, . . . ,hCn, pni, Ui is a P-proof scheme, C = p ← posBody(C),¬**negBody**(C)is a clause in the program P, and **posBody**(C) ⊆
{p1**, . . . , p**n}, then hhC1, p1i, . . . ,hCn, pni,hC, pi, U ∪ **negBody**(C)i is a P-proof scheme.

When S = hhC1, p1i, . . . ,hCn, pni, Ui is a P-proof scheme, then we call (i) the integer n - the *length* of S, (ii) the set U - the *support* of S, and (iii) the atom pn
- the *conclusion* of S. We denote U by **supp**(S).

Example 3.1 Let P be a program consisting of four clauses: C1 = p ←, C2 =
q ← p,¬r, C3 = r ← ¬q, and C4 = s ← ¬t. Then we have the following examples of P-proof schemes: