{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:40Z","timestamp":1725456220976},"publisher-location":"Berlin\/Heidelberg","reference-count":18,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012832","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"182-196","source":"Crossref","is-referenced-by-count":3,"title":["Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time"],"prefix":"10.1007","author":[{"given":"Jean","family":"Gallier","sequence":"first","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]},{"given":"David","family":"Plaisted","sequence":"additional","affiliation":[]},{"given":"Stan","family":"Raatz","sequence":"additional","affiliation":[]},{"given":"Wayne","family":"Snyder","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Proof Methods for Equational Theories","author":"L. Bachmair","year":"1987","unstructured":"Bachmair, L. \u201cProof Methods for Equational Theories\u201d, Ph.D thesis, University of Illinois, Urbana Champaign, Illinois (1987)."},{"key":"13_CR2","unstructured":"Bachmair, L., Dershowitz, N., and Plaisted, D., \u201cCompletion without Failure,\u201d Proceedings of CREAS, Lakeway, Texas (May 1987), also submitted for publication."},{"key":"13_CR3","unstructured":"Dauchet, M., Tison, S., Heuillard, T., and Lescanne, P., \u201cDecidability of the Confluence of Ground Term Rewriting Systems,\u201d LICS'87, Ithaca, New York (1987) 353\u2013359."},{"key":"13_CR4","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,. \u201cTermination of Rewriting,\u201d Journal of Symbolic Computation 3 (1987) 69\u2013116.","journal-title":"Journal of Symbolic Computation"},{"key":"13_CR5","volume-title":"Proceedings of CREAS","author":"N Dershowitz","year":"1987","unstructured":"Dershowitz, N,. \u201cCompletion and its Applications,\u201d Proceedings of CREAS, Lakeway, Texas (May 1987)."},{"issue":"4","key":"13_CR6","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P. J. Downey","year":"1980","unstructured":"Downey, Peter J., Sethi, Ravi, and Tarjan, Endre R. \u201cVariations on the Common Subexpressions Problem.\u201d J.ACM 27(4) (1980) 758\u2013771.","journal-title":"J.ACM"},{"key":"13_CR7","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J.H. Gallier","year":"1986","unstructured":"Gallier, J.H. Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York (1986)."},{"key":"13_CR8","unstructured":"Gallier, J.H., Raatz, S., and Snyder, W., \u201cTheorem Proving using Rigid E-Unification: Equational Matings,\u201d LICS'87, Ithaca, New York (1987) 338\u2013346."},{"key":"13_CR9","unstructured":"Gallier, J.H., Narendran, P., Plaisted, D., and Snyder, W., \u201cRigid E-Unification is NP-complete,\u201d LICS'88, Edinburgh, Scottland (July 1988)"},{"issue":"4","key":"13_CR10","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G., \u201cConfluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,\u201d J.ACM 27:4 (1980) 797\u2013821.","journal-title":"J.ACM"},{"key":"13_CR11","volume-title":"Formal Languages: Perspectives and Open Problems","author":"G. Huet","year":"1982","unstructured":"Huet, G. and Oppen, D. C., \u201cEquations and Rewrite Rules: A Survey,\u201d in Formal Languages: Perspectives and Open Problems, R.V. Book, ed., Academic Press, New York (1982)."},{"key":"13_CR12","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(85)90023-4","volume":"35","author":"D. Kapur","year":"1985","unstructured":"Kapur, D., and Narendran, P., \u201cA Finite Thue System With Decidable Word Problem and Without Equivalent Finite Canonical System,\u201d Theoret. Comp. Sci. 35 (1985) 337\u2013344.","journal-title":"Theoret. Comp. Sci."},{"key":"13_CR13","unstructured":"Knuth, D.E. and Bendix, P.B., \u201cSimple Word Problems in Univeral Algebras,\u201d in Computational Problems in Abstract Algebra, Leech, J., ed., Pergamon Press (1970)."},{"key":"13_CR14","series-title":"Technical Report TR","volume-title":"Complexity of Finitely Presented Algebras","author":"D. Kozen","year":"1976","unstructured":"Kozen, Dexter. Complexity of Finitely Presented Algebras, Technical Report TR 76-294, Department of Computer Science, Cornell University, Ithaca, NY (1976)."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Kozen, Dexter. Complexity of Finitely Presented Algebras, 9th STOC Symposium, Boulder Colorado, 164\u2013177 (May 1977)","DOI":"10.1145\/800105.803406"},{"key":"13_CR16","unstructured":"Lankford, D.S., \u201cCanonical Inference,\u201d Report ATP-32, University of Texas (1975)"},{"issue":"2","key":"13_CR17","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson Greg, and Oppen, Derek C. Fast Decision Procedures Based on Congruence Closure. J. ACM 27(2) (1980) 356\u2013364.","journal-title":"J. ACM"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Otto, F., and Squier, C., \u201cThe Word Problem for Finitely Presented Monoids and Finite Canonical Rewriting Systems,\u201d RTA'87, Bordeaux, France (1987) 74\u201382.","DOI":"10.1007\/3-540-17220-3_7"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012832","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:24:22Z","timestamp":1586579062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0012832","relation":{},"subject":[]}}