Contributions to the stable model semantics of logic programs with negation

Understanding the stable model semantics is an important topic in Logic Programming and Non-Monotonic Reasoning. In fact, stable models are closely related to extensions in default logic, and to other non-monotonic formalisms like TMS and abduction. In this paper we propose two new explicit characterizations of the stable model semantics. First, we specify a simple requirement for checking stability of a minimal model. Second, we characterize stable models in terms of their ''difference'' with respect to the set of true atoms of the well-founded model of the program. This provides a method for: efficiently computing stable models whenever the Herbrand base is finite; in many cases when the Herbrand base is infinite, computing the basic sets of assumptions on which the stable models are based. The method may help ensure correctness of any procedural semantics based on stable models, like for instance abduction.