Abstract
We show how to combine the two most powerful approaches for automated termination analysis of logic programs (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms LPs to term rewrite systems (TRSs) and tries to prove termination of the resulting TRSs. To this end, we adapt the well-known dependency pair framework from TRSs to LPs. With the resulting method, one can combine arbitrary termination techniques for LPs in a completely modular way and one can use both direct and transformational techniques for different parts of the same LP.
Supported by FWO/2006/09: Termination analysis: Crossing paradigm borders and by the Deutsche Forschungsgemeinschaft (DFG), grant GI 274/5-2.
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
Apt, K.R.: From Logic Programming to Prolog. Prentice Hall, London (1997)
Arts, T., Giesl, J.: Termination of Term Rewriting using Dependency Pairs. Theoretical Computer Science 236(1,2), 133–178 (2000)
Bossi, A., Cocco, N., Fabris, M.: Norms on Terms and their use in Proving Universal Termination of a Logic Program. Th. Comp. Sc. 124(2), 297–328 (1994)
Codish, M., Taboch, C.: A Semantic Basis for Termination Analysis of Logic Programs. Journal of Logic Programming 41(1), 103–123 (1999)
Dershowitz, N.: Termination of Rewriting. J. Symb. Comp. 3(1,2), 69–116 (1987)
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)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination Proofs in the DP Framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)
Hirokawa, N., Middeldorp, A.: Automating the Dependency Pair Method. Information and Computation 199(1,2), 172–199 (2005)
Janssens, G., Bruynooghe, M.: Deriving Descriptions of Possible Values of Program Variables by Means of Abstract Interpretation. Journal of Logic Programming 13(2,3), 205–258 (1992)
Jurdzinski, M.: LP Course Notes, http://www.dcs.warwick.ac.uk/mju/CS205/
Mesnard, F., Bagnara, R.: cTI: A Constraint-Based Termination Inference Tool for ISO-Prolog. Theory and Practice of Logic Programming 5(1,2), 243–257 (2005)
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)
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)
Nguyen, M.T., Giesl, J., Schneider-Kamp, P., De Schreye, D.: Termination Analysis of Logic Programs based on Dependency Graphs. In: King, A. (ed.) LOPSTR 2007. LNCS, vol. 4915, pp. 8–22. Springer, Heidelberg (2008)
Ohlebusch, E., Claves, C., Marché, C.: TALP: A Tool for the Termination Analysis of Logic Programs. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 270–273. Springer, Heidelberg (2000)
Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated Termination Proofs for Logic Programs by Term Rewriting. ACM Transactions on Computational Logic 11(1) (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schneider-Kamp, P., Giesl, J., Nguyen, M.T. (2010). The Dependency Triple Framework for Termination of Logic Programs . In: De Schreye, D. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2009. Lecture Notes in Computer Science, vol 6037. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12592-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-12592-8_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12591-1
Online ISBN: 978-3-642-12592-8
eBook Packages: Computer ScienceComputer Science (R0)