{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:49:18Z","timestamp":1725551358123},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662013"},{"type":"electronic","value":"9783540486855"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48685-2_15","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:41Z","timestamp":1269882821000},"page":"190-204","source":"Crossref","is-referenced-by-count":5,"title":["Normalization via Rewrite Closures"],"prefix":"10.1007","author":[{"given":"L.","family":"Bachmair","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I. V.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,11,5]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Canonical equational proofs. Birkh\u00e4user, Boston, 1991.","DOI":"10.1007\/978-1-4684-7118-2"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. JACM, 41:236\u2013276, 1994.","journal-title":"JACM"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"L. P. Chew. An improved algorithm for computing with equations. In 21st Annual Symposium on Foundations of Computer Science, 1980.","DOI":"10.1109\/SFCS.1980.11"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"L. P. Chew. Normal forms in term rewriting systems. PhD thesis, Purdue University, 1981.","DOI":"10.1145\/800076.802452"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J. P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B: Formal Models and Semantics), Amsterdam, 1990. North-Holland.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Proc. 8th Intl. RTA","author":"D. Kapur","year":"1997","unstructured":"D. Kapur. Shostak\u2019s congruence closure as completion. In H. Comon, editor, Proc. 8th Intl. RTA, pages 23\u201337, 1997. LNCS 1232, Springer, Berlin."},{"key":"15_CR7","first-page":"2","volume-title":"Handbook of Logic in Computer Science","author":"J. W. Klop","year":"1992","unstructured":"J. W. Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, chapter 6, pages 2\u2013116. Oxford University Press, Oxford, 1992."},{"issue":"2","key":"15_CR8","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. Oppen. Fast decision procedures based on congruence closure. JACM, 27(2):356\u2013364, 1980.","journal-title":"JACM"},{"key":"15_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TACAS","author":"D. J. Sherman","year":"1998","unstructured":"D. J. Sherman and N. Magnier. Factotum: Automatic and systematic sharing support for systems analyzers. In Proc. TACAS, LNCS 1384, 1998."},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"984","DOI":"10.1145\/210118.210130","volume":"42","author":"R. M. Verma","year":"1995","unstructured":"R. M. Verma. A theory of using history for equational systems with applications. JACM, 42:984\u20131020, 1995.","journal-title":"JACM"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"R. M. Verma and I. V. Ramakrishnan. Nonoblivious normalization algorithms for nonlinear systems. In Proc. of the Int. Colloquium on Automata, Languages and Programming, New York, 1990. Springer-Verlag.","DOI":"10.1007\/BFb0032045"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48685-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T14:58:54Z","timestamp":1558969134000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48685-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662013","9783540486855"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-48685-2_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}