TermiLog: A system for checking termination of queries to logic programs

  • N. Lindenstrauss
  • Y. Sagiv
  • A. Serebrenik
Tool Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


TermiLog is a system implemented in SICStus Prolog for automatically checking termination of queries to logic programs. Given a program and query, the system either answers that the query terminates or that it cannot prove termination. The system can handle automatically 82% of the 120 programs we tested it on.


Logic Program Termination Proof Prolog Program Greatest Common Divisor Datalog Program 
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.


  1. [AB91]
    K. R. Apt and M. Bezem. Acyclic Programs. New Generation Computing, 9:335–363, 1991.Google Scholar
  2. [AP93]
    K. R. Apt and D. Pedreschi. Reasoning about Termination of Pure Prolog Programs. Information and Computation, 106:109–157, 1993.Google Scholar
  3. [AP94]
    K. R. Apt and D. Pedreschi. Modular Termination Proofs for Logic and Pure Prolog Programs. In Advances in Logic Programming Theory, 183–229. Oxford University Press, 1994.Google Scholar
  4. [BrSa89]
    A. Brodsky and Y. Sagiv. Inference of monotonicity constraints in Datalog programs. Proceedings of the Eighth ACM SIGACT-SIGART-SIGMOD Symposium on Principles of Database Systems, 1989, 190–199.Google Scholar
  5. [BGH94]
    F. Bueno, M. García de la Banda and M. Hermenegildo. Effectiveness of Global Analysis in Strict Independence-Based Automatic Program Parallelization. International Symposium on Logic Programming, 320–336. MIT Press, 1994.Google Scholar
  6. [Cous92]
    P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Programming, 13:103–179, 1992.Google Scholar
  7. [DSD94]
    D. De Schreye and S. Decorte. Termination of Logic Programs: the Never-Ending Story. J. Logic Programming, 19/20:199–260, 1994.Google Scholar
  8. [LiSa96]
    N. Lindenstrauss and Y. Sagiv. Checking Termination of Queries to Logic Programs. Scholar
  9. [LiSa97]
    N. Lindenstrauss and Y. Sagiv. Automatic Termination Analysis of Logic Programs. ICLP'97. MIT Press, 1997.Google Scholar
  10. [LiSaExp]
    N. Lindenstrauss and Y. Sagiv. Automatic Termination Analysis of Logic Programs (with Detailed Experimental Results). Scholar
  11. [LSS97]
    N. Lindenstrauss, Y. Sagiv and A. Serebrenik. An Example Session with TermiLog. Scholar
  12. [Llo87]
    J. W. Lloyd. Foundations of Logic Programming. Springer Verlag, second edition, 1987.Google Scholar
  13. [O'K90]
    R. A. O'Keefe. The Craft of Prolog. MIT Press, 1990.Google Scholar
  14. [Plu90]
    L. Plumer. Termination Proofs for Logic Programs. Springer Verlag, LNAI 446, 1990.Google Scholar
  15. [Sag91]
    Y. Sagiv. A termination test for logic programs. In International Logic Programming Symposium. MIT Press, 1991.Google Scholar
  16. [SICS95]
    SICStus Prolog User's Manual. Release 3. Swedish Institute of Computer Science, 1995.Google Scholar
  17. [StSh86]
    L. Sterling and E. Shapiro. The Art of Prolog. MIT Press, 1986.Google Scholar
  18. [UV88]
    J. D. Ullman and A. Van Gelder. Efficient tests for top-down termination of logical rules. JACM 35:2(1988), 345–373.Google Scholar
  19. [VanG91]
    A. Van Gelder. Deriving constraints among argument sizes in logic programs. Annals of Mathematics and Artificial Intelligence, 3:361–392, 1991.Google Scholar
  20. [Ver92]
    C. Verschaetse. Static Termination Analysis for Definite Horn Clause Programs. Ph.D. Thesis, K.U. Leuven, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • N. Lindenstrauss
    • 1
  • Y. Sagiv
    • 1
  • A. Serebrenik
    • 1
  1. 1.Dept. of Computer ScienceHebrew UniversityJerusalemIsrael

Personalised recommendations