A goal-oriented approach to computing the well-founded semantics

AbstractGlobal SLS resolution is an ideal procedural semantics for the well-founded semantics. We present a more effective variant of global SLS resolution, called XOLDTNF resolution, which incorporates simple mechanisms for loop detection and handling. Termination is guaranteed for all programs with the bounded-term-size property. We establish the soundness and (search space) completeness of XOLDTNF resolution. An implementation of XOLDTNF resolution in Prolog is available via FTP