Detecting Optimal Termination Conditions of Logic Programs

  • Fred Mesnard
  • Etienne Payet
  • Ulrich Neumerkel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)


In this paper, we begin with an approach to non-termination inference of logic programs. Our framework relies on an extension of the Lifting Theorem, where some specific argument positions can be instantiated while others are generalized. Atomic left looping queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. Then non-termination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. For each class of atomic queries not covered by a termination condition, the aim is to ensure the existence of one query from this class which leads to an infinite search tree. An experimental evaluation is reported. When termination and non-termination analysis produce complementary results for a logic procedure, they induce a characterization of the operational behavior of the logic procedure with respect to the left most selection rule and the language used to describe sets of atomic queries.


Logic Program Predicate Symbol Relation Symbol Partial Correctness Loop Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K. R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.Google Scholar
  2. 2.
    K. R. Apt and D. Pedreschi. Modular termination proofs for logic and pure Prolog programs. In G. Levi, editor, Advances in Logic Programming Theory, pages 183–229. Oxford University Press, 1994.Google Scholar
  3. 3.
    K. R. Apt and M. H. Van Emden. Contributions to the theory of logic programming. Journal of the ACM, 29(3):841–862, 1982.zbMATHCrossRefGoogle Scholar
  4. 4.
    T. Arts and H. Zantema. Termination of logic programs using semantic unification. In Logic Program Synthesis and Transformation, volume 1048 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1996.Google Scholar
  5. 5.
    R. Bol. Loop Checking in Logic Programming. PhD thesis, CWI, Amsterdam, 1991.Google Scholar
  6. 6.
    M. Bruynooghe, D. De Schreye, and B. Martens. A general criterion for avoiding infinite unfolding during partial deduction. New Generation Computing, 11(1):47–79, 1992.zbMATHCrossRefGoogle Scholar
  7. 7.
    M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming, 41(1):103–123, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    D. De Schreye, M. Bruynooghe, and K. Verschaetse. On the existence of non-terminating queries for a restricted class of Prolog-clauses. Artificial Intelligence, 41:237–248, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    D. De Schreye and S. Decorte. Termination of logic programs: the never-ending story. Journal of Logic Programming, 19–20:199–260, 1994.CrossRefMathSciNetGoogle Scholar
  10. 10.
    N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering,Communication and Computing, 12(1/2):117–156, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    P. Devienne, P. Lebégue, and J-C. Routier. Halting problem of one binary Horn clause is undecidable. In LNCS, volume 665, pages 48–57. Springer-Verlag, 1993. Proc. of STACS’93.Google Scholar
  12. 12.
    M. Gabbrielli and R. Giacobazzi. Goal independency and call patterns in the analysis of logic programs. In Proceedings of the ACM Symposium on applied computing, pages 394–399. ACM Press, 1994.Google Scholar
  13. 13.
    S. Genaim and M. Codish. Inferring termination condition for logic programs using backwards analysis. In Proceedings of Logic for Programming, Artificial intelligence and Reasoning, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2001. TerminWeb can be used online from Scholar
  14. 14.
    R. Gori and G. Levi. Finite failure is and-compositional. Journal of Logic and Computation, 7(6):753–776, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    H. J. Komorowski. Partial evaluation as a means for inferencing data structures in an applicative language: a theory and implementation in the case of Prolog. In Proc. of the 9th POPL, pages 255–267, 1982.Google Scholar
  16. 16.
    N. Lindenstrauss. TermiLog: a system for checking termination of queries to logic programs, 1997.ñaomil.
  17. 17.
    F. Mesnard. Inferring left-terminating classes of queries for constraint logic programs by means of approximations. In M. J. Maher, editor, Proc. of the 1996 Joint Intl. Conf. and Symp. on Logic Programming, pages 7–21. MIT Press, 1996.Google Scholar
  18. 18.
    F. Mesnard and U. Neumerkel. cTI: a tool for inferring termination conditions of ISO-Prolog, april 2000.
  19. 19.
    F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In P. Cousot, editor, Static Analysis Symposium, volume 2126 of Lecture Notes in Computer Science, pages 93–110. Springer-Verlag, Berlin, 2001.CrossRefGoogle Scholar
  20. 20.
    R. O’Keefe. The Craft Of Prolog. MIT Press, 1990.Google Scholar
  21. 21.
    L. Plümer. Termination proofs for logic programs. Number 446 in LNAI. Springer-Verlag, Berlin, 1990.zbMATHGoogle Scholar
  22. 22.
    Y-D. Shen, L-Y. Yuan, and J-H. You. Loops checks for logic programs with functions. Theoretical Computer Science, 266(1–2):441–461, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    D. Skordev. An abstract approach to some loop detection problems. Fundamenta Informaticae, 31:195–212, 1997.zbMATHMathSciNetGoogle Scholar
  24. 24.
    C. Speirs, Z. Somogyi, and H. Søndergaard. Termination analysis for Mercury. In P. Van Hentenryck, editor, Proc. of the International Static Analysis Symposium, volume 1302 of LNCS, pages 160–171. Springer-Verlag, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Fred Mesnard
    • 1
  • Etienne Payet
    • 1
  • Ulrich Neumerkel
    • 2
  1. 1.Iremia - Université de La RéunionFrance
  2. 2.Institut für ComputersprachenT. U. WienAustria

Personalised recommendations