{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T18:35:01Z","timestamp":1723487701447},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T00:00:00Z","timestamp":1141603200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T00:00:00Z","timestamp":1141603200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[2006,4]]},"DOI":"10.1007\/s00200-005-0189-5","type":"journal-article","created":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T09:26:58Z","timestamp":1141637218000},"page":"49-73","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting"],"prefix":"10.1007","volume":"17","author":[{"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,3,6]]},"reference":[{"key":"189_CR1","first-page":"133","volume":"236","author":"Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs Theoretical Comp. Sci. 236, 133\u2013178 (2000)","journal-title":"Sci."},{"key":"189_CR2","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"Basu","year":"6","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: On the Combinatorial and Algebraic Complexity of Quantifier Elimination. J. ACM 43(6), 1002\u20131045 (1996)","journal-title":"J. ACM"},{"key":"189_CR3","doi-asserted-by":"crossref","unstructured":"Beeson, M.J.: Foundations of Constructive Mathematics. Springer-Verlag, Berlin, 1985","DOI":"10.1007\/978-3-642-68952-9"},{"key":"189_CR4","doi-asserted-by":"crossref","unstructured":"Bonfante, G., Cichon, A., Marion, J.-Y., Touzet, H.: Complexity classes and rewrite systems with polynomial interpretation. In Gottlob, G., Grandjean, E., Seyr, K. (eds.) Proc. of 12th International Workshop on Computer Science Logic, CSL '98, LNCS 1584, 372\u2013384 (1998)","DOI":"10.1007\/10703163_25"},{"key":"189_CR5","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0956796800003877","volume":"11","author":"Bonfante","year":"1","unstructured":"Bonfante, G., Cichon, A., Marion, J.-Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Functional Prog. 11(1), 33\u201353 (2001)","journal-title":"J. Functional Prog."},{"key":"189_CR6","doi-asserted-by":"crossref","unstructured":"Bonfante, G., Marion, J.-Y., Moyen, J.Y.: Quasi-interpretations and Small Space Bounds. In: Giesl, J. (ed.) Proc. of 16th International Conference on Rewriting Techniques and Applications, RTA'05, LNCS 3467, 150\u2013164 (2005)","DOI":"10.1007\/978-3-540-32033-3_12"},{"key":"189_CR7","doi-asserted-by":"crossref","unstructured":"Bochnak, J., Coste, M., Roy, M-F.: Real Algebraic Geometry. Springer-Verlag, Berlin, 1998","DOI":"10.1007\/978-3-662-03718-8"},{"key":"189_CR8","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"Cherifa","year":"2","unstructured":"ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming 9(2), 137\u2013160 (1987)","journal-title":"Science of Computer Programming"},{"key":"189_CR9","doi-asserted-by":"crossref","unstructured":"Cichon, A., Lescanne, P.: Polynomial interpretations and the complexity of algorithms. In Kapur, D. (ed.) Proc. of 11th International Conference on Automated Deduction, CADE'92, LNAI 607, 139\u2013147, Springer-Verlag, Berlin, 1992","DOI":"10.1007\/3-540-55602-8_161"},{"key":"189_CR10","doi-asserted-by":"crossref","unstructured":"Cox, D., Little, J., O'Shea, D.: Ideals, Varieties, and Algorithms. Springer-Verlag, Berlin, 1997","DOI":"10.1007\/978-1-4757-2693-0"},{"key":"189_CR11","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s002000000044","volume":"12","author":"Cropper","year":"2001","unstructured":"Cropper, N., Martin, U.: The Classification of Polynomial Orderings on Monadic Terms. Applicable Algebra in Engineering, Commun. Comput. 12, 197\u2013226 (2001)","journal-title":"Applicable Algebra in Engineering, Commun. Comput."},{"key":"189_CR12","unstructured":"Contejean, E., March\u00e9, C., Monate, B., Urbain, X.: Proving termination of rewriting with CiME. In Rubio, A. (ed.) Proc. of 6th International Workshop on Termination, WST'03, Technical Report DSIC II\/15\/03, Valencia, Spain, 2003. Available at http:\/\/cime.lri.fr pp 71\u201373"},{"key":"189_CR13","doi-asserted-by":"crossref","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Automated Reasoning, to appear, 2005","DOI":"10.1007\/s10817-005-9022-x"},{"key":"189_CR14","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier Elimination for Real Closed Fields by Cyllindrical Algebraic Decomposition. In Barkhage, H. (ed.) Proc. of 2nd GI Conference on Automata Theory and Formal Languages, LNCS 33, 134\u2013183, Springer-Verlag, Berlin, 1975","DOI":"10.1007\/3-540-07407-4_17"},{"key":"189_CR15","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/0304-3975(92)90022-8","volume":"103","author":"Dauchet","year":"2","unstructured":"Dauchet, M.: Simulation of Turing machines by a regular rewrite rule. Theor. Comp. Sci. 103(2), 409\u2013420 (1992)","journal-title":"Theor. Comp. Sci."},{"key":"189_CR16","doi-asserted-by":"crossref","unstructured":"Dedekind, R.: Theory of Algebraic Integers. Cambridge University Press, 1996","DOI":"10.1017\/CBO9780511623639"},{"key":"189_CR17","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","volume":"9","author":"Dershowitz","year":"5","unstructured":"Dershowitz, N.: A note on simplification orderings. Information Processing Letters 9(5), 212\u2013215 (1979)","journal-title":"Information Processing Letters"},{"key":"189_CR18","unstructured":"Dershowitz, N.: Personal communication. March 2004"},{"key":"189_CR19","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Generating Polynomial Orderings for Termination Proofs. In Hsiang, J. (ed.) Proc. of 6th International Conference on Rewriting Techniques and Applications, RTA'95, LNCS 914, 426\u2013431, Springer-Verlag, Berlin, 1995","DOI":"10.1007\/3-540-59200-8_77"},{"key":"189_CR20","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Generating Polynomial Orderings for Termination Proofs. Technical Report IBN 95\/23, Technische Hochschule Darmstadt, 1995 pp. 18","DOI":"10.1007\/3-540-59200-8_77"},{"key":"189_CR21","unstructured":"Giesl, J.: POLO - A System for Termination Proofs using Polynomial Orderings. Technical Report IBN 95\/24, Technische Hochschule Darmstadt, 1995 pp. 27"},{"key":"189_CR22","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated Termination Proofs with AProVE. In van Oostrom, V. (ed.) Proc. of 15h International Conference on Rewriting Techniques and Applications, RTA'04, LNCS 3091, 210\u2013220, Springer-Verlag, Berlin, 2004. Available at http:\/\/www-i2.informatik.rwth-aachen.de\/AProVE","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"189_CR23","doi-asserted-by":"crossref","unstructured":"Hofbauer, D.: Termination Proofs by Context-Dependent Interpretations. In Middeldorp, A. (ed.) Proc. of 12th International Conference on Rewriting Techniques and Applications, RTA'01, LNCS 2051, 108\u2013121 Springer-Verlag, Berlin, 2001","DOI":"10.1007\/3-540-45127-7_10"},{"key":"189_CR24","doi-asserted-by":"crossref","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In N. Dershowitz, editor, Proc. of the 3rd International Conference on Rewriting Techniques and Applications, RTA'89, LNCS 355, 167\u2013177 Springer-Verlag, Berlin, 1989","DOI":"10.1007\/3-540-51081-8_107"},{"key":"189_CR25","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool. In Giesl, J (ed.) Proc. of 16th International Conference on Rewriting Techniques and Applications, RTA'05, LNCS 3467, 175\u2013184, 2005. Available at http:\/\/cl2-informatik.uibk.ac.at.","DOI":"10.1007\/978-3-540-32033-3_14"},{"key":"189_CR26","unstructured":"Iturriaga, R.: Contributions to mechanical mathematics. PhD Thesis, Carnegie-Mellon University, Pittsburgh, PA, USA, 1967"},{"key":"189_CR27","unstructured":"Lang, S.: Algebra. Springer-Verlag, Berlin, 2004"},{"key":"189_CR28","unstructured":"Lankford, D.S.: On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA, 1979"},{"key":"189_CR29","doi-asserted-by":"crossref","unstructured":"Lucas, S. MU-TERM: A Tool for Proving Termination of Context-Sensitive Rewriting In van Oostrom, V. (ed.) Proc. of 15h International Conference on Rewriting Techniques and Applications, RTA'04, LNCS 3091 200\u2013209, Springer-Verlag, Berlin, 2004. Available at http:\/\/www.dsic.upv.es\/~slucas\/csr\/termination\/muterm","DOI":"10.1007\/978-3-540-25979-4_14"},{"issue":"3","key":"189_CR30","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1051\/ita:2005029","volume":"39","author":"S. Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications, 39(3):547\u2013586, 2005","journal-title":"RAIRO Theoretical Informatics and Applications"},{"key":"189_CR31","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In Proc. of the Third Hawaii International Conference on System Science, 1970 pp 789\u2013792"},{"key":"189_CR32","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/S0890-5401(03)00011-7","volume":"183","author":"Marion","year":"1","unstructured":"Marion, J.Y.: Analysing the implicit complexity of programs. Information and Computation 183(1), 2\u201318 (2003)","journal-title":"Information and Computation"},{"key":"189_CR33","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1006\/jsco.1999.0333","volume":"29","author":"Martin","year":"2000","unstructured":"Martin, U., Shand, D.: Invariants, Patterns and Weights for Ordering Terms. J. Symbolic Computation 29, 921\u2013957 (2000)","journal-title":"J. Symbolic Computation"},{"key":"189_CR34","first-page":"354","volume":"11","author":"Matijasevich","year":"2","unstructured":"Matijasevich, Y.: Enumerable sets are Diophantine. Soviet Mathematics (Dokladi) 11(2), 354\u2013357 (1970)","journal-title":"Soviet Mathematics (Dokladi)"},{"key":"189_CR35","unstructured":"Rouyer, J.: Calcul formel en g\u00e9om\u00e9trie alg\u00e9brique r\u00e9elle appliqu\u00e9 \u00e0 la terminaison des syst\u00e8mes de r\u00e9\u00e9criture. Universit\u00e9 de Nancy, I, PhD Thesis, 1991"},{"key":"189_CR36","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1016\/0304-3975(94)90111-2","volume":"135","author":"Scott","year":"2","unstructured":"Scott, E.A.: Weights for total division orderings on strings. Theor. Comp. Sci. 135(2), 345\u2013359 (1994)","journal-title":"Theor. Comp. Sci."},{"key":"189_CR37","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","volume":"49","author":"Steinbach","year":"1994","unstructured":"Steinbach, J.: Generating Polynomial Orderings. Information Processing Letters 49, 85\u201393 (1994)","journal-title":"Information Processing Letters"},{"key":"189_CR38","unstructured":"Steinbach, J.: Termination of Rewriting - Extensions, Comparison and Automatic Generation of Simplification Orderings. PhD Thesis. Fachbereich Informatik, Universit\u00e4t Kaiserslautern, Jan 1994"},{"key":"189_CR39","doi-asserted-by":"crossref","unstructured":"Tarski, A:. A Decision Method for Elementary Algebra and Geometry. Second Edition. University of California Press, Berkeley, 1951","DOI":"10.1525\/9780520348097"},{"key":"189_CR40","unstructured":"TeReSe, editor, Term Rewriting Systems, Cambridge University Press, 2003"},{"key":"189_CR41","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved Modular Termination Proofs Using Dependency Pairs. In Basin, D.A., Rusinowitch, M. (eds.) Proc. of 2nd International Joint Conference on Automated Reasoning, IJCAR'04, LNCS 3097, 75\u201390, Springer-Verlag, Berlin, 2004","DOI":"10.1007\/978-3-540-25984-8_4"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-005-0189-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00200-005-0189-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-005-0189-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-005-0189-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,14]],"date-time":"2022-05-14T06:34:43Z","timestamp":1652510083000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00200-005-0189-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,6]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["189"],"URL":"https:\/\/doi.org\/10.1007\/s00200-005-0189-5","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,3,6]]},"assertion":[{"value":"11 March 2005","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 June 2005","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 March 2006","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}