Default Logic (and thus stable semantics of logic programs). Bonatti [Bo04] and separately Milnikel [Mi05] devised non-monotonic proof systems to study skeptical consequences of programs and default theories. Lifschitz [Li96] used prooftheoretic methods to approximate well-founded semantics of logic programs. Bondarenko et.al. [BTK93] studied an approach to stable semantics using methods with a clear proof-theoretic flavor. Marek, Nerode, and Remmel in a series of papers, [MNR90a, MNR90b, MNR91, MNR92, MNR94a, MNR94b], developed proof theoretic methods to study what they termed *non-monotonic rule systems* which have as special cases almost all ASP formalisms that have been seriously studied in the literature. Recently the area of proof systems for ASP (and more generally, nonmonotonic logics) received a lot of attention [GS07, JO07]. It is clear that the community feels that an additional research of this area is necessary.

Nevertheless, there is no clear classification of proof systems for nonmonotonic reasoning analogous to that present in classical logic, and SAT in particular.

In this paper, we define a notion of P-proof schemes, which is a kind of a proof system that was previously used by Marek, Nerode, and Remmel to study complexity issues for stable semantics of logic programs [MNR94a]. This proof system abstracts of M-proofs of [MT93] and produces Hilbert-style proofs. The nonmonotonic character of our P-proofs is provided by the presence of guards, called the support of the proof scheme, to insure context-dependence. A different but equivalent, presentation of proof schemes, using a guarded resolution is also possible
[MR09].

We shall show that we can use P-proof schemes to find a characterization of stable models via *reduced defining equations*. While in general these defining equations may be infinite, we study the case of programs for which all these equations are finite. This resulting class of programs, called FSP-programs, turn out to be characterized by a form of continuity of the Gelfond-Lifschitz operator.

## 1.1 Contributions Of The Paper

The contributions of this paper consist, primarily of investigations that elucidate the proof-theoretical character of the stable semantics for logic programs, an area with 20 years history [GL88]. The principal results of this paper are:
1. We show that the Gelfond-Lifschitz operator GLP is, in fact a proof-theoretical construct (Proposition 4.3)
2. As a result of the analysis of the Gelfond-Lifschitz operator we are able to show that the upper-half continuity of that operator is equivalent to finiteness of (propositional) formulas in a certain class associated with the program P
(Proposition 4.6)