{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T20:10:11Z","timestamp":1736453411847,"version":"3.32.0"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2005,5]]},"DOI":"10.1007\/s10817-005-9022-x","type":"journal-article","created":{"date-parts":[[2006,7,5]],"date-time":"2006-07-05T22:17:32Z","timestamp":1152137852000},"page":"325-363","source":"Crossref","is-referenced-by-count":43,"title":["Mechanically Proving Termination Using Polynomial Interpretations"],"prefix":"10.1007","volume":"34","author":[{"given":"Evelyne","family":"Contejean","sequence":"first","affiliation":[]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[]},{"given":"Ana Paula","family":"Tom\u00e1s","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,7,5]]},"reference":[{"key":"9022_CR1","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T. and Giesl, J.: Termination of term rewriting using dependency pairs, Theor. Comp. Sci. 236 (2000), 133-178.","journal-title":"Theor. Comp. Sci."},{"key":"9022_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F. and Nipkow, T.: Term Rewriting and All That, Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"9022_CR3","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. Ben Cherifa","year":"1987","unstructured":"Ben Cherifa, A. and Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation, Sci. Comput. Program. 9 (1987), 137\u2013159.","journal-title":"Sci. Comput. Program."},{"key":"9022_CR4","doi-asserted-by":"crossref","first-page":"21","DOI":"10.5802\/jtnb.104","volume":"6","author":"F. Bergeron","year":"1994","unstructured":"Bergeron, F., Berstel, J. and Brlek, S.: Efficient computation of addition chains, Journal de th\u00e9orie des nombres de Bordeaux 6 (1994), 21\u201338.","journal-title":"Journal de th\u00e9orie des nombres de Bordeaux"},{"issue":"3","key":"9022_CR5","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1016\/0196-6774(89)90036-9","volume":"10","author":"F. Bergeron","year":"1989","unstructured":"Bergeron, F., Berstel, J., Brlek, S. and Duboc, C.: Addition chains using continued fractions, J. Algorithms 10(3) (1989), 403\u2013412.","journal-title":"J. Algorithms"},{"key":"9022_CR6","unstructured":"Bleichenbacher, D. and Flammenkamp, A.: An Efficient Algorithm for Computing Shortest Addition Chains, http:\/\/wwwhomes.uni-bielefeld.de\/achim\/addition_chain.html , 1997."},{"issue":"1","key":"9022_CR7","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0956796800003877","volume":"11","author":"G. Bonfante","year":"2001","unstructured":"Bonfante, G., Cichon, A., Marion, J.-Y. and Touzet, H.: Algorithms with polynomial interpretation termination proof, J. Funct. Program. 11(1) (2001), 33\u201353.","journal-title":"J. Funct. Program."},{"key":"9022_CR8","doi-asserted-by":"crossref","unstructured":"Bos, J. and Coster, M.: Addition Chain Heuristics, in G. Brassard (ed.), Advances in Cryptology \u2013 Proc. Crypto '89, Vol. 435 of Lecture Notes in Computer Science, Santa Barbara, California, USA, pp. 400\u2013407, 1989.","DOI":"10.1007\/0-387-34805-0_37"},{"key":"9022_CR9","unstructured":"Cichon, E. A. and Touzet:, H.: An Ordinal Calculus for Proving Termination in Term Rewriting, in H. Kirchner (ed.), Proceedings 21st International Colloquium on Trees in Algebra and Programming, Vol. 1059 of Lecture Notes in Computer Science, Link\u00f6ping (Sweden), pp. 226\u2013240, 1996."},{"issue":"3","key":"9022_CR10","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0743-1066(95)00121-2","volume":"27","author":"P. Codognet","year":"1996","unstructured":"Codognet, P. and Diaz, D.: Compiling constraints in clp(FD), J. Log. Program. 27(3) (1996), 185\u2013226.","journal-title":"J. Log. Program."},{"key":"9022_CR11","unstructured":"Contejean, E., March\u00e9, C. Monate, B. and Urbain, X.: Proving Termination of Rewriting with CiME, in A. Rubio (ed.), Extended Abstracts of the 6th International Workshop on Termination, WST'03, 2003, pp. 71-73, http:\/\/cime.lri.fr ."},{"key":"9022_CR12","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.-P. and Urbain, X.: Mechanically proving termination using polynomial interpretations, Research Report 1382, LRI, 2004."},{"key":"9022_CR13","doi-asserted-by":"crossref","unstructured":"Courcelle, B.: Recursive Applicative Program Schemes, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B., North-Holland, Chapt. 9, 1990, pp. 459\u2013492.","DOI":"10.1016\/B978-0-444-88074-1.50014-7"},{"key":"9022_CR14","doi-asserted-by":"crossref","unstructured":"de Rooij, P.: Efficient exponentiation using precomputation and vector addition chains, in A. D. Santis (ed.), Advances in Cryptology \u2013 EUROCRYPT '94, Vol. 950 of Lecture Notes in Computer Science, Perugia, Italy, 1995, pp. 389\u2013399.","DOI":"10.1007\/BFb0053453"},{"key":"9022_CR15","unstructured":"Deplagne, \u00c9.: Sequent Calculus Viewed Modulo, in Catherine Pili\u00e8re (ed.), Proceedings of the Fifth ESSLLI Student Session, University of Birmingham, 2000, pp. 66\u201376."},{"issue":"3","key":"9022_CR16","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term rewriting systems, Theor. Comp. Sci. 17(3) (1982), 279\u2013301.","journal-title":"Theor. Comp. Sci."},{"key":"9022_CR17","doi-asserted-by":"crossref","unstructured":"Dershowitz, N.: Trees, Ordinals, and Termination, in M. C. Gaudel and J.-P. Jouannaud (eds.), 4th International Joint Conference on Theory and Practice of Software Development, Vol. 668 of Lecture Notes in Computer Science, Orsay, France, pp. 243\u2013250.","DOI":"10.1007\/3-540-56610-4_68"},{"key":"9022_CR18","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. and Jouannaud, J.-P.: Rewrite Systems, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B., North-Holland, 1990, pp. 243\u2013320.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"1","key":"9022_CR19","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1137\/0209011","volume":"9","author":"D. Dobkin","year":"1980","unstructured":"Dobkin, D. and Lipton, R. J.: Addition chain methods for the evaluation of specific polynomials, SIAM J. Comput. 9(1) (1980), 121\u2013125.","journal-title":"SIAM J. Comput."},{"issue":"3","key":"9022_CR20","doi-asserted-by":"crossref","first-page":"638","DOI":"10.1137\/0210047","volume":"10","author":"P. J. Downey","year":"1981","unstructured":"Downey, P. J., Leong, B. L. and Sethi, R.: Computing sequences with addition chains, SIAM J. Comput. 10(3) (1981), 638\u2013646.","journal-title":"SIAM J. Comput."},{"key":"9022_CR21","doi-asserted-by":"crossref","unstructured":"Fissore, O., Gnaedig, I. and Kirchner, H.: CARIBOO: An Induction Based Proof Tool for Termination with Strategies, in Proc. Fourth International Conference on Principles and Practice of Declarative Programming (PPDP), Pittsburgh, USA, 2002, pp. 62\u201373, http:\/\/www.loria.fr\/~fissore\/CARIBOO .","DOI":"10.1145\/571157.571164"},{"key":"9022_CR22","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Generating Polynomial Orderings for Termination Proofs, in J. Hsiang (ed.), 6th International Conference on Rewriting Techniques and Applications, Vol. 914 of Lecture Notes in Computer Science, Kaiserslautern, Germany, 1995, pp. 426\u2013431.","DOI":"10.1007\/3-540-59200-8_77"},{"issue":"2","key":"9022_CR23","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl, J., Arts, T. and Ohlebusch, E.: Modular termination proofs for rewriting using dependency Pairs, J. Symb. Comput. 34(2) (2002), 21\u201358.","journal-title":"J. Symb. Comput."},{"key":"9022_CR24","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S.: AProVE: A System for Proving Termination, in A. Rubio (ed.), Extended Abstracts of the 6th International Workshop on Termination, WST'03, 2003, pp. 68\u201370, http:\/\/www-i2.informatik.rwth-aachen.de\/AProVE ."},{"key":"9022_CR25","doi-asserted-by":"crossref","unstructured":"Gramlich, B. and Lucas, S.: Simple Termination of Context-Sensitive Rewriting, in B. Fischer and E. Visser (eds.), in Proc. 3rd ACM Sigplan Workshop on Rule-Based Programming, RULE'02, Pittsburgh, USA, 2002, pp. 29\u201341.","DOI":"10.1145\/570186.570189"},{"key":"9022_CR26","unstructured":"Hirokawa, N. and Middeldorp, A.: Approximating Dependency Graphs without using Tree Automata Techniques, in A. Rubio (ed.), Extended Abstracts of the 6th International Workshop on Termination, WST'03, 2003, pp. 8\u201310, Technical Report DSIC II\/15\/03, Universidad Polit\u00e9cnica de Valencia, Spain."},{"key":"9022_CR27","doi-asserted-by":"crossref","unstructured":"Hirokawa, N. and Middeldorp, A.: Tsukuba Termination Tool, in R. Nieuwenhuis (ed.), 14th International Conference on Rewriting Techniques and Applications, Vol. 2706 of Lecture Notes in Computer Science, Valencia, Spain, 2003, pp. 311\u2013320.","DOI":"10.1007\/3-540-44881-0_22"},{"key":"9022_CR28","doi-asserted-by":"crossref","unstructured":"Hofbauer, D. and Lautermann, C.: Termination Proofs and the Length of Derivations, in N. Dershowitz (ed.), Rewriting Techniques and Applications, Vol. 355 of Lecture Notes in Computer Science, Chapel Hill, USA, 1989, pp. 167\u2013177.","DOI":"10.1007\/3-540-51081-8_107"},{"issue":"1","key":"9022_CR29","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1005983105493","volume":"21","author":"H. Hong","year":"1998","unstructured":"Hong, H. and Jaku\u0161, D.: Testing positiveness of polynomials, J. Autom. Reason. 21(1) (1998), 23\u201338.","journal-title":"J. Autom. Reason."},{"key":"9022_CR30","doi-asserted-by":"crossref","unstructured":"Jaffar, J. and Lassez, J.-L.: Constraint Logic Programming, in Proceedings of the 14th ACM Conference on Principles of Programming Languages, Munich, Germany, 1987, pp. 111\u2013119.","DOI":"10.1145\/41625.41635"},{"key":"9022_CR31","unstructured":"Klop, J. W.: Term rewriting systems, in S. Abramsky, D. Gabbay, and T. Maibaum (eds.), Handbook of Logic in Computer Science, Vol. 2., Clarendon, 1992, pp. 1\u2013116."},{"key":"9022_CR32","unstructured":"Knuth, D. E.: The art of computer programming, 2nd edn, Vol. 2., Addison-Wesley, 1981."},{"key":"9022_CR33","doi-asserted-by":"crossref","unstructured":"Kusakari, K., Nakamura, M. and Toyama, Y.: Argument Filtering Transformation, in G. Nadathur (ed.), Principles and Practice of Declarative Programming, International Conference PPDP'99, Vol. 1702 of Lecture Notes in Computer Science, Paris, 1999, pp. 47\u201361.","DOI":"10.1007\/10704567_3"},{"key":"9022_CR34","unstructured":"Lang, S.: Algebra, 3rd edn, Addison-Wesley, 1993."},{"key":"9022_CR35","unstructured":"Lankford, D. S.: On proving term rewriting systems are Noetherian, Technical Report MTP-3, Mathematics Department, Louisiana Tech. Univ., 1979. Available at http:\/\/perso.ens-lyon.fr\/pierre.lescanne\/not_accessible.html ."},{"key":"9022_CR36","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF01214624","volume":"7","author":"P. Lescanne","year":"1995","unstructured":"Lescanne, P.: Elementary interpretations in proofs of termination, Form. Asp. Comput. 7 (1995), 77\u201390.","journal-title":"Form. Asp. Comput."},{"key":"9022_CR37","doi-asserted-by":"crossref","unstructured":"Lucas, S.: Termination of (Canonical) Context-Sensitive Rewriting, in S. Tison (ed.), 13th International Conference on Rewriting Techniques and Applications, Vol. 2378 of Lecture Notes in Computer Science, Copenhagen, Denmark, 2002, pp. 296\u2013310.","DOI":"10.1007\/3-540-45610-4_21"},{"key":"9022_CR38","doi-asserted-by":"crossref","unstructured":"Lucas, S.: 2003, Mu-term, A Tool for Proving Termination of Rewriting with Replacement Restrictions, 2002, Available at http:\/\/www.dsic.upv.es\/~slucas\/csr\/termination\/muterm\/ .","DOI":"10.1007\/978-3-540-25979-4_14"},{"key":"9022_CR39","unstructured":"Manna, Z. and Ness, S.: On the termination of Markov algorithms, in Proc. Third Hawaii International Conference on Systems Sciences, Honolulu, HI, 1970, pp. 789\u2013792. http:\/\/perso.ens-lyon.fr\/pierre.lescanne\/not_accessible.html ."},{"issue":"2","key":"9022_CR40","first-page":"354","volume":"11","author":"Y. V. Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y. V.: Enumerable sets are diophantine, Sov. Math. (Dokladi) 11(2) (1970), 354\u2013357.","journal-title":"Sov. Math. (Dokladi)"},{"key":"9022_CR41","unstructured":"Matiyasevich, Y. V.: Hilbert's Tenth Problem, MIT Press, 1993."},{"key":"9022_CR42","doi-asserted-by":"crossref","unstructured":"Middeldorp, A.: Approximating Dependency Graphs using Tree Automata Techniques, in R. Gor\u00e9, A. Leitsch, and T. Nipkow (eds.), International Joint Conference on Automated Reasoning, Vol. 2083 of Lecture Notes in Artificial Intelligence, Siena, Italy, 2001, pp. 593\u2013610.","DOI":"10.1007\/3-540-45744-5_49"},{"issue":"2","key":"9022_CR43","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"F. L. Morris","year":"1984","unstructured":"Morris, F. L. and Jones, C. B.: An early program proof by Alan Turing, Ann. Hist. Comput. 6(2) (1984), 139\u2013143.","journal-title":"Ann. Hist. Comput."},{"issue":"1","key":"9022_CR44","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0196-6774(81)90003-1","volume":"2","author":"J. Olivos","year":"1981","unstructured":"Olivos, J.: On vectorial addition chains, J. Algorithms 2(1) (1981), 13\u201321.","journal-title":"J. Algorithms"},{"key":"9022_CR45","first-page":"2","volume":"13","author":"C. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C. and Knuth, D.: Duality in addition chains, Bulletin of the EACTS 13 (1981), 2\u20133.","journal-title":"Bulletin of the EACTS"},{"issue":"2","key":"9022_CR46","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1137\/0209022","volume":"9","author":"N. Pippenger","year":"1980","unstructured":"Pippenger, N.: On the evaluation of powers and monomials, SIAM J. Comput. 9(2) (1980), 230\u2013250.","journal-title":"SIAM J. Comput."},{"key":"9022_CR47","doi-asserted-by":"crossref","unstructured":"Rosu, G. and Viswanathan, M.: Testing Extended Regular Language Membership Incrementally by Rewriting, in R. Nieuwenhuis (ed.), 14th International Conference on Rewriting Techniques and Applications, Vol. 2706 of Lecture Notes in Computer Science, 2003, Valencia, Spain.","DOI":"10.1007\/3-540-44881-0_35"},{"key":"9022_CR48","unstructured":"Rouyer, J.: A method to decide whether a multivariate integral polynomial admits roots in a product of closed intervals of R, Research Report 91-R-183, Centre de Recherche en Informatique de Nancy, 1991."},{"key":"9022_CR49","doi-asserted-by":"crossref","unstructured":"Rouyer, J.: Preuves de terminaison de syst\u00e8mes de r\u00e9\u00e9criture fond\u00e9es sur les interpr\u00e9tations polynomiales. Une m\u00e9thode bas\u00e9e sur le th\u00e9or\u00e8me de Sturm, R.A.I.R.O. 25(2) (1991), 157\u2013169.","DOI":"10.1051\/ita\/1991250201571"},{"key":"9022_CR50","doi-asserted-by":"crossref","unstructured":"Sauerbrey, J. and Dietel, A.: Resource Requirements for the Application of Addition Chains in Modulo Exponentiation, in R. Rueppel (ed.), Advances in Cryptology \u2013 EUROCRYPT '92, Vol. 658 of Lecture Notes in Computer Science, Balatonf\u00fcred, Hungary, 1993, pp. 174\u2013182.","DOI":"10.1007\/3-540-47555-9_15"},{"issue":"1","key":"9022_CR51","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(75)90008-0","volume":"1","author":"A. Schonhage","year":"1975","unstructured":"Schonhage, A.: A lower bound for the length of addition chains, Theor. Comp. Sci. 1(1) (1975), 1\u201312.","journal-title":"Theor. Comp. Sci."},{"key":"9022_CR52","doi-asserted-by":"crossref","unstructured":"Steinbach, J.: Proving Polynomials Positive, in R. Shyamasundar (ed.), Foundations of Software Technology and Theoretical Computer Science, Vol. 652 of Lecture Notes in Computer Science, New Delhi, India, 1992, pp. 191\u2013202.","DOI":"10.1007\/3-540-56287-7_105"},{"key":"9022_CR53","unstructured":"Terese: in M. Bezem, J. W. Klop, and R. de Vrijer, (eds.), 2003, Term Rewriting Systems, Vol. 55 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1992, http:\/\/www.cs.vu.nl\/~terese\/ ."},{"key":"9022_CR54","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, University of California Press, Berkeley, CA, 1951."},{"key":"9022_CR55","unstructured":"Turing, A. M.: Checking a large routine, in Report of a Conference on High Speed Automatic Calculing Machines, Cambridge, 1949, pp. 67\u201369."},{"key":"9022_CR56","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF03177743","volume":"32","author":"X. Urbain","year":"2004","unstructured":"Urbain, X.: Modular and incremental automated termination proofs, J. Autom. Reason. 32, (2004) 315\u2013355.","journal-title":"J. Autom. Reason."},{"key":"9022_CR57","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0196-6774(91)90005-J","volume":"12","author":"H. Zantema","year":"1991","unstructured":"Zantema, H.: Minimizing Sums of Addition Chains, J. Algorithms 12 (1991), 281\u2013307.","journal-title":"J. Algorithms"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9022-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-9022-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9022-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T19:29:55Z","timestamp":1736450995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-9022-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["9022"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-9022-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}