Abstract
The most important open problem in the study of termination for logic programs is that of existential termination. In this paper we present a powerful transformational methodology that provides necessary (and, under some conditions, sufficient) criteria for existential termination. The followed approach is to develop a suitable transformation from logic programs to Term Rewriting Systems (TRSs), such that proving termination of the obtained TRS implies existential termination of the original logic program. Thus, all the extensive amount of work on termination for TRSs can be automatically used in the logic programming setting. Moreover, the approach is also able to cope with the dual notion of universal termination: in fact, a whole spectrum of termination properties, said k-termination, is investigated, of which universal and existential termination are the extremes. Also, a satisfactory treatment to the problem of termination for logic programming with negation is achieved. This way we provide a unique, uniform approach covering all these different notions of termination.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
G. Aguzzi and U. Modigliani. Proving termination of logic programs by transforming them into equivalent term rewriting systems. FST&TCS, LNCS 761, pp. 114–124. 1993.
A. Aiken and T.K. Lakshman. Directional type checking of logic programs. In Proc. of SAS, LNCS 864, pages 43–60, 1994.
K.R. Apt and S. Etalle. On the unification free Prolog programs. Proc MFCS LNCS 711, pp. 1–19. Springer, 1993.
K.R. Apt and D. Pedreschi. Proving termination of general Prolog programs. In Proc TACS, LNCS 526, pages 265–289. Springer-Verlag, 1991.
T. Arts and H. Zantema. Termination of logic programs using semantic unification. In Proc. 5th LoPSTr, LNCS. 1996. To appear.
M. Baudinet. Proving termination properties of Prolog programs: a semantic approach. Journal of Logic Programming, 14:1–29, 1992.
F. Bronsard, T.K. Lakshman, and U.S Reddy. A framework of directionality for proving termination of logic programs. Proc. JICSLP, pp. 321–335. The MIT Press, 1992.
M. Chtourou and M. Rusinowitch. Méthode transformationnelle pour la preuve de terminaison des programmes logiques. Manuscript, 1993.
K.L. Clark and S.-Å. Tärnlund. A first order theory of data and programs. In B. Gilchrist, editor, Proc. IFIP Congress on Information Processing, pp. 939–944, 1977.
H. Coelho and J.C. Cotta. Prolog by Example. Springer-Verlag, 1988.
L. Colussi, E. Marchiori, and M. Marchiori. On termination of constraint logic programs. In Proc. CP'95, LNCS 976, pp. 431–448. Springer, 1995.
T. Conway, F. Henderson, and Z. Somogyi. Code generation for Mercury. In Proc. International Logic Programming Symposium, pp. 242–256. The MIT Press, 1995.
D. de Schreye and S. Decorte. Termination of logic programs: The never-ending story. Journal of Logic Programming, 19,20:199–260, 1994.
S.K. Debray. Static inference of modes and data dependencies in logic programs. ACM TOPLAS, 11(3):418–450, July 1989.
N. Dershowitz. Termination of rewriting. J. of Symbolic Computation, 3:69–116, 1987.
N. Dershowitz and C. Hoot. Topics in termination. In Proceedings of the Fifth RTA, LNCS 690, pp. 198–212. Springer, 1993.
N. Dershowitz and J. Jouannaud. Rewrite systems. Handbook of Theoretical Computer Science, vol. B, chapter 6, pp. 243–320. Elsevier-MIT Press, 1990.
N. Franchez, O. Grumberg, S. Katz, and A. Pnueli. Proving termination of Prolog programs. In R. Parikh, editor, Logics of programs, pp. 89–105. Springer, 1985.
H. Ganzinger and U. Waldmann. Termination proofs of well-moded logic programs via conditional rewrite systems. CTRS'92, LNCS 656, pp. 216–222. Springer, 1993.
G. Levi and F. Scozzari. Contributions to a theory of existential termination for definite logic programs. GULP-PRODE'95, pp. 631–642. 1995.
J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, second edition, 1987.
E. Marchiori. Practical methods for proving termination of general logic programs. The Journal of Artificial Intelligence Research, 1996. To appear.
M. Marchiori. Logic programs as term rewriting systems. Proc. 3rd Int. Conf. on Algebraic and Logic Programming, LNCS 850, pp. 223–241. Springer, 1994.
M. Marchiori. Localizations of unification freedom through matching directions. Proc. International Logic Programming Symposium, pp. 392–406. The MIT Press, 1994.
M. Marchiori. The functional side of logic programming. In Proc. ACM FPCA, pages 55–65. ACM Press, 1995.
K. Rao, D. Kapur, and R.K. Shyamasundar. A transformational methodology for proving termination of logic programs. 5th CSL, LNCS 626, pp. 213–226, Springer, 1992.
K Rao, P.K. Pandya, and R.K. Shyamasunder. Verification tools in the development of provably correct compilers. FME'93, LNCS 670, pp. 442–461. Springer, 1993.
Y. Rouzaud and L. Nguyen-Phoung. Integrating modes and subtypes into a Prolog type checker. In Proc. JICSLP, pages 85–97. The MIT Press, 1992.
L. Sterling and E. Shapiro. The Art of Prolog. The MIT Press, 1986.
B. Wang and R.K. Shyamasundar. A methodology for proving termination of logic programs. Journal of Logic Programming, 21(1):1–30, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marchiori, M. (1996). Proving existential termination of normal logic programs. In: Wirsing, M., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1996. Lecture Notes in Computer Science, vol 1101. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014328
Download citation
DOI: https://doi.org/10.1007/BFb0014328
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61463-0
Online ISBN: 978-3-540-68595-1
eBook Packages: Springer Book Archive