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.
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)