%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "chenw96.ltx",
%%%     date      = "16 May 1996",
%%%     time      = "14:58:7 EDT",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "60494 135 713 5863",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 1995 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.
%%%
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{ChenW96}

\title{Tabled Evaluation with Delaying for General Logic Programs}

\author{Weidong Chen \and David~S. Warren}

\Pages{20--74}

\Month{January}

\Year{1996}

\Volume{43}

\Number{1}

\maketitle

\begin{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. \par We address all three
  problems for a goal-oriented query evaluation of general logic programs by
  presenting a tabled evaluation with delaying, called \emph{SLG resolution}.
  It has three distinctive features: \begin{enumerate} \item 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. \item 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. \item 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. \end{enumerate} 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.

\end{abstract}

\begin{categories}

F.4.1 [\textbf{Mathematical Logic and Formal Languages}]: Mathematical
Logic---\emph{logic programming}; \emph{proof theory}; H.2.3
[\textbf{Database Management}]: Languages---\emph{query languages};
H.2.4 [\textbf{Database Management}]: Systems---\emph{query
processing}; I.2.3 [\textbf{Artificial Intelligence}]: Deduction and
Theorem Proving---\emph{logic programming}; \emph{nonmonotonic
reasoning and belief revision}

\end{categories}

\begin{terms}

Query Evaluation, Deductive Databases, Logic Programming

\end{terms}

\begin{keywords}

Program transformations, stable models, tabled evaluation, well-founded models

\end{keywords}

\end{document}
