Enhancing Global SLS-Resolution with Loop Cutting and Tabling Mechanisms

TL;DR

This paper introduces SLTNF-resolution, an improved procedural semantics for logic programming that enhances global SLS-resolution with loop cutting and tabling, effectively addressing infinite loops and redundancy.

Contribution

It develops SLTNF-resolution, combining loop cutting and tabling to improve efficiency and correctness over existing linear tabling semantics.

Findings

SLTNF-resolution is sound and complete for well-founded semantics.

It outperforms existing linear tabling semantics like SLT-resolution.

Addresses infinite loops and redundant computations effectively.

Abstract

Global SLS-resolution is a well-known procedural semantics for top-down computation of queries under the well-founded model. It inherits from SLDNF-resolution the {\em linearity} property of derivations, which makes it easy and efficient to implement using a simple stack-based memory structure. However, like SLDNF-resolution it suffers from the problem of infinite loops and redundant computations. To resolve this problem, in this paper we develop a new procedural semantics, called {\em SLTNF-resolution}, by enhancing Global SLS-resolution with loop cutting and tabling mechanisms. SLTNF-resolution is sound and complete w.r.t. the well-founded semantics for logic programs with the bounded-term-size property, and is superior to existing linear tabling procedural semantics such as SLT-resolution.