Journal of the Association for Computing Machinery, Vol. 43, No. 1, January 1996, pp. 20–74.

Tabled Evaluation with Delaying for General Logic Programs

WEIDONG CHEN

AND

DAVID S. WARREN

Abstract. SLD resolution with negation as finite failure (SLDNF) reflects the procedural interpretation of predicate calculus as a programming language and forms the computational basis for Prolog systems. Despite its advantages for stack-based memory management, SLDNF is often not appropriate for query evaluation for three reasons: (a) it may not terminate due to infinite positive recursion; (b) it may not terminate due to infinite recursion through negation; and (c) it may repeatedly evaluate the same literal in a rule body, leading to unacceptable performance.

We address all three problems for a goal-oriented query evaluation of general logic programs by presenting a tabled evaluation with delaying, called SLG resolution. It has three distinctive features:

1. SLG resolution is a partial deduction procedure, consisting of seven fundamental transformations. A query is transformed step by step into a set of answers. The use of transformations separates logical issues of query evaluation from procedural ones. SLG allows an arbitrary computation rule for selecting a literal from a rule body and an arbitrary control strategy for selecting transformations to apply.

2. SLG resolution is sound and search space complete with respect to the well-founded partial model for all non-floundering queries, and preserves all three-valued stable models. To evaluate a query under different three-valued stable models, SLG resolution can be enhanced by further processing of the answers of subgoals relevant to a query.

3. SLG resolution avoids both positive and negative loops and always terminates for programs with the bounded-term-size property. It has a polynomial time data complexity for well-founded negation of function-free programs. Through a delaying mechanism for handling ground negative literals involved in loops, SLG resolution avoids the repetition of any of its derivation steps.

Restricted forms of SLG resolution are identified for definite, locally stratified, and modularly stratified programs, shedding light on the role each transformation plays. SLG resolution makes many more rule specifications into effective programs. With simple (user or computer generated) annotations, both SLDNF resolution and SLG resolution can be used in a single application, allowing a smooth integration of Prolog computation and

Copyright 1996 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org. tabled evaluation of queries. Furthermore, Prolog compiler technology has been adapted for two efficient implementations of SLG resolution. For all these reasons, we believe that SLG resolution will provide the computational basis for the next generation of logic programming systems.

Categories and Subject Descriptors. F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—logic programming; proof theory; H.2.3 [Database Management]: Languages—query languages; H.2.4 [Database Management]: Systems— query processing; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving—logic programming; nonmonotonic reasoning and belief revision

General Terms. Query Evaluation, Deductive Databases, Logic Programming

Additional Key words and Phrases. Program transformations, stable models, tabled evaluation, well-founded models