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 recursio~(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 goal-oriented query evaluation of general logic programs by presenting tabled evaluation with delaying, called SL.G resolution. It has three distinctive features (0 SLG resolutionis a partial deductionprocedure,consistingof sevenfundamentaltransformations. A query is transformed step by step into a set of answers. The use of transformations separates logicaf is-sues 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. (ii) 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. (iii) 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-A preliminary version of this paper as 22 W. CHEN AND D. S. WARREN Several extensions of SLD resolution with memoing have been studied, includ ing extension tables [Dietrich and Warren 1986], OLDT resolution [Tamaki and Sato 1986], and QSQR [Vieille 1987]. The main idea is to keep a global table of subgoals and their answers that have been computed. If a subgoal is identical to or subsumed by a previous one, instead of being solved using rules in a program, it is solved using answers computed for the previous subgoal. This avoids infinite branches and redundant computation due to repeated subgoals in the search space of SLD resolution. These techniques have been generalized to stratified programs [Kemp and Topor 1988; Seki and Itoh 1988] and modularly stratified programs [Ross 1991]. Nontermination may also occur due to infinite recursion through negation, which has to be treated differently from infinite recursion in definite programs. A positive loop, such as p + p, is considered failed as can be seen in the well-founded partial model of p ~ p where p is false. In contrast, a negative loop, such as p - N p, is considered indeterminate since p is undefined in the well-founded partial model of p - N p. Mechanisms for handling infinite recursion through negation have been Techniques for effective set-at-a-time query evaluation have been studied in deductive databases, including magic sets [Bancilhon et al. 1986; Beeri and Ramakrishnan 1987], magic templates [Ramakrishnan 1991], and Alexander templates [Sekl 1989]. The main idea is to simulate top-down SLD resolution to avoid generation of tuples irrelevant to the given goal. In fact, tuples of magic predicates correspond to subgoals maintained in OLDT resolution [Tamaki and Sato 1986]. For definite programs, it has been shown [Bry 1990; Seki 1989] that the top-down with memoing and the set-at-a-time approaches are essen tially equivalent. Methods of query processing have been investigated for stratified and modularly stratified programs [Bry 1989; Ramakrishnan et al. 1992; Ross 1989]. With negation, the major issue becomes maintaining dependencies among magic tuples (or subgoals) so as to ensure that a positive subgoal be fully evaluated before its negative counterpart is solved. Kemp et al. [1991] devel oped a technique that computes the well-founded partial model using a doubled program, one for deriving definitely true answers and the other for deriving potentially true answers. The doubled program technique may make too many magic facts true, which means that more subgoals are evaluated than necessary. Morishita [1992] proposed an alternating fmpoint semantics tailored to magic sets computation, which generates fewer magic facts.
Showing the abstract — retrieve the full paper via the Exa API.