{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:54:41Z","timestamp":1773654881334,"version":"3.50.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[1993,6,1]],"date-time":"1993-06-01T00:00:00Z","timestamp":738892800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1993,6]]},"DOI":"10.1007\/bf01209624","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T07:35:07Z","timestamp":1109316907000},"page":"537-568","source":"Crossref","is-referenced-by-count":8,"title":["Proving termination of (conditional) rewrite systems"],"prefix":"10.1007","volume":"30","author":[{"given":"Eddy","family":"Bevers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johan","family":"Lewi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Pedreschi, D.: Studies in pure prolog: termination. In: Lloyd, J.W. (ed.) Proc. Esprit Symposium on Computational Logic, pp. 150?176, 1990","DOI":"10.1007\/978-3-642-76274-1_9"},{"key":"CR2","first-page":"1","volume-title":"Formal techniques in artificial intelligence. A sourcebook","author":"J. Avenhaus","year":"1990","unstructured":"Avenhaus, J., Madlener, K.: Term rewriting and equational reasoning. In: Banerji, R.B. (ed.) Formal techniques in artificial intelligence. A sourcebook, pp. 1?44. Amsterdam: Elsevier 1990"},{"key":"CR3","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/3-540-16780-3_76","volume-title":"CADE 8","author":"L. Bachmair","year":"1986","unstructured":"Bachmair, L., Dershowitz, N.: Commutation, transformation and termination. In: Siekmann, J.H. (ed.) CADE 8 (Lect. Notes Comput. Sci., vol. 230, pp. 5?20) Berlin Heidelberg New York: Springer 1986"},{"key":"CR4","unstructured":"Bachmair, L.: Proof methods for equational theories. PhD thesis, Dept. of Computer Science, University of Illinois at Urbana-Champaign, 1987"},{"key":"CR5","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/3-540-17660-8_48","volume-title":"TAPSOFT '87","author":"F. Bellegarde","year":"1987","unstructured":"Bellegarde, F., Lescanne, P.: Transformation orderings. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT '87 (Lect. Notes Comput. Sci., vol. 249, pp. 69?80) Berlin Heidelberg New York: Springer 1987"},{"key":"CR6","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-16780-3_78","volume-title":"CADE 8","author":"A. Ben Cherifa","year":"1986","unstructured":"Ben Cherifa, A., Lescanne, P.: An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations. In: Siekmann, J.H. (ed.) CADE 8 (Lect. Notes Comput. Sci., vol. 230, pp. 42?51) Berlin Heidelberg New York: Springer 1986"},{"issue":"2","key":"CR7","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., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program.9(2), 137?159 (1987)","journal-title":"Sci. Comput. Program."},{"key":"CR8","volume-title":"Conditional rewrite rules: Confluence and termination","author":"J. Bergstra","year":"1982","unstructured":"Bergstra, J., Klop, J.W.: Conditional rewrite rules: Confluence and termination. Report IW 198\/82, Mathematisch Centrum, Amsterdam, 1982"},{"key":"CR9","unstructured":"Bevers, E.: Automated reasoning in conditional algebraic specifications: termination and proof by consistency. PhD thesis, Dept. of Computer Science KU Leuven, 1993"},{"key":"CR10","volume-title":"A computational logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A computational logic, New York: Academic Press 1979"},{"issue":"1","key":"CR11","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","volume":"12","author":"R. Burstall","year":"1969","unstructured":"Burstall, R.: Proving properties of programs by structural induction. Comput. J.12(1), 41?48 (1969)","journal-title":"Comput. J."},{"key":"CR12","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/BFb0012855","volume-title":"CADE 9","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G.: Canonical conditional rewrite systems. In: Lusk, E., Overbeek, R. (eds.) CADE 9 (Lect. Notes Comput. Sci., vol. 310, pp. 538?549) Berlin Heidelberg New York: Springer 1988"},{"issue":"5","key":"CR13","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","volume":"9","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N.: A note on simplification orderings. Inf. Process. Lett.9(5), 212?215 (1979)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"CR14","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. J. Theor. Comput. Sci.17(3), 279?301 (1982)","journal-title":"J. Theor. Comput. Sci."},{"key":"CR15","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-15976-2_9","volume-title":"Rewriting techniques and applications","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N.: Termination. In: Jouannaud, J.-P. (ed.) Rewriting techniques and applications (Lect. Notes Comput. Sci., vol. 202, pp. 180?224) Berlin Heidelberg New York: Springer 1985"},{"issue":"1?2","key":"CR16","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symb. Comput.3(1?2), 69?115 (1987)","journal-title":"J. Symb. Comput."},{"key":"CR17","series-title":"Lect. Notes Comput. Sci.","volume-title":"Rewriting techniques and applications","year":"1989","unstructured":"Dershowitz, N. (ed.): Rewriting techniques and applications. (Lect. Notes Comput. Sci., vol. 355) Berlin Heidelberg New York: Springer 1989"},{"key":"CR18","first-page":"243","volume-title":"Handbook of theoretical computer science, vol. B","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of theoretical computer science, vol. B, chap. 6, pp. 243?320. Amsterdam: Elsevier 1990"},{"key":"CR19","unstructured":"Geser, A.: Termination relative. PhD thesis, University Passau, 1989"},{"key":"CR20","series-title":"Rapport Laboria","volume-title":"On the uniform halting problem for term rewriting systems","author":"G. Huet","year":"1978","unstructured":"Huet, G., Lankford, D.S.: On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA, Le Chesnay, France, 1978"},{"key":"CR21","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal language theory: perspectives and open problems","author":"G. Huet","year":"1980","unstructured":"Huet, G., Oppen, D.: Equations and rewrite rules: a survey. In: Book, R.V. (ed.) Formal language theory: perspectives and open problems, pp. 349?405, New York: Academic Press 1980"},{"key":"CR22","first-page":"331","volume-title":"Second IFIP Workshop on Formal Description of Programming Concepts","author":"J.-P. Jouannaud","year":"1982","unstructured":"Jouannaud, J.-P., Lescanne, P., Reinig, F.: Recursive decomposition ordering. In: Bj\u00f8rner, D. (ed.) Second IFIP Workshop on Formal Description of Programming Concepts, pp. 331?348. Amsterdam: North-Holland 1982"},{"key":"CR23","volume-title":"Proc. 3rd IFIP Working Conference on Formal Description of Programming Concepts","author":"J.-P. Jouanaud","year":"1986","unstructured":"Jouanaud, J.-P., Waldmann, B.: Reductive conditional term rewriting systems. In: Proc. 3rd IFIP Working Conference on Formal Description of Programming Concepts. Amsterdam: North-Holland 1986"},{"key":"CR24","series-title":"Lect. Notes Comput. Sci.","volume-title":"Rewriting techniques and applications","year":"1985","unstructured":"Jouannaud, J.-P. (ed.): Rewriting techniques and applications. (Lect. Notes Comput. Sci., vol. 202) Berlin Heidelberg New York: Springer 1985"},{"key":"CR25","volume-title":"Two generalisations of the recursive path ordering","author":"S. Kamin","year":"1980","unstructured":"Kamin, S., L\u00e9vy, J.-J.: Two generalisations of the recursive path ordering. Department of Computer Science, University of Illinois, USA, 1980"},{"key":"CR26","series-title":"Lect. Notes Comput. Sci.","volume-title":"Conditional term rewriting systems","year":"1987","unstructured":"Kaplan, S., Jouannaud, J.-P. (eds.): Conditional term rewriting systems. (Lect. Notes Comput. Sci., vol. 308) Berlin Heidelberg New York, Springer 1987"},{"key":"CR27","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(84)90087-2","volume":"33","author":"S. Kaplan","year":"1984","unstructured":"Kaplan, S.: Conditional rewrite rules. Theor. Comput. Sci.33, 175?193 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"CR28","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(87)80010-X","volume":"4","author":"S. Kaplan","year":"1987","unstructured":"Kaplan, S.: Simplifying conditional term rewriting systems: unification, termination and confluence. J. Symb. Comput.4, 295?334 (1987)","journal-title":"J. Symb. Comput."},{"key":"CR29","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/3-540-15198-2_11","volume-title":"Mathematical foundations of software development. Vol. 1: Colloquium on Trees in Algebra and Programming (CAAP '85)","author":"D. Kapur","year":"1985","unstructured":"Kapur, D., Narendran, P., Sivakumar, G.: A path ordering for proving termination of term rewriting systems. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds.) Mathematical foundations of software development. Vol. 1: Colloquium on Trees in Algebra and Programming (CAAP '85) (Lect. Notes Comput. Sci., vol. 185, pp. 173?187) Berlin Heidelberg New York: Springer 1985"},{"key":"CR30","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4.50028-X","volume-title":"Computational problems in abstract algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational problems in abstract algebra, pp. 263?297. New York: Pergamon Press 1970"},{"key":"CR31","volume-title":"Canonical algebraic simplification in computational logic","author":"D.S. Lankford","year":"1975","unstructured":"Lankford, D.S.: Canonical algebraic simplification in computational logic. Memo ATP-25, Automatic Theorem Proving Project, University of Texas, Austin, TX, 1975"},{"key":"CR32","volume-title":"On proving term rewriting systems are noetherian","author":"D.S. Lankford","year":"1979","unstructured":"Lankford, D.S.: On proving term rewriting systems are noetherian. Memo MTP-3, Mathematics Department Louisiana Tech. University, Ruston, LA, 1979"},{"key":"CR33","first-page":"181","volume-title":"Ninth Colloquium on Trees in Algebra and Programming","author":"P. Lescanne","year":"1984","unstructured":"Lescanne, P.: Uniform termination of term rewriting systems: recursive decomposition ordering with status. In: Courcelle, B. (ed.) Ninth Colloquium on Trees in Algebra and Programming, pp. 181?194. Cambridge: Cambridge University Press 1984"},{"key":"CR34","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00302640","volume":"6","author":"P. Lescanne","year":"1990","unstructured":"Lescanne, P.: On the recursive decomposition ordering with lexicographical status and other related orderings. J. Autom. Reasoning6, 39?49 (1990)","journal-title":"J. Autom. Reasoning"},{"key":"CR35","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Granborg, B.S.M. (ed.) Third Hawaii International Conference on System Science, pp. 789?792. North Hollywood Western Periodicals"},{"key":"CR36","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-17220-3_4","volume-title":"Conditional term rewriting systems","author":"U. Martin","year":"1987","unstructured":"Martin, U.: How to choose the weights in the Knuth-Bendix ordering. In: Kaplan, S., Jouannaud, J.-P. (eds.) Conditional term rewriting systems (Lect. Notes Comput. Sci., vol. 308, pp. 42?53) Berlin Heidelberg New York: Springer 1987"},{"key":"CR37","series-title":"Technical Report R-78-943","volume-title":"A recursively defined ordering for proving termination of term rewriting systems","author":"D.A. Plaisted","year":"1978","unstructured":"Plaisted, D.A.: A recursively defined ordering for proving termination of term rewriting systems. Technical Report R-78-943, Department of Computer Science, University of Illinois, Urbana, IL, 1978"},{"key":"CR38","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-15976-2_10","volume-title":"Rewriting techniques and applications","author":"M. rusinowitch","year":"1985","unstructured":"rusinowitch, M.: Path of subterm ordering and recursive decomposition ordering revisited. In: Jouannaud, J.-P. (ed.) Rewriting techniques and applications (Lect. Notes Comput. Sci., vol. 202, pp. 225?240) Berlin Heidelberg New York: Springer 1985"},{"key":"CR39","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/3-540-51081-8_124","volume-title":"Rewriting techniques and applications","author":"J. Steinbach","year":"1989","unstructured":"Steinbach, J.: Extensions and comparisons of simplification orderings. In: Dershowitz, N. (ed.) Rewriting techniques and applications (Lect. Notes Comput. Sci., vol. 355, pp. 434?448) Berlin Heidelberg New York: Springer 1989"},{"key":"CR40","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-75030-4","volume-title":"Algebraic specifications in software engineering: an introduction","author":"I. Horebeek Van","year":"1989","unstructured":"Van Horebeek, I., Lewi, J.: Algebraic specifications in software engineering: an introduction. Berlin Heidelberg New York: Springer 1989"},{"key":"CR41","unstructured":"Vergauwen, B.: Een modelvoorbeeld van algebra\u00efsche specificaties: een telefooncentrale. Master's thesis, Dept. Computerwetenschappen, K.U. Leuven (In Dutch) 1987"},{"key":"CR42","series-title":"Leet. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/BFb0012831","volume-title":"CADE 9","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Lusk, E., Overbeek, R. (eds.) CADE 9 (Leet. Notes Comput. Sci., vol. 310, pp. 162?181) Berlin Heidelberg New York: Springer 1988"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01209624.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01209624\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01209624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T05:40:20Z","timestamp":1556775620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01209624"}},"subtitle":["A semantic approach"],"short-title":[],"issued":{"date-parts":[[1993,6]]},"references-count":42,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1993,6]]}},"alternative-id":["BF01209624"],"URL":"https:\/\/doi.org\/10.1007\/bf01209624","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,6]]}}}