×

Termination analysis of logic programs based on dependency graphs. (English) Zbl 1179.68040

King, Andy (ed.), Logic-based program synthesis and transformation. 17th international symposium, LOPSTR 2007, Kongens Lyngby, Denmark, August 23–24, 2007. Revised selected papers. Berlin: Springer (ISBN 978-3-540-78768-6/pbk). Lecture Notes in Computer Science 4915, 8-22 (2008).
Summary: This paper introduces a modular framework for termination analysis of logic programming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the logic programming domain. The main idea of the approach is that termination conditions for a program are established based on the decomposition of its dependency graph into its strongly connected components. These conditions can then be analysed separately by possibly different well-founded orders. We propose a constraint-based approach for automating the framework. Then, for example, termination techniques based on polynomial interpretations can be plugged in as a component to generate well-founded orders.
For the entire collection see [Zbl 1154.68018].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N17 Logic programming

Software:

TPDB; AProVE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), 133–178 (2000) · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8
[2] Bol, R.N., Apt, K.R., Klop, J.W.: An analysis of loop checking mechanisms for logic programs. Theoretical Computer Science 86(1), 35–79 (1991) · Zbl 0741.68027 · doi:10.1016/0304-3975(91)90004-L
[3] Bossi, A., Cocco, N., Fabris, M.: Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science 124(2), 297–328 (1994) · Zbl 0795.68040 · doi:10.1016/0304-3975(92)00019-N
[4] Bruynooghe, M., Codish, M., Gallagher, J.P., Genaim, S., Vanhoof, W.: Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems 29(2) (2007) · Zbl 05459388 · doi:10.1145/1216374.1216378
[5] Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41(1), 103–123 (1999) · Zbl 0948.68114 · doi:10.1016/S0743-1066(99)00006-0
[6] Codish, M., Genaim, S.: Proving termination one loop at a time. In: Proc. WLPE 2003 (2003)
[7] Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning 34(4), 325–363 (2005) · Zbl 1108.03017 · doi:10.1007/s10817-005-9022-x
[8] De Schreye, D., Verschaetse, K., Bruynooghe, M.: A framework for analyzing the termination of definite logic programs with respect to call patterns. In: Proc. FGCS 1992, pp. 481–488 (1992) · Zbl 0862.68016
[9] De Schreye, D., Serebrenik, A.: Acceptability with General Orderings. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2407, pp. 187–210. Springer, Heidelberg (2002) · Zbl 1012.68037 · doi:10.1007/3-540-45628-7_9
[10] Decorte, S., De Schreye, D., Vandecasteele, H.: Constraint-based automatic termination analysis of logic programs. ACM Transactions on Programming Languages and Systems 21(6), 1137–1195 (1999) · doi:10.1145/330643.330645
[11] Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation 3(1-2), 69–116 (1987) · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6
[12] Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. In: Applicable Algebra in Engineering, Communication and Computing, 12(1,2), pp. 117–156 (2001) · Zbl 0977.68052 · doi:10.1007/s002000100065
[13] Waldmann, J., Zantema, H., Endrullis, J.: Matrix Interpretations for Proving Termination of Term Rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 574–588. Springer, Heidelberg (2006) · Zbl 1222.68362 · doi:10.1007/11814771_47
[14] Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT Solving for Termination Analysis with Polynomial Interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007) · Zbl 1214.68352 · doi:10.1007/978-3-540-72788-0_33
[15] Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation 34(1), 21–58 (2002) · Zbl 1010.68073 · doi:10.1006/jsco.2002.0541
[16] Giesl, J., Thiemann, R., Schneider-Kamp, P.: The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005) · Zbl 1108.68477 · doi:10.1007/978-3-540-32275-7_21
[17] Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006) · Zbl 05528293 · doi:10.1007/11814771_24
[18] Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006) · Zbl 1113.68088 · doi:10.1007/s10817-006-9057-7
[19] Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation 199(1-2), 172–199 (2005) · Zbl 1081.68038 · doi:10.1016/j.ic.2004.10.004
[20] Hong, H., Jakuš, D.: Testing positiveness of polynomials. Journal of Automated Reasoning 21(1), 23–38 (1998) · Zbl 0916.68084 · doi:10.1023/A:1005983105493
[21] Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 48–62. Springer, Heidelberg (1999) · Zbl 0953.68068 · doi:10.1007/10704567_3
[22] Lankford, D.S.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)
[23] Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. POPL 2001, pp. 81–92 (2001) · Zbl 1323.68216 · doi:10.1145/360204.360210
[24] Marché, C., Zantema, H.: The Termination Competition. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 303–313. Springer, Heidelberg (2007) · Zbl 05222820 · doi:10.1007/978-3-540-73449-9_23
[25] Mesnard, F., Bagnara, R.: cTI: A constraint-based termination inference tool for ISO-Prolog. In: Theory and Practice of Logic Programming, vol. 5(1, 2), pp. 243–257 (2005) · Zbl 1093.68559
[26] Nguyen, M.T., De Schreye, D.: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 311–325. Springer, Heidelberg (2005) · Zbl 1165.68337 · doi:10.1007/11562931_24
[27] De Schreye, D., Nguyen, M.T.: Polytool: Proving Termination Automatically Based on Polynomial Interpretations. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 210–218. Springer, Heidelberg (2007) · Zbl 05189215 · doi:10.1007/978-3-540-71410-1_15
[28] Plümer, L.: Termination Proofs for Logic Programs. Springer, Heidelberg (1990) · Zbl 0705.68090 · doi:10.1007/3-540-52837-7
[29] Podelski, A., Rybalchenko, A.: Transition invariants. In: Proc. LICS 2004, pp. 32–41 (2004) · Zbl 1315.68104 · doi:10.1109/LICS.2004.1319598
[30] Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Society 30, 264–286 (1930) · JFM 55.0032.04 · doi:10.1112/plms/s2-30.1.264
[31] 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) · Zbl 1196.68036 · doi:10.1007/978-3-540-71410-1_13
[32] The termination problem data base, http://www.lri.fr/ marche/tpdb .
[33] Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing 16(4), 229–270 (2005) · Zbl 1101.68640 · doi:10.1007/s00200-005-0179-7
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.