Abstract
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.
This research was supported in part by grants from the Israel Science Foundation
Chapter PDF
References
K. R. Apt and M. Bezem. Acyclic Programs. New Generation Computing, 9:335–363, 1991.
K. R. Apt and D. Pedreschi. Reasoning about Termination of Pure Prolog Programs. Information and Computation, 106:109–157, 1993.
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.
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.
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.
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Programming, 13:103–179, 1992.
D. De Schreye and S. Decorte. Termination of Logic Programs: the Never-Ending Story. J. Logic Programming, 19/20:199–260, 1994.
N. Lindenstrauss and Y. Sagiv. Checking Termination of Queries to Logic Programs. http://www.cs.huji.ac.il/~naomil/
N. Lindenstrauss and Y. Sagiv. Automatic Termination Analysis of Logic Programs. ICLP'97. MIT Press, 1997.
N. Lindenstrauss and Y. Sagiv. Automatic Termination Analysis of Logic Programs (with Detailed Experimental Results). http://www.cs.huji.ac.il/~naomil/
N. Lindenstrauss, Y. Sagiv and A. Serebrenik. An Example Session with TermiLog. http://www.cs.huji.ac.il/~naomil/
J. W. Lloyd. Foundations of Logic Programming. Springer Verlag, second edition, 1987.
R. A. O'Keefe. The Craft of Prolog. MIT Press, 1990.
L. Plumer. Termination Proofs for Logic Programs. Springer Verlag, LNAI 446, 1990.
Y. Sagiv. A termination test for logic programs. In International Logic Programming Symposium. MIT Press, 1991.
SICStus Prolog User's Manual. Release 3. Swedish Institute of Computer Science, 1995.
L. Sterling and E. Shapiro. The Art of Prolog. MIT Press, 1986.
J. D. Ullman and A. Van Gelder. Efficient tests for top-down termination of logical rules. JACM 35:2(1988), 345–373.
A. Van Gelder. Deriving constraints among argument sizes in logic programs. Annals of Mathematics and Artificial Intelligence, 3:361–392, 1991.
C. Verschaetse. Static Termination Analysis for Definite Horn Clause Programs. Ph.D. Thesis, K.U. Leuven, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lindenstrauss, N., Sagiv, Y., Serebrenik, A. (1997). TermiLog: A system for checking termination of queries to logic programs. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_44
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive