{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,2]],"date-time":"2023-05-02T11:12:17Z","timestamp":1683025937879},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We focus on termination proofs of rewrite systems, especially of rewrite systems containing associative and commutative operators. We prove their termination by elementary interpretations, more specifically, by functions defined by addition, multiplication and exponentiation. We discuss a method based on polynomial interpretations and propose an implementation of a mechanisation of the comparison of expressions built with polynomials and exponentials.<\/jats:p>","DOI":"10.1007\/bf01214624","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T16:30:35Z","timestamp":1109349035000},"page":"77-90","source":"Crossref","is-referenced-by-count":7,"title":["Termination of rewrite systems by elementary interpretations"],"prefix":"10.1145","volume":"7","author":[{"given":"Pierre","family":"Lescanne","sequence":"first","affiliation":[{"name":"Centre de Recherche en Informatique de Nancy (CNRS) and INRIA-Lorraine, BP 239, Campus Scientifique, 54506, Vand\u0153uvre-l\u00e8s-Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"542","volume-title":"COMTES \u2014 an experimental environment for the completion of term rewriting systems","author":"Avenhaus J.","year":"1989"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bachmair L.: Canonical equational proofs . Computer Science Logic Progress in Theoretical Computer Science. Birkh\u00e4user Verlag AG 1991.","DOI":"10.1007\/978-1-4684-7118-2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90030-X"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bachmair L. Dershowitz N. and Plaisted D.: Completion without failure. In H. A\u00eft-Kaci and M. Nivat editors Resolution of Equations in Algebraic Structures Volume 2: Rewriting Techniques pages 1\u201330. Academic Press 1989.","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01810293"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(85)80019-5"},{"key":"e_1_2_1_2_7_2","volume-title":"Rapport interne 91-R-151","author":"Cichon E. A.","year":"1991"},{"key":"e_1_2_1_2_8_2","unstructured":"Delor C.: Terminaison des syst\u00e8mes de r\u00e9\u00e9criture application \u00e0 la transformation des formules \u00e9quationnelles. Th\u00e8se de l'Universit\u00e9 de Paris VII June 1991."},{"key":"e_1_2_1_2_9_2","unstructured":"Dershowitz N. and Mitra S.: RPO for AC-termination. Unpublished manuscript U. of Illinois 1992."},{"key":"e_1_2_1_2_10_2","unstructured":"Forgaard R.: A program for generating and analyzing term rewriting systems. Technical Report 343 Laboratory for Computer Science Massachusetts Institute of Technology 1984. Master's Thesis."},{"key":"e_1_2_1_2_11_2","volume-title":"Dissertation thesis","author":"Geser A.","year":"1990"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Garland S. J. and Guttag J. V.: An overview of LP the Larch Prover. In N. Dershowitz editor Proceedings 3rd Conference on Rewriting Techniques and Applications Chapel Hill (North Carolina USA) volume 355 of LNCS pages 137\u2013151. Springer-Verlag April 1989.","DOI":"10.1007\/3-540-51081-8_105"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Gnaedig I. and Lescanne P.: Proving termination of associative rewriting systems by rewriting. In J. Siekmann editor Proceedings 8th International Conference on Automated Deduction Oxford (UK) volume 230 of LNCS pages 52\u201361. Springer-Verlag 1986.","DOI":"10.1007\/3-540-16780-3_79"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Hsiang J. and Rusinowitch M.: On word problem in equational theories. In Th. Ottmann editor Proceedings of 14th International Colloquium on Automata Languages and Programming Karlsruhe (Germany) volume 267 of LNCS pages 54\u201371. Springer-Verlag 1987.","DOI":"10.1007\/3-540-18088-5_6"},{"key":"e_1_2_1_2_15_2","unstructured":"Kamin S. and L\u00e9vy J.-J.: Attempts for generalizing the recursive path ordering. Unpublished manuscript 1980."},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Kapur D. Sivakumar G. and Zhang H.: A new method for proving termination of AC-rewrite systems. In Proceedings 10th Conf. on Foundations of Software Technology and Theoretical Computer Science volume 472 of LNCS pages 133\u2013148. Springer-Verlag 1990.","DOI":"10.1007\/3-540-53487-3_40"},{"key":"e_1_2_1_2_17_2","volume-title":"Technical report","author":"Lankford D. S.","year":"1979"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Lescanne P.: Computer experiments with the REVE term rewriting systems generator. In Proceedings of 10th ACM Symposium on Principles of Programming Languages pages 99\u2013108. Association for Computing Machinery 1983.","DOI":"10.1145\/567067.567078"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Lescanne P.: Completion procedures as transition rules + control. In M. Diaz and F. Orejas editors TAPSOFT'89 volume 351 of LNCS pages 28\u201341. Springer-Verlag 1989.","DOI":"10.1007\/3-540-50939-9_123"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Lescanne P.: Implementation of completion by transition rules + control: ORME. In H. Kirchner and W. Wechler editors Proceedings 2nd International Workshop on Algebraic and Logic Programming Nancy (France) volume 463 of LNCS pages 262\u2013269. Springer-Verlag 1990.","DOI":"10.1007\/3-540-53162-9_44"},{"key":"e_1_2_1_2_21_2","unstructured":"P\u00e9ter R.: Recursive Functions . Academic Press 1967."},{"key":"e_1_2_1_2_22_2","unstructured":"Weis P. Aponte M. V. Laville A. Mauny M. and Su\u00e1rez A.: The CAML reference manual. Technical report Projet Formel INRIA-ENS 1989. Version 2.6."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01214624.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01214624\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01214624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,2]],"date-time":"2023-05-02T10:51:40Z","timestamp":1683024700000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01214624"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["10.1007\/BF01214624"],"URL":"https:\/\/doi.org\/10.1007\/bf01214624","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}