Stable Models

Stable models are one of the most popular semantics for non-stratified programs. The intuition behind the stable model semantics for a ground program P can be seen as follows. Each negative literal notL in P is treated as a special kind of atom called an assumption. To compute the stable model, a guess is made about whether each assumption is true or false, creating an assumption set, A. Once an assumption set is given, negative literals do not need to be evaluated as in the well-founded semantics; rather an evaluation treats a negative literal as an atom that succeeds or fails depending on whether it is true or false in A.

Example 5.3.1   Consider the simple, non-stratified program

there are two stable models of this program: in one writes_manual(terry) is true, and in another writes_manual(kostis) is true. In the Well-Founded model, neither of these literals is true. The residual program for the above program is

Computing stable models is an intractable problem, meaning that any algorithm to evaluate stable models may have to fall back on generating possible assumption sets, in pathological cases. For a ground program, if it is ensured that residual clauses are produced for all atoms, using the residual program may bring a performance gain since the search space of algorithms to compute stable models will be correspondingly reduced. In fact, by using XSB in conjunction with a Stable Model generator, Smodels [36], an efficient system has been devised for model checking of concurrent systems that is 10-20 times faster than competing systems [34].