Abstract
We study termination of logic programs with dynamic scheduling, as it can be realised using delay declarations. Following previous work, our minimum assumption is that derivations are input-consuming, a notion introduced to define dynamic scheduling in an abstract way. Since this minimum assumption is sometimes insufficient to ensure termination, we consider here various additional assumptions on the permissible derivations. In one dimension, we consider derivations parametrised by any property that the selected atoms must have, e.g. being ground in the input positions. In another dimension, we consider both local and non-local derivations. In all cases, we give sufficient criteria for termination. The dimensions can be combined, yielding the most comprehensive approach so far to termination of logic programs with dynamic scheduling. For non-local derivations, the termination criterion is even necessary.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Apt, K.R.: From Logic Programming to Prolog. Prentice-Hall, Englewood Cliffs (1997)
Apt, K.R., Etalle, S.: On the unification free Prolog programs. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 1–19. Springer, Heidelberg (1993)
Apt, K.R., Luitjes, I.: Verification of logic programs with delay declarations. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 66–90. Springer, Heidelberg (1995)
Apt, K.R., Pedreschi, D.: Reasoning about termination of pure Prolog programs. Information and Computation 106(1), 109–157 (1993)
Apt, K.R., Pedreschi, D.: Modular termination proofs for logic and pure Prolog programs. In: Levi, G. (ed.) Advances in Logic Programming Theory, pp. 183–229. Oxford University Press, Oxford (1994)
Bossi, A., Etalle, S., Rossi, S.: Properties of input-consuming derivations. Theory and Practice of Logic Programming 2(2), 125–154 (2002)
Bossi, A., Etalle, S., Rossi, S., Smaus, J.-G.: Semantics and termination of simply moded logic programs with dynamic scheduling. Transactions on Computational Logic (2004) (to appear in summer 2004)
De Schreye, D., Decorte, S.: Termination of logic programs: The never-ending story. Journal of Logic Programming 19/20, 199–260 (1994)
Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing (1/2), 117–156 (2001)
Etalle, S., Bossi, A., Cocco, N.: Termination of well-moded programs. Journal of Logic Programming 38(2), 243–257 (1999)
Genaim, S., Codish, M., Gallagher, J., Lagoon, V.: Combining norms to prove termination. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 126–138. Springer, Heidelberg (2002)
Hill, P.M., Lloyd, J.W.: The Gödel Programming Language. MIT Press, Cambridge (1994)
Lüttringhaus-Kappel, S.: Control generation for logic programs. In: Warren, D.S. (ed.) Proceedings of the 10th International Conference on Logic Programming, pp. 478–495. MIT Press, Cambridge (1993)
Marchiori, E., Teusink, F.: On termination of logic programs with delay declarations. Journal of Logic Programming 39(1-3), 95–124 (1999)
Martin, J., King, A.: Generating efficient, terminating logic programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 273–284. Springer, Heidelberg (1997)
Mesnard, F., Neumerkel, U.: Applying static analysis techniques for inferring termination conditions of logic programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 93–110. Springer, Heidelberg (2001)
Naish, L.: Coroutining and the construction of terminating logic programs. Technical Report 92/5, Department of Computer Science, University of Melbourne (1992)
Pedreschi, D., Ruggieri, S., Smaus, J.-G.: Classes of terminating logic programs. Theory and Practice of Logic Programming 2(3), 369–418 (2002)
Smaus, J.-G.: Proving termination of input-consuming logic programs. In: De Schreye, D. (ed.) Proc. of the International Conference on Logic Programming, pp. 335–349. MIT Press, Cambridge (1999)
Smaus, J.-G.: Termination of logic programs for various dynamic selection rules. Technical Report 191, Institut für Informatik, Universität Freiburg (2003)
Smaus, J.-G.: Termination of logic programs using various dynamic selection rules. Technical Report 203, Institut für Informatik, Universität Freiburg (2004)
Smaus, J.-G., Hill, P.M., King, A.M.: Verifying termination and error-freedom of logic programs with block declarations. Theory and Practice of Logic Programming 1(4), 447–486 (2001)
Swedish Institute of Computer Science. SICStus Prolog User’s Manual (2003), http://www.sics.se/isl/sicstuswww/site/documentation.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smaus, JG. (2004). Termination of Logic Programs Using Various Dynamic Selection Rules. In: Demoen, B., Lifschitz, V. (eds) Logic Programming. ICLP 2004. Lecture Notes in Computer Science, vol 3132. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27775-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-27775-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22671-0
Online ISBN: 978-3-540-27775-0
eBook Packages: Springer Book Archive