Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-28T11:51:26.685Z Has data issue: false hasContentIssue false
  • English
  • Français

Termination prediction for general logic programs

Published online by Cambridge University Press:  16 June 2009

YI-DONG SHEN ,
DANNY DE SCHREYE  and
DEAN VOETS
YI-DONG SHEN
Affiliation:
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China (e-mail: [email protected])
DANNY DE SCHREYE
Affiliation:
Department of Computer Science, Celestijnenlaan 200 A, B-3001 Heverlee, Belgium (e-mail: [email protected], [email protected])
DEAN VOETS
Affiliation:
Department of Computer Science, Celestijnenlaan 200 A, B-3001 Heverlee, Belgium (e-mail: [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination proof approaches. We introduce an idea of termination prediction, which predicts termination of a logic program in case that neither a termination nor a non-termination proof is applicable. We establish a necessary and sufficient characterization of infinite (generalized) SLDNF-derivations with arbitrary (concrete or moded) queries, and develop an algorithm that predicts termination of general logic programs with arbitrary nonfloundering queries. We have implemented a termination prediction tool and obtained quite satisfactory experimental results. Except for five programs which break the experiment time limit, our prediction is 100% correct for all 296 benchmark programs of the Termination Competition 2007, of which 18 programs cannot be proved by any of the existing state-of-the-art analyzers like AProVE07, NTI, Polytool, and TALP.

Keywords

Logic programmingtermination analysisloop checkingmoded queriestermination prediction
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 9 , Issue 6 , November 2009 , pp. 751 - 780
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aguzzi, G. and Modigliani, U. 1993. Proving termination of logic programs by transforming them into equivalent term rewriting systems. In Proceedings of the 13th FST and TCS, Bombay, India. Lecture Notes in Computer Science 761, Springer, 114–124.Google Scholar
Apt, K. R. and Pedreschi, D. 1993. Reasoning about termination of pure prolog programs. Information and Computation 106 (1), 109–157.CrossRefGoogle Scholar
Arts, T. and Zantema, H. 1995. Termination of logic programs using semantic unification. In Proceedings of the 5th International Symposium on Logic-based Program Synthesis and Transformation, Utrecht, the Netherlands. Lecture Notes in Computer Science 1048, Springer, 219–233.Google Scholar
Bol, R. N., Apt, K. R. and Klop, J. W. 1991. An analysis of loop checking mechanisms for logic programs. Theoretical Computer Science 86 (1), 35–79.CrossRefGoogle Scholar
Bossi, A., Cocco, N., Rossi, S. and Etalle, S. 2002. On modular termination proofs of general logic programs. Theory and Practice of Logic Programming 2 (3), 263–291.CrossRefGoogle Scholar
Bruynooghe, M., Codish, M., Gallagher, J., Genaim, S. and Vanhoof, W. 2007. Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems 29 (2), 10.CrossRefGoogle Scholar
Bruynooghe, M., Schreye, D. D. and Martens, B. 1992. A general criterion for avoiding infinite unfolding during partial deduction. New Generation Computing 11 (1), 47–79.CrossRefGoogle Scholar
Chen, W. D. and Warren, D. S. 1996. Tabled evaluation with delaying for general logic programs. Journal of the ACM 43 (1), 20–74.CrossRefGoogle Scholar
Clark, K. L. 1978. Negation as failure. In Logic and Databases, Ed. Gallaire, H. and Minker, J., Perseus Publishing, 293–322.Google Scholar
Decorte, S., Schreye, D. D. and Vandecasteele, H. 1999. Constraint-based termination analysis of logic programs. ACM Transactions on Programming Languages and Systems 21 (6), 1137–1195.CrossRefGoogle Scholar
Dershowttz, N., Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. 2001. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing 12 (1/2), 117–156.CrossRefGoogle Scholar
Gelder, A. V. 1987. Efficient loop detection in prolog. Journal of Logic Programming 4, 23–31.CrossRefGoogle Scholar
Genaim, S. and Codish, M. 2005. Inferring termination conditions for logic programs using backwards analysis. Theory and Practice of Logic Programming 5 (1/2), 75–91.CrossRefGoogle Scholar
Giesl, J., Schneider-Kamp, P. and Thiemann, R. 2006. Aprove 1.2: Automatic termination proofs in the dp framework. In Proceedings of the 3rd IJCAR, Seattle, WA, USA. Lecture Notes in Computer Science 4130, Springer, 281–286.Google Scholar
Lindenstrauss, N. and Sagiv, Y. 1997. Automatic termination analysis of logic programs. In Proceedings of the 14th ICLP, Leuven, Belgium. MIT Press, 63–77.Google Scholar
Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. 1997. Termilog: A system for checking termination of queries to logic programs. In Proceedings of the 9th CAV, Haifa, Israel. Lecture Notes in Computer Science 1254, Springer, 444–447.Google Scholar
Lloyd, J. W. 1987. Foundations of Logic Programming. Springer-Verlag, Berlin.CrossRefGoogle Scholar
Marchiori, E. 1996a. Practical methods for proving termination of general logic programs. Journal of Artificial Intelligence Research 4, 179–208.CrossRefGoogle Scholar
Marchiori, M. 1996b. Proving existential termination of normal logic programs. In Proceedings of the 5th AMAST, Munich, Germany. Lecture Notes in Computer Science 1101, Springer, 375–390.Google Scholar
Martens, B. and Schreye, D. D. 1996. Automatic finite unfolding using well-founded measures. Journal of Logic Programming 28 (2), 89–146.CrossRefGoogle Scholar
Mesnard, F. and Bagnara, R. 2005. cti: A constraint-based termination inference tool for iso-prolog. Theory and Practice of Logic Programming 5 (1/2), 243–257.CrossRefGoogle Scholar
Mesnard, F. and Neumerkel, U. 2001. Applying static analysis techniques for inferring termination conditions of logic programs. In Proceedings of the 8th International Symposium on Static Analysis, Paris, France. Lecture Notes in Computer Science 2126, Springer, 93–110.Google Scholar
Nguyen, M. T. and Schreye, D. D. 2005. Polynomial interpretations as a basis for termination analysis of logic programs. In Proceedings of the 21st ICLP, Sitges, Spain. Lecture Notes in Computer Science 3668, Springer, 311–326.Google Scholar
Nguyen, M. T., Schreye, D. D., Giesl, J. and Schneider-Kamp, P. 2006. Polytool: Proving Termination Automatically Based on Polynomial Interpretations. Technical Report, Department of Computer Science, K.U. Leuven, Belgium.Google Scholar
Ohlebusch, E., Claves, C., and Marche, C. 2000. Talp: A tool for the termination analysis of logic programs. In Proceedings of the 11th RTA, Norwich, UK. Lecture Notes in Computer Science 1833, Springer, 270–273.Google Scholar
Payet, E. 2006. Detecting non-termination of term rewriting systems using an unfolding operator. In Proc. of the 16th International Symposium on Logic-Based Program Synthesis and Transformation, Venice, Italy. Lecture Notes in Computer Science 4407, Springer, 194–209.Google Scholar
Payet, E. and Mesnard, F. 2006. Non-termination inference of logic programs. ACM Transactions on Programming Languages and Systems 28 (2), 256–289.CrossRefGoogle Scholar
Rao, M. K., Kapur, D. and Shyamasundar, R. 1998. Transformational methodology for proving termination of logic programs. Journal of Logic Programming 34 (1), 1–42.Google Scholar
Sahlin, D. 1993. Mixtus: An automatic partial evaluator for full prolog. New Generation Computing 12 (1), 7–51.CrossRefGoogle Scholar
Schneider-Kamp, P., Giesl, J., Serebrenik, A. and Thiemann, R. 2006. Automated termination analysis for logic programs by term rewriting. In Proceedings of the 16th International Symposium on Logic-based Program Synthesis and Transformation, Venice, Italy. Lecture Notes in Computer Science 4407, Springer, 177–193.Google Scholar
Schreye, D. D. and Decorte, S. 1993. Termination of logic programs: The never-ending story. Journal of Logic Programming 19/20 (1), 199–260.CrossRefGoogle Scholar
Shen, Y. D. 1997. An extended variant of atoms loop check for positive logic programs. New Generation Computing 15 (2), 187–204.CrossRefGoogle Scholar
Shen, Y. D., You, J. H. and Yuan, L. Y. 2004. Enhancing global sls-resolution with loop cutting and tabling mechanisms. Theoretical Computer Science 328 (3), 271–287.CrossRefGoogle Scholar
Shen, Y. D., You, J. H., Yuan, L. Y., Shen, S. P. and Yang, Q. 2003. A dynamic approach to characterizing termination of general logic programs. ACM Transactions on Compututational Logic 4 (4), 417–430.CrossRefGoogle Scholar
Shen, Y. D., Yuan, L. Y. and You, J. H. 2001. Loop checks for logic programs with functions. Theoretical Computer Science 266 (1–2), 441–461.CrossRefGoogle Scholar
van Raamsdonk, F. 1997. Translating logic programs into conditional rewriting systems. In Proceedings of the 14th ICLP, Leuven, Belgium. MIT Press, 168–182.Google Scholar
Verbaeten, S., Schreye, D. D. and Sagonas, K. 2001. Termination proofs for logic programs with tabling. ACM Transactions on Computational Logic 2 (1), 57–92.CrossRefGoogle Scholar