Abstract
Polynomial interpretations are a standard technique used in almost all tools for proving termination of term rewrite systems (TRSs) automatically. Traditionally, one applies interpretations with polynomials over the naturals. But recently, it was shown that interpretations with polynomials over the rationals can be significantly more powerful. However, searching for such interpretations is considerably more difficult than for natural polynomials. Moreover, while there exist highly efficient SAT-based techniques for finding natural polynomials, no such techniques had been developed for rational polynomials yet. In this paper, we tackle the two main problems when applying rational polynomial interpretations in practice: (1) We develop new criteria to decide when to use rational instead of natural polynomial interpretations. (2) Afterwards, we present SAT-based methods for finding rational polynomial interpretations and evaluate them empirically.
C. Fuhs, J. Giesl, C. Otto, and P. Schneider-Kamp were supported by the DAAD under grant D/06/12785 and by the DFG under grant GI 274/5-2. S. Lucas and R. Navarro-Marset were partially supported by the EU (FEDER) and the Spanish MEC, under grants TIN 2007-68093-C02-02 and HA 2006-0007. R. Navarro-Marset was partially supported by the Spanish MEC under FPU grant AP2006-026.
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., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Contejean, E., Marché, C., Monate, B., Urbain, X.: CiME, http://cime.lri.fr
Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning 34(4), 325–363 (2005)
Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation 3, 69–116 (1987)
Endrullis, J.: Jambox, http://joerg.endrullis.de
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 574–588. Springer, Heidelberg (2006)
Fuhs, C., Giesl, J., Middeldorp, A., Thiemann, R., Schneider-Kamp, P., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007)
Gebhardt, A., Hofbauer, D., Waldmann, J.: Matrix Evolutions. In: Proc. WST 2007 (2007)
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)
Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)
Hong, H., Jakuš, D.: Testing positiveness of polynomials. Journal of Automated Reasoning 21(1), 23–38 (1998)
Lucas, S.: MU-TERM: a tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 200–209. Springer, Heidelberg (2004)
Lucas, S.: Polynomials over the reals in proofs of termination: From theory to practice. RAIRO Theoretical Informatics and Applications 39(3), 547–586 (2005)
Lucas, S.: On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. Applicable Algebra in Engineering, Communication and Computing 17(1), 49–73 (2006)
Lucas, S.: Practical use of polynomials over the reals in proofs of termination. In: Proc. PPDP 2007, pp. 39–50. ACM Press, New York (2007)
Marché, C., Zantema, H.: The termination competition. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 303–313. Springer, Heidelberg (2007)
Thiemann, R., Middeldorp, A.: Innermost termination of rewrite systems by labeling. In: Proc. WRS 2007. ENTCS 204, pp. 3–19 (2008)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fuhs, C., Navarro-Marset, R., Otto, C., Giesl, J., Lucas, S., Schneider-Kamp, P. (2008). Search Techniques for Rational Polynomial Orders. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds) Intelligent Computer Mathematics. CICM 2008. Lecture Notes in Computer Science(), vol 5144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85110-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-85110-3_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85109-7
Online ISBN: 978-3-540-85110-3
eBook Packages: Computer ScienceComputer Science (R0)