Abstract
In this paper, we present a new approach to non-termination analysis of logic programs, based on moded SLDNF-resolution. Moded SLDNF-resolution is a symbolic execution for moded goals, developed for termination prediction. To prove non-termination, we use a complete loop checker to create a finite symbolic derivation tree of a logic program for a moded query. Then, we check if this derivation tree contains an infinite loop, using a new non-termination condition. We implemented this approach and tested it on the benchmark from the Termination Competition of 2007. The results are very satisfactory: our tool is able to prove non-termination and construct non-terminating queries for all non-terminating benchmark programs, and thus, significantly improves on the results of the only other non-termination analyzer, NTI.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bol, R.N.: Loop checking in logic programming. CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands (1995)
Bruynooghe, M., Codish, M., Gallagher, J., Genaim, S., Vanhoof, W.: Termination analysis through combination of type based norms. TOPLASÂ 29(2), 10 (2007)
Bruynooghe, M., Janssens, G.: An instance of abstract interpretation integrating type and mode inferencing. In: ICLP/SLP, pp. 669–683 (1988)
Codish, M.: Proving termination with (boolean) satisfaction. In: King, A. (ed.) LOPSTR 2007. LNCS, vol. 4915, pp. 1–7. Springer, Heidelberg (2008)
Debray, S.K., López-GarcÃa, P., Hermenegildo, M.V.: Non-failure analysis for logic programs. In: ICLP, pp. 48–62 (1997)
Decorte, S., De Schreye, D., Vandecasteele, H.: Constraint-based termination analysis of logic programs. TOPLAS 21(6), 1137–1195 (1999)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)
Mesnard, F., Bagnara, R.: Cti: A constraint-based termination inference tool for iso-prolog. TPLP 5(1-2), 243–257 (2005)
Nguyen, M.T., De Schreye, D.: Polytool: Proving termination automatically based on polynomial interpretations. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 210–218. Springer, Heidelberg (2007)
Payet, É., Mesnard, F.: Nontermination inference of logic programs. ACM Transactions on Programming Languages and Systems 28(2), 256–289 (2006)
Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination analysis for logic programs by term rewriting. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 177–193. Springer, Heidelberg (2007)
Shen, Y.-D., De Schreye, D., Voets, D.: Termination prediction for general logic programs. Report CW 2009 536, K.U.L. Accepted for TPLP
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Voets, D., De Schreye, D. (2009). A New Approach to Non-termination Analysis of Logic Programs. In: Hill, P.M., Warren, D.S. (eds) Logic Programming. ICLP 2009. Lecture Notes in Computer Science, vol 5649. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02846-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-02846-5_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02845-8
Online ISBN: 978-3-642-02846-5
eBook Packages: Computer ScienceComputer Science (R0)