A simple proof-theoretic characterization of Stable Models

Stable models of logic programs have been studied and characterized also in comparison with other formalisms by many researchers. As already argued, such characterizations are interesting for many reasons, including the possibility of leading to new algorithms for computing stable models. In this paper we provide a simple characterization of stable models which can be seen as the proof-theoretic counterpart of the standard model-theoretic definition. We show how it can be naturally encoded in difference logic. Our encoding, compared to the existing reductions to classical logics, does not explicitly rely on a previous computation of Clark's completion, and it does not involve any Boolean variable.