Abstract
In this paper we present some new refinements of the dependency pair method for automatically proving the termination of term rewrite systems. These refinements are very easy to implement, increase the power of the method, result in simpler termination proofs, and make the method more efficient.
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., 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-09, RWTH Aachen (2001)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 5–20. Springer, Heidelberg (1986)
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 at http://cime.lri.fr/
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.: Termination dependencies. In: Proceedings of the 6th International Workshop on Termination, Technical Report DSIC-II/15/03, Universidad Politécnica de Valencia, pp. 27–30 (2003)
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. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 165–179. Springer, Heidelberg (2003)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing dependency pairs. Technical Report AIB-2003-08, RWTH Aachen, Germany (2003)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)
Gramlich, B.: Generalized sufficient conditions for modular termination of rewriting. Applicable Algebra in Engineering, Communication and Computing 5, 131–158 (1994)
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) (Full version submitted for publication)
Hirokawa, N., Middeldorp, A.: Tsukuba termination tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 311–320. Springer, Heidelberg (2003)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool (2004), Available at http://cl2-informatik.uibk.ac.at/ttt
Middeldorp, A.: Approximations for strategies and termination. In: Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol. 70(6) (2002)
Middeldorp, A., Ohsaki, H.: Type introduction for equational rewriting. Acta Informatica 36(12), 1007–1029 (2000)
Steinbach, J., Kühler, U.: Check your ordering – termination proofs and open problems. Technical Report SR-90-25, Universität Kaiserslautern (1990)
Terese, A.: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)
Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proceedings of the 2nd International Joint Conference on Automated Reasoning, LNCS(LNAI) 2004 (to appear)
Toyama, Y.: Counterexamples to the termination for the direct sum of term rewriting systems. Information Processing Letters 25, 141–143 (1987)
Urbain, X.: Modular & incremental automated termination proofs. Journal of Automated Reasoning (2004) (to appear)
Zantema, H.: TORPA: Termination of rewriting proved automatically. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 95–104. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hirokawa, N., Middeldorp, A. (2004). Dependency Pairs Revisited. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive