Journal of the ACM Bibliography

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 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.

The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.

Preliminary version

A preliminary version of these results was presented in: Weidong Chen and David Scott Warren. Query evaluation under the well founded semantics. In Proceedings of the Twelfth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 168-179, Washington, D.C., 25-28 May 1993.

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

Selected references

• Krzysztof R. Apt and M. H. Van Emden. Contributions to the theory of logic programming. Journal of the ACM, 29(3):841-862, July 1982.

• Isaac Balbin, Graeme S. Port, Kotagiri Ramamohanarao, and Krishnamurthy Meenakshi. Efficient bottom-UP computation of queries on stratified databases. Journal of Logic Programming, 11(3-4):295-344, October/November 1991.

• Weidong Chen, Terrance Swift, and David Scott Warren. Efficient top-down computation of queries under the well-founded semantics. Journal of Logic Programming, 24(3):161-199, September 1995.

• M. H. Van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733-742, October 1976.

• Allen Van Gelder, Kenneth A. Ross, and John S. Schlipf. The well-founded semantics for general logic programs. Journal of the ACM, 38(3):620-650, July 1991.

• John W. Lloyd and John C. Sheperdson. Partial evaluation in logic programming. Journal of Logic Programming, 11(3-4):217-242, October/November 1991.

• Wiktor Marek and Miroslaw Truszczynski. Autoepistemic logic. Journal of the ACM, 38(3):588-619, July 1991.

• Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258-282, April 1982.

• Raghu Ramakrishnan. Magic templates: A spellbinding approach to logic programs. Journal of Logic Programming, 11(3-4):189-216, October/November 1991.

• Peter J. Stuckey. Constructive negation for constraint logic programming. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 328-339, Amsterdam, The Netherlands, 15-18 July 1991. IEEE Computer Society Press.

• Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, pages 137-146, San Francisco, California, 5-7 May 1982.

• Laurent Vieille. Recursive query processing: The power of logic. Theoretical Computer Science, 69(1):1-53, 5 December 1989. Fundamental study.

Shortcuts: