Guarded resolution for Answer Set Programming

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 Gelfond-Lifschitz operator can be viewed as a proof-theoretic concept. As an application, we find a propositional theory EP whose models are precisely stable models of programs. We also find a class of propositional theories CP with the following properties. Propositional models of theories in CP are precisely stable models of P, and the theories in CT are of the size linear in the size of P .