{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T22:52:16Z","timestamp":1791413536973,"version":"4.3.3"},"reference-count":44,"publisher":"EDP Sciences","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RAIRO-Theor. Inf. Appl."],"published-print":{"date-parts":[[2005,7]]},"DOI":"10.1051\/ita:2005029","type":"journal-article","created":{"date-parts":[[2005,7,4]],"date-time":"2005-07-04T16:10:40Z","timestamp":1120493440000},"page":"547-586","source":"Crossref","is-referenced-by-count":34,"title":["Polynomials over the reals in proofs of termination : from theory to practice"],"prefix":"10.1051","volume":"39","author":[{"given":"Salvador","family":"Lucas","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"250","published-online":{"date-parts":[[2005,7,15]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"Arts","year":"2000","journal-title":"Theor. Comput. Sci."},{"key":"R2","unstructured":"T. Arts and J. Giesl,A collection of examples for termination of term rewriting using dependency pairs. Technical report, AIB-2001-09, RWTH Aachen, Germany (2001)."},{"key":"R3","unstructured":"J. Bochnak, M. Coste and M-F. Roy,G\u00e9om\u00e9trie alg\u00e9braique r\u00e9elle. Springer-Verlag, Berlin (1987)."},{"key":"R4","first-page":"314","volume":"2392","author":"Borralleras","year":"2002","journal-title":"LNAI"},{"key":"R5","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow,Term Rewriting and All That.Cambridge University Press (1998).","DOI":"10.1017\/CBO9781139172752"},{"key":"R6","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"ben Cherifa","year":"1987","journal-title":"Sci. Comput. Program."},{"key":"R7","doi-asserted-by":"crossref","unstructured":"A. Cichon and P. Lescanne, Polynomial interpretations and the complexity of algorithms, inProc. of 11th International Conference on Automated Deduction, CADE'92, edited by D. Kapur, Springer-Verlag, Berlin. LNAI607(1992) 139\u2013147.","DOI":"10.1007\/3-540-55602-8_161"},{"key":"R8","unstructured":"E. Contejean and C. March\u00e9, B. Monate and X. Urbain, Proving termination of rewriting with CiME, inProc. of 6th International Workshop on Termination, WST'03, edited by A. Rubio, Technical Report DSIC II\/15\/03, Valencia, Spain (2003) 71\u201373. Available at http:\/\/cime.lri.fr"},{"key":"R9","unstructured":"E. Contejean, C. March\u00e9, A.-P. Tom\u00e1s and X. Urbain,Mechanically proving termination using polynomial interpretations.Research Report 1382, LRI, Universit\u00e9 de Paris-Sud (2004)."},{"key":"R10","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1016\/0304-3975(92)90022-8","volume":"103","author":"Dauchet","year":"1992","journal-title":"Theor. Comput. Sci."},{"key":"R11","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","volume":"9","author":"Dershowitz","year":"1979","journal-title":"Inform. Proc. Lett."},{"key":"R12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theor. Comput. Sci."},{"key":"R13","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. Symbol. Comput."},{"key":"R14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0304-3975(91)90040-9","volume":"83","author":"Dershowitz","year":"1991","journal-title":"Theor. Comput. Sci."},{"key":"R15","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/j.ipl.2004.10.005","volume":"93","author":"Fern\u00e1ndez","year":"2005","journal-title":"Inform. Proc. Lett."},{"key":"R16","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"38","author":"Giesl","year":"2002","journal-title":"J. Symbol. Comput."},{"key":"R17","unstructured":"A. Geser,Relative Termination.Ph.D. Thesis. Fakult\u00e4t f\u00fcr Mathematik und Informatik. Universit\u00e4t Passau (1990)."},{"key":"R18","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-59200-8_77","volume":"914","author":"Giesl","year":"1995","journal-title":"Lect. Notes Comput. Sci."},{"key":"R19","doi-asserted-by":"crossref","unstructured":"B. Gramlich and S. Lucas, Simple termination of context-sensitive rewriting, inProc. of 3rd ACM SIGPLAN Workshop on Rule-based Programming, RULE'02ACM Press, New York (2002) 29\u201341.","DOI":"10.1145\/570186.570189"},{"key":"R20","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1017\/S0956796803004945","volume":"14","author":"Giesl","year":"2004","journal-title":"J. Funct. Program."},{"key":"R21","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume":"3091","author":"Giesl","year":"2004","journal-title":"Lect. Notes. Comput. Sci."},{"key":"R22","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1005983105493","volume":"21","author":"Hong","year":"1998","journal-title":"J. Automated Reasoning"},{"key":"R23","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-51081-8_107","volume":"355","author":"Hofbauer","year":"1989","journal-title":"Lect. Notes Comput. Sci."},{"key":"R24","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-540-25979-4_18","volume":"3091","author":"Hirokawa","year":"2004","journal-title":"Lect. Notes. Comput. Sci."},{"key":"R25","first-page":"185","volume":"3249","author":"Hirokawa","year":"2004","journal-title":"LNAI"},{"key":"R26","unstructured":"N. Hirokawa and A. Middeldorp, Tyrolean Termination Tool, inProc. of 16th International Conference on Rewriting Techniques and Applications, RTA'05, edited by J. Giesl.Lect. Notes. Comput. Sci., to appear (2005). Available at http:\/\/cl2-informatik.uibk.ac.at"},{"key":"R27","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/3-540-45127-7_10","volume":"2051","author":"Hofbauer","year":"2001","journal-title":"Lect. Notes Comput. Sci."},{"key":"R28","doi-asserted-by":"crossref","unstructured":"D.E. Knuth and P.E. Bendix, Simple Word Problems in Universal Algebra, inComputational Problems in Abstract Algebra, edited by J. Leech, Pergamon Press (1970) 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"R29","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/10704567_3","volume":"1702","author":"Kusakari","year":"1999","journal-title":"Lect. Notes Comput. Sci."},{"key":"R30","unstructured":"D.S. Lankford,On proving term rewriting systems are noetherian.Technical Report, Louisiana Technological University, Ruston, LA (1979)."},{"key":"R31","unstructured":"S. Lang,Algebra. Springer-Verlag, Berlin (2004)."},{"key":"R32","first-page":"1","volume":"1998","author":"Lucas","year":"1998","journal-title":"J. Funct. Logic Program."},{"key":"R33","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0890-5401(02)93176-7","volume":"178","author":"Lucas","year":"2002","journal-title":"Inform. Comput."},{"key":"R34","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-45610-4_21","volume":"2378","author":"Lucas","year":"2002","journal-title":"Lect. Notes Comput. Sci."},{"key":"R35","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-25979-4_14","volume":"3091","author":"Lucas","year":"2004","journal-title":"Lect. Notes Comput. Sci."},{"key":"R36","unstructured":"S. Lucas,Proving Termination of Context-Sensitive Rewriting by Transformation.Technical Report DSIC-II\/18\/04, DSIC, Universidad Polit\u00e9cnica de Valencia (2004)."},{"key":"R37","doi-asserted-by":"crossref","unstructured":"E. Ohlebusch,Advanced Topics in Term Rewriting. Springer-Verlag, Berlin (2002).","DOI":"10.1007\/978-1-4757-3661-8"},{"key":"R38","unstructured":"J.P. Rellier, CON'FLEX. INRA, France, 1996. Main URL: http:\/\/www.inra.fr\/bia\/T\/rellier\/Logiciels\/conflex\/welcome.html"},{"key":"R39","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","volume":"49","author":"Steinbach","year":"1994","journal-title":"Inform. Proc. Lett."},{"key":"R40","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/FI-1995-24123","volume":"24","author":"Steinbach","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"R41","doi-asserted-by":"crossref","unstructured":"A. Tarski,A Decision Method for Elementary Algebra and Geometry.Second Edition. University of California Press, Berkeley (1951).","DOI":"10.1525\/9780520348097"},{"key":"R42","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-540-25984-8_4","volume":"3097","author":"Thiemann","year":"2004","journal-title":"Lect. Notes Comput. Sci."},{"key":"R43","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-62950-5_69","volume":"1232","author":"Zantema","year":"1997","journal-title":"Lect. Notes Comput. Sci."},{"key":"R44","unstructured":"H. Zantema, Termination, inTerm Rewriting Systems, Chap. 6. edited by TeReSe, Cambridge University Press (2003)."}],"container-title":["RAIRO - Theoretical Informatics and Applications"],"original-title":[],"link":[{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita:2005029\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,12]],"date-time":"2021-07-12T23:54:11Z","timestamp":1626134051000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita:2005029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":44,"journal-issue":{"issue":"3"},"alternative-id":["ita0508"],"URL":"https:\/\/doi.org\/10.1051\/ita:2005029","relation":{},"ISSN":["0988-3754","1290-385X"],"issn-type":[{"value":"0988-3754","type":"print"},{"value":"1290-385X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7]]}}}