{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T05:49:51Z","timestamp":1768283391456,"version":"3.49.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1990,2,1]],"date-time":"1990-02-01T00:00:00Z","timestamp":633830400000},"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":[[1990,2]]},"DOI":"10.1007\/bf01237233","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T23:47:12Z","timestamp":1109375232000},"page":"95-119","source":"Crossref","is-referenced-by-count":30,"title":["Automating the Knuth Bendix ordering"],"prefix":"10.1007","volume":"28","author":[{"given":"Jeremy","family":"Dick","sequence":"first","affiliation":[]},{"given":"John","family":"Kalmus","sequence":"additional","affiliation":[]},{"given":"Ursula","family":"Martin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0167-6423(86)90017-1","volume":"6","author":"F. Bellegarde","year":"1986","unstructured":"Bellegarde, F.: Rewriting systems of FP expressions to reduce the number sequences yielded. Sci. Comput. Program.6, 11?34 (1986)","journal-title":"Sci. Comput. Program."},{"key":"CR2","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"},{"key":"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., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program.9, 137?160 (1987)","journal-title":"Sci. Comput. Program."},{"key":"CR4","volume-title":"Linear programming","author":"V. Chvatal","year":"1983","unstructured":"Chvatal, V.: Linear programming. New York: Freeman 1983"},{"key":"CR5","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, 279?301 (1982)","journal-title":"Theor. Comp. Sci."},{"key":"CR6","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. Symbol. Comput.3, 69?116 (1987)","journal-title":"J. Symbol. Comput."},{"key":"CR7","series-title":"Lect. Notes Comput. Sci.","volume-title":"Proceedings of the First International Conference on Rewriting Techniques and Applications","author":"R. Forgaard","year":"1985","unstructured":"Forgaard, R., Detlefs, D.: A procedure for automatically proving the termination of a set of rewrite rules. Proceedings of the First International Conference on Rewriting Techniques and Applications. (Lect. Notes Comput. Sci., vol. 202) Berlin Heidelberg New York: Springer 1985"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Dick, A.J.J.: ERIL ? Equational reasoning: an interactive laboratory. Rutherford Appleton Laboratory Report RAL-86-010, March 1985","DOI":"10.1007\/3-540-15984-3_295"},{"key":"CR9","unstructured":"Dick, A.J.J., Kalmus J.R.: ERIL (Equational reasoning: an interactive laboratory). User's manual. Version R1.6, Rutherford Appleton Laboratory Report RAL-88-055, September 1988"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"193","DOI":"10.2307\/2269866","volume":"33","author":"S. Feferman","year":"1968","unstructured":"Feferman, S.: Systems of predicative analysis II: Representation of ordinals. J. Symbol. Logic33, 193?220 (1968)","journal-title":"J. Symbol. Logic"},{"key":"CR11","volume-title":"The theory of linear economic models","author":"D. Gale","year":"1960","unstructured":"Gale, D.: The theory of linear economic models. New York: McGraw Hill 1960"},{"issue":"4","key":"CR12","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J. Ass. Comp. Mach.27(4) 797?821 (1980), preliminary version in 18th Symposium on Foundations of Computer Science, IEEE, 1977","journal-title":"J. Ass. Comp. Mach."},{"key":"CR13","unstructured":"Huet, G., Lankford, D.S.: On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA, March 1978"},{"issue":"3","key":"CR14","first-page":"326","volume":"2","author":"G. Higman","year":"1952","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proc LMS(3)2, 326?336 (1952)","journal-title":"Proc LMS"},{"key":"CR15","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.C.: Equations and rewrite rules: a survey. In: Book, R. (ed.), Formal language theory, perspectives and open problems, pp. 349?405. New York: Academic Press 1980"},{"key":"CR16","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":"CR17","volume-title":"Linear programming","author":"B. Kreko","year":"1968","unstructured":"Kreko, B.: Linear programming. London: Pitman 1968"},{"key":"CR18","series-title":"Automatic Theorem Proving Project","volume-title":"Canonical algebraic simplification in computational logic","author":"D.S. Lankford","year":"1975","unstructured":"Lankford, D.S.: Canonical algebraic simplification in computational logic. Mem ATP-25. Automatic Theorem Proving Project. University of Texas, Austin TX, May 1975"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Lescanne, P.: Computer experiments with the REVE term rewriting system generator, Proc 10th ACM POPL symposium, Austin, TX 1983, pp. 99?108","DOI":"10.1145\/567067.567078"},{"key":"CR20","first-page":"80","volume":"30","author":"P. Lescanne","year":"1986","unstructured":"Lescanne, P.: Divergence of the Knuth Bendix completion procedure and termination orderings. Bull. Eur. Assoc. Theoret. Comput. Sci.30, 80?83 (1986)","journal-title":"Bull. Eur. Assoc. Theoret. Comput. Sci."},{"key":"CR21","unstructured":"Lescanne, P.: Private communication"},{"key":"CR22","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. Proceedings of the Third Hawaii International Conference on System Science, Honolulu, HI, January 1970, pp. 789?792"},{"key":"CR23","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-17220-3_4","volume-title":"Proceedings of the Second International Conference on Rewriting Techniques and Applications (RTA 87), Bordeaux, France, May 1987","author":"U. Martin","year":"1987","unstructured":"Martin, U.: How to choose the weights in the Knuth Bendix ordering. Proceedings of the Second International Conference on Rewriting Techniques and Applications (RTA 87), Bordeaux, France, May 1987. (Lect. Notes Comput. Sci., vol. 256, pp. 42?53) Berlin Heidelberg New York: Springer 1987"},{"key":"CR24","series-title":"Lect Notes Comput. Sci.","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08531-9","volume-title":"Computing in systems described by equations","author":"M.J. O'Donnell","year":"1977","unstructured":"O'Donnell, M.J.: Computing in systems described by equations (Lect Notes Comput. Sci., vol. 58) Berlin Heidelberg New York: Springer 1977"},{"key":"CR25","series-title":"Lect. Notes Comput. Sci.","volume-title":"Proceedings of the First International Conference on Rewriting Techniques and Applications","author":"M. Rusinowitch","year":"1985","unstructured":"Rusinowitch, M.: Plaisted ordering and recursive decomposition ordering revisited. Proceedings of the First International Conference on Rewriting Techniques and Applications. (Lect. Notes Comput. Sci., vol. 202) Berlin Heidelberg New York: Springer 1985"},{"key":"CR26","first-page":"179","volume-title":"Studies in linear and non-linear programming","author":"H. Uzawa","year":"1958","unstructured":"Uzawa, H.: An elementary method for linear programming. In: Arrow, K.J., Hurwicz, L., Uzawa, H. (eds.) Studies in linear and non-linear programming, pp. 179?188. Stanford: Stanford University Press 1958"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01237233.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01237233\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01237233","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T00:03:44Z","timestamp":1586131424000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01237233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,2]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1990,2]]}},"alternative-id":["BF01237233"],"URL":"https:\/\/doi.org\/10.1007\/bf01237233","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,2]]}}}