A procedural semantics for well-founded negation in logic programs

AbstractWe 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. 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 nonfloundering queries. Although not effective in general, global SLS-resolution is effective for classes of “acrylic” programs and can be augmented with a memoing device to be effective for all function-free programs