Click on the title to obtain a gzip-ed PostScript version of the paper (76K).

###
Abstract:

Fixed-order computation rules, used by Prolog and most deductive
database systems, do not suffice to compute the well-founded
semantics because they cannot properly resolve loops through negation.
This inadequacy is reflected both in formulations of SLS-resolution
which is an ideal search strategy, and in more practical strategies
like *SLG*, or *Well-Founded Ordered Search*.
Typically, these practical strategies combine an inexpensive fixed-order
search with a relatively expensive dynamic search, such as an alternating
fixpoint. Restricting the search space of evaluation strategies by
maximizing the use of fixed-order computation is of prime importance for
efficient goal-directed evaluation of the well-founded semantics.
Towards this end, the theory of *modular stratification*,
formulates a subset of normal logic programs whose literals can be
statically reordered so that the program can be evaluated using a
fixed-order computation rule. However, exploration of larger classes
of stratified programs that can be evaluated in this manner has been
left open in the literature, perhaps due to the lack of implementation
methods that can benefit from such results. We address the limits of
fixed-order computation by adapting results of Przymusinski to formulate
the class of *left-to-right dynamically stratified programs*.
We show that this class properly includes other classes of fixed-order
stratified programs. Furthermore, we introduce *SLG-strat*,
a variant of SLG resolution that uses a fixed-order computation rule,
and prove that it correctly evaluates ground left-to-right dynamically
stratified programs. We outline how SLG-strat can be used as a basis for
restricting the space of possible SLG derivations and, finally,
outline how these results are used in the abstract machine of XSB, and
can be used in other methods such as Ordered Search of CORAL.