A Procedural Semantics for Well Founded Negation in Logic Programs

We introduce global SLS-resolution, a procedural semantics for well-founded negation as defined by Van Gelder, Ross and Schlipf. Global SLS-resolution extends Przymusinski 's SLS-resolution, and may be applied to all programs, whether locally stratified or not. 1 Global SLS-resolution is defined in terms of global trees, a new data structure representing the dependence of goals on derived negative subgoals. We prove that global SLS-resolution is sound with respect to the well-founded semantics, and complete for non-floundering queries. While not effective in general, global SLS-resolution is effective for classes of "acyclic" programs, and can be augmented with a memoing device to be effective for all function-free programs. This research was supported by the National Science Foundation under grant IRI-87-22886, by a grant from IBM Corporation, and by the United States Air Force Office of Scientific Research under contract AFOSR-88-0266. A preliminary version of this paper was presen..