Abstract
Loop checking is a mechanism used to prune infinite SLD-derivations. Here we study two classes of loop checking mechanisms — subsumption checks and context checks. We analyze their soundness, completeness relative strength and related concepts. We prove their soundness (no computed answer substitution to a goal is missed) and demonstrate their completeness (all resulting derivations are finite) for some classes of logic programs. The completeness theorems for the subsumption checks make use of a simple version of Kruskal's Tree Theorem [K], called Higman's Lemma [H].
This paper is a sequel to Apt, Bol and Klop [ABK] where a formal framework for studying loop checking mechanisms was introduced and where so-called equality checks were studied.
This research was partly supported by Esprit BRA-project 3020 Integration.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
K.R. Apt, R.N. Bol and J.W. Klop, On the Safe Termination of PROLOG Programs, in: Proceedings of the Sixth International Conference on Logic Programming, (G. Levi and M. Martelli eds.), MIT Press, Cambridge Massachusetts, 1989, 353–368.
Ph. Besnard, On Infinite Loops in Logic Programming, Internal Report 488, IRISA, Rennes, 1989.
D.R. Brough and A. Walker, Some Practical Properties of Logic Programming Interpreters, in: Proceedings of the International Conference on Fifth Generation Computer Systems, (ICOT eds), 1984, 149–156.
M.A. Covington, Eliminating Unwanted Loops in PROLOG, SIGPLAN Notices, Vol. 20, No. 1, 1985, 20–26.
C.L. Chang and R.C. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.
N. Dershowitz, A note on Simplification Orderings, Information Processing Letters 9, 1979, 212–215.
A. van Gelder, Efficient Loop Detection in PROLOG using the Tortoise-and-Hare Technique, J. Logic Programming 4, 1987, 23–31.
G. Higman, Ordering by divisibility in abstract algebra's, Proceedings of the London Mathematical Society (3) 2 (7), 1952, 215–221.
J.B. Kruskal, Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture, Transactions of the AMS 95, 1960, 210–225.
J.W. Lloyd, Foundations of Logic Programming, Second Edition, Springer-Verlag, Berlin, 1987.
J.W. Lloyd and J.C. Shepherdson, Partial Evaluation in Logic Programming, Technical Report CS-87-09, Dept. of Computer Science, University of Bristol, 1987.
D. Poole and R. Goebel, On Eliminating Loops in PROLOG, SIGPLAN Notices, Vol. 20, No. 8, 1985, 38–40.
D.E. Smith, M.R. Genesereth and M.L. Ginsberg, Controlling Recursive Inference, Artificial Intelligence 30, 1986, 343–389.
H. Seki and H. Itoh, A Query Evaluation Method for Stratified Programs under the Extended CWA, in: Proceedings of the Fifth International Conference on Logic Programming, MIT Press, Cambridge Massachusetts, 1988, 195–211.
L. Vieille, Recursive Query Processing: The Power of Logic, Theoretical Computer Science 68, No. 2, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bol, R.N., Apt, K.R., Klop, J.W. (1990). On the power of subsumption and context checks. In: Miola, A. (eds) Design and Implementation of Symbolic Computation Systems. DISCO 1990. Lecture Notes in Computer Science, vol 429. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52531-9_132
Download citation
DOI: https://doi.org/10.1007/3-540-52531-9_132
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52531-8
Online ISBN: 978-3-540-47014-4
eBook Packages: Springer Book Archive