The limits of fixed-order computation
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 [8, 12] 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.
KeywordsLogic Program Ground Atom Computation Rule Ground Instance Normal Logic Program
Unable to display preview. Download preview PDF.
- 1.N. Bidoit and C. Froidevaux. Negation by default and unstratifiable logic programs. Theoretical Comput. Sci., 78(1):85–112, January 1991.Google Scholar
- 2.R. Bol and L. Degerstedt. Tabulated resolution for well founded semantics. In D. Miller, editor, Proceedings of the 1993 International Symposium on Logic Programming, pages 199–219, Vancouver, October 1993. The MIT Press.Google Scholar
- 3.W. Chen and D. S. Warren. Tabled Evaluation with Delaying for General Logic Programs. J. ACM, 43(1):20–74, January 1996.Google Scholar
- 4.J. Dix. Classifying semantics of logic programs. In A. Nerode, W. Marek, and V. S. Subrahmanian, editors, Logic Programming and Mon-Monotonic Reasoning, Proceedings of the first International Workshop, pages 166–180, Washington D.C., July 1991. The MIT Press.Google Scholar
- 5.M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In R. A. Kowalski and K. A. Bowen, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 1081–1086, Seattle, August 1988. The MIT Press.Google Scholar
- 6.S. Morishita. An Extension of Van Gelder's Alternating Fixpoint to Magic Programs. J. Comput. Syst. Sci., 52(3):506–521, June 1996.Google Scholar
- 7.H. Przymusinska and T. C. Przymusinski. Weakly Stratified Logic Programs. Fundamenta Informaticae, 13(1):51–65, March 1990.Google Scholar
- 8.T. C. Przymusinski. Every Logic Program has a Natural Stratification and an Iterated Least Fixed Point Model. In Proceedings of the Eighth ACM Symposium on Principles of Database Systems, pages 11–21, Philadelphia, Pennsylvania, March 1989. ACM.Google Scholar
- 9.T. C. Przymusinski. Well-Founded and Stationary Models of Logic Programs. Annals of Mathematics and Artificial Intelligence, 12:141–187, 1994.Google Scholar
- 10.R. Ramakrishnan, D. Srivastava, and S. Sudarshan. Controlling the search in bottom-up evaluation. In K. Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 273–287, Washington D.C., October 1992. The MIT Press.Google Scholar
- 11.R. Ramakrishnan, D. Srivastava, and S. Sudarshan. CORAL — Control, Relations, and Logic. In Proceedings of the 18th Conference on Very Large Data Bases, pages 238–249, Vancouver, Canada, August 1992.Google Scholar
- 12.K. A. Ross. A procedural semantics for well-founded negation in logic programs. Journal of Logic Programming, 13(1):1–22, May 1992.Google Scholar
- 13.K. A. Ross. Modular Stratification and Magic Sets for Datalog programs with Negation. J. ACM, 41(6):1216–1266, November 1994.Google Scholar
- 14.K. Sagonas, T. Swift, and D. S. Warren. XSB as an Efficient Deductive Database Engine. In Proceedings of the ACM SIGMOD International Conference on the Management of Data, pages 442–453, Minneapolis, Minnesota, May 1994.Google Scholar
- 15.K. Sagonas, T. Swift, and D. S. Warren. An Abstract Machine for Fixed-Order Dynamically Stratified Programs. In Proceedings of the Thirteenth International Conference on Automated Deduction, LNAI, New Brunswick, New Jersey, July 1996. Springer-Verlag. To appear.Google Scholar
- 16.P. J. Stuckey and S. Sudarshan. Well-Founded Ordered Search. In R. Shyamasundar, editor, Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, number 761 in LNCS, pages 161–171, Bombay, India, December 1993. Springer-Verlag.Google Scholar
- 17.T. Swift and D. S. Warren. An abstract machine for SLG resolution: Definite Programs. In M. Bruynooghe, editor, Proceedings of the 1994 International Symposium on Logic Programming, pages 633–652, Ithaca, November 1994. The MIT Press.Google Scholar
- 18.A. Van Gelder. The Alternating Fixpoint of Logic Programs with Negation. In Proceedings of the Eighth ACM Symposium on Principles of Database Systems, pages 1–10, Philadelphia, Pennsylvania, March 1989. ACM.Google Scholar
- 19.A. Van Gelder, K. A. Ross, and J. S. Schlipf. The Well-Founded Semantics for General Logic Programs. J. ACM, 38(3):620–650, July 1991.Google Scholar