Abstract
In contrast to the current general way of developing tools for proving termination automatically, this paper intends to show an alternative program based on using on the one hand the theory of term orderings to develop powerful and widely applicable methods and on the other hand constraint based techniques to put them in practice.
In order to show that this program is realizable a constraint-based framework is presented where ordering based methods for term rewriting, including extensions like Associative-Commutative rewriting, Context-Sensitive rewriting or Higher-Order rewriting, as well as the use of rewriting strategies, can be put in practice in a natural way.
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
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), 133–178 (2000)
Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol. 1831, pp. 346–364. Springer, Heidelberg (2000)
Borralleras, C.: Ordering-based methods for proving termination automatically. PhD thesis, Dpto. LSI, Universitat Politècnica de Catalunya (2003)
Borralleras, C., Rubio, A.: A monotonic higher-order semantic path ordering. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 531–547. Springer, Heidelberg (2001)
Borralleras, C., Rubio, A.: Monotonic AC-compatible semantic path orderings. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 279–295. Springer, Heidelberg (2003)
Fissore, O., Gnaedig, I., Kirchner, H.: CARIBOO: An Induction Based Proof Tool for Termination with Strategies. In: Proc. 4th Int. Conf. on Principles and Practice of Declarative Programming, pp. 62–73. ACM Press, New York (2002)
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., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning 37(3), 155–203 (2006)
Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation 199(1-2), 172–199 (2005)
Jouannaud, J.-P., Rubio, A.: Polymorphic higher-order recursive path orderings. Journal of the ACM, 54(1) (2007)
Kamin, S., Levy, J.J.: Two generalizations of the recursive path ordering. Dept. of Computer Science, Univ. of Illinois, Urbana, IL (1980)
van de Pol, J.: Operational semantics of rewriting with priorities. Theoretical Computer Science 200(1-2), 289–312 (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Borralleras, C., Rubio, A. (2007). Orderings and Constraints: Theory and Practice of Proving Termination. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds) Rewriting, Computation and Proof. Lecture Notes in Computer Science, vol 4600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73147-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-73147-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73146-7
Online ISBN: 978-3-540-73147-4
eBook Packages: Computer ScienceComputer Science (R0)