An Abstract Machine for Computing the Well-Founded Semantics

Click on the title to obtain a gzip-ed PostScript version of the paper (82K).

Abstract:

The well-founded semantics has gained wide acceptance partly because it is a skeptical semantics. That is, the well-founded model posits as unknown atoms which are deemed true or false in other formalisms such as stable models. This skepticism makes the well-founded model not only useful in itself, but also suitable as a basis for other forms of non-monotonic reasoning. For instance, since algorithms to compute stable models are intractable, the atoms relevant to such algorithms can be limited to those undefined in the well-founded model.

This paper presents an implementation of the well-founded semantics in the SLG-WAM of XSB. To compute the well-founded semantics, the SLG-WAM adds three operations to its tabling engine --- negative loop detection, delay and simplification --- which serve to detect, to break and to resolve cycles through negation that may arise in evaluating normal programs. We describe fully the addition of these operations to our tabling engine, and demonstrate the efficiency of our implementation in two ways. First, we present a theorem that bounds the need for delay to those literals which are not dynamically stratified for a fixed-order computation. Secondly, we present performance results that indicate that the overhead of delay and simplification to Prolog --- or tabled --- evaluations is minimal.