{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:09Z","timestamp":1725663369940},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540172208"},{"type":"electronic","value":"9783540474210"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1987]]},"DOI":"10.1007\/3-540-17220-3_17","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:14:47Z","timestamp":1330197287000},"page":"192-203","source":"Crossref","is-referenced-by-count":9,"title":["Completion for rewriting modulo a congruence"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Nachum","family":"Dershowitz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,26]]},"reference":[{"key":"17_CR1","unstructured":"Bachmair, L. (1987). Proof methods for equational theories. Ph.D. thesis, Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., and Dershowitz, N. (1986). Critical pair criteria for the Knuth-Bendix completion method. Proc. Symp. on Symbolic and Algebraic Computation, B. W. Char, ed., Waterloo, Canada, 215\u2013217. (Revised version to appear in J. Symbolic Computation.)","DOI":"10.1145\/32439.32481"},{"key":"17_CR3","unstructured":"Bachmair, L., Dershowitz, N., and Hsiang, J. (1986). Orderings for equational proofs. Proc. IEEE Symp. Logic in Computer Science, Cambridge, Massachusetts, 346\u2013357."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Hullot, J.-M. (1980). A catalogue of canonical term rewriting systems. Tech. Rep. CSL-113, SRI International, Menlo Park, California.","DOI":"10.21236\/ADA087641"},{"key":"17_CR5","series-title":"Lect. Notes in Comp. Sci.","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-12727-5_16","volume-title":"Proc. 8th Coll. on Trees in Algebra and Programming","author":"J.-P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P. (1983). Confluent and coherent equational term rewriting systems: Application to proofs in abstract data types. Proc. 8th Coll. on Trees in Algebra and Programming, G. Ausiello and M. Protasi, eds., Lect. Notes in Comp. Sci., vol. 59, Springer-Verlag, Berlin, 269\u2013283."},{"key":"17_CR6","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., and Kirchner, H. (1986). Completion of a set of rules modulo a set of equations. SIAM J. Computing 15, 1155\u20131194.","journal-title":"SIAM J. Computing"},{"key":"17_CR7","unstructured":"Kapur, D., Musser, D.R., and Narendran, P. (1986). Only prime superpositions need be considered in the Knuth-Bendix procedure. Unpublished manuscript, Computer Science Branch, Corporate Research and Development, General Electric, Schenectady, New York."},{"key":"17_CR8","unstructured":"Knuth, D., and Bendix, P. (1970). Simple word problems in universal algebras. Computational Problems in Abstract Algebra, J. Leech, ed., Pergamon Press, 263\u2013297."},{"key":"17_CR9","unstructured":"K\u00fcchlin, W. (1986). Equational Completion by Proof Simplification. Report No. 86-02, Mathematik, ETH Z\u00fcrich, Switzerland."},{"key":"17_CR10","volume-title":"Decision procedures for simple equational theories with permutative axioms: Canonical sets of permutative reductions. Memo ATP-37","author":"D. Lankford","year":"1977","unstructured":"Lankford, D., and Ballantyne, A. (1977). Decision procedures for simple equational theories with permutative axioms: Canonical sets of permutative reductions. Memo ATP-37, Dept. of Mathematics and Computer Science, University of Texas, Austin, Texas."},{"key":"17_CR11","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson, G., and Stickel, M. (1981). Complete sets of reductions for some equational theories. J. ACM 28, 233\u2013264.","journal-title":"J. ACM"},{"key":"17_CR12","series-title":"Lect. Notes in Comp. Sci.","first-page":"1","volume-title":"Proc. 7th Conf. Automated Deduction","author":"J. Siekman","year":"1984","unstructured":"Siekman, J. (1984). Universal unification. Proc. 7th Conf. Automated Deduction, R. E. Shostak, ed., Lect. Notes in Comp. Sci., vol. 170, Springer-Verlag, Berlin, 1\u201342."}],"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-17220-3_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:10:39Z","timestamp":1619557839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-17220-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987]]},"ISBN":["9783540172208","9783540474210"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-17220-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1987]]}}}