Summary: We investigate a proof system based on a guarded resolution rule and show its adequacy for the stable semantics of normal logic programs. As a consequence, we show that the Gelfond-Lifschitz operator can be viewed as a proof-theoretic concept. As an application, we find a propositional theory \(E_{P}\) whose models are precisely stable models of programs. We also find a class of propositional theories \(\mathcal C_{P}\) with the following properties. Propositional models of theories in \(\mathcal C_{P}\) are precisely stable models of \(P\), and the theories in \(\mathcal C_{T}\) are of the size linear in the size of \(P\).