Abstract.
The dependency pair approach is one of the most powerful techniques for termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by weakly monotonic well-founded orders. We improve the dependency pair approach by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, we extend transformation techniques to manipulate dependency pairs which simplify (innermost) termination proofs significantly. In order to fully automate the dependency pair approach, we show how transformation techniques and the search for suitable orders can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples.
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.
Similar content being viewed by others
References
Arts, T.: System description: The dependency pair method. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 261–264. Springer, Heidelberg (2000)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical Report AIB-2001-093, RWTH Aachen (2001)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambr. Univ. Pr., Cambridge (1998)
Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 346–364. Springer, Heidelberg (2000)
Contejean, E., Marché, C., Monate, B., Urbain, X.: Cime version 2 (2000), Available from http://cime.lri.fr
Dershowitz, N.: Termination of rewriting. J. Symbolic Comp. 3, 69–116 (1987)
Dershowitz, N.: 33 examples of termination. In: Comon, H., Jouannaud, J.-P. (eds.) TCS School 1993. LNCS, vol. 909, pp. 16–26. Springer, Heidelberg (1995)
Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing 12(1-2), 117–156 (2001)
Fissore, O., Gnaedig, I., Kirchner, H.: Cariboo: An induction based proof tool for termination with strategies. In: Proc. 4th PPDP, pp. 62–73. ACM, New York (2002)
Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra in Engineering, Communication and Computing 12(1-2), 39–72 (2001)
Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation 34(1), 21–58 (2002)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. Technical Report AIB-2003-043, RWTH Aachen, Germany (2003)
Gramlich, B.: On proving termination by innermost termination. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 97–107. Springer, Heidelberg (1996), Available from http://aib.informatik.rwth-aachen.de
Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 32–46. Springer, Heidelberg (2003)
Hirokawa, N., Middeldorp, A.: Tsukuba termination tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 311–320. Springer, Heidelberg (2003)
Huet, G., Hullot, J.-M.: Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences 25, 239–299 (1982)
Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 48–62. Springer, Heidelberg (1999)
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)
Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 593–610. Springer, Heidelberg (2001)
Ohlebusch, E.: Hierarchical termination revisited. IPL 84(4), 207–214 (2002)
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)
Steinbach, J.: Automatic termination proofs with transformation orderings. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 11–25. Springer, Heidelberg (1995); Full version appeared as Technical Report SR-92-23, Universität Kaiserslautern, Germany
Steinbach, J.: Simplification orderings: History of results. Fund. I. 24, 47–87 (1995)
Thiemann, R., Giesl, J.: Size-change termination for term rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 264–278. Springer, Heidelberg (2003)
Toyama, Y.: Counterexamples to the termination for the direct sum of term rewriting systems. Information Processing Letters 25, 141–143 (1987)
Urbain, X.: Automated incremental termination proofs for hierarchically defined term rewriting systems. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 485–498. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S. (2003). Improving Dependency Pairs. In: Vardi, M.Y., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2003. Lecture Notes in Computer Science(), vol 2850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39813-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-39813-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20101-4
Online ISBN: 978-3-540-39813-4
eBook Packages: Springer Book Archive