Abstract
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. We show how polynomial interpretations with negative coefficients, like x–1 for a unary function symbol or x–y for a binary function symbol, can be used to extend the class of rewrite systems that can be automatically proved terminating.
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)
Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming 9, 137–159 (1987)
Contejean, E., Marché, C., Monate, B., Urbain, X.: CiME version 2 (2000), Available at http://cime.lri.fr/
Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI (2004)
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., Hoot, C.: Natural termination. Theoretical Computer Science 142(2), 179–207 (1995)
Giesl, J.: Generating polynomial orderings for termination proofs. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 426–431. Springer, Heidelberg (1995)
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.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)
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.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Proc. 7th Internation Workshop on Termination, Technical Report AIB-2004-07, RWTH Aachen, pp. 59–62 (2004)
Hong, H., Jakuš, D.: Testing positiveness of polynomials. Journal of Automated Reasoning 21, 23–28 (1998)
Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)
Lucas, S.: Polynomials for proving termination of context-sensitive rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 318–332. Springer, Heidelberg (2004)
Lucas, S.: Polynomials over the reals in proof of termination. In: Proc. 7th Internation Workshop on Termination, Technical Report AIB-2004-07, RWTH Aachen, pp. 39–42 (2004)
Steinbach, J.: Generating polynomial orderings. Information Processing Letters 49, 85–93 (1994)
Steinbach, J., Kühler, U.: Check your ordering – termination proofs and open problems. Technical Report SR-90-25, Universität Kaiserslautern (1990)
Terese. 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: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 75–90. Springer, Heidelberg (2004)
Urbain, X.: Modular & incremental automated termination proofs. Journal of Automated Reasoning (2004) (to appear)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)
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). Polynomial Interpretations with Negative Coefficients. In: Buchberger, B., Campbell, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2004. Lecture Notes in Computer Science(), vol 3249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30210-0_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-30210-0_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23212-4
Online ISBN: 978-3-540-30210-0
eBook Packages: Springer Book Archive