{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T06:14:04Z","timestamp":1768284844420,"version":"3.49.0"},"reference-count":29,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1988,8,1]],"date-time":"1988-08-01T00:00:00Z","timestamp":586396800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":9116,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[1988,8]]},"DOI":"10.1016\/s0747-7171(88)80018-x","type":"journal-article","created":{"date-parts":[[2008,5,29]],"date-time":"2008-05-29T10:22:56Z","timestamp":1212056576000},"page":"1-18","source":"Crossref","is-referenced-by-count":46,"title":["Critical pair criteria for completion"],"prefix":"10.1016","volume":"6","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Nachum","family":"Dershowitz","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(88)80018-X_bib1","series-title":"Dissertation","article-title":"Proof methods for equational theories","author":"Bachmair","year":"1987"},{"key":"10.1016\/S0747-7171(88)80018-X_bib2","series-title":"Proc. IEEE Symp. Logic in Computer Science","first-page":"346","article-title":"Orderings for equational proofs","author":"Bachmair","year":"1986"},{"key":"10.1016\/S0747-7171(88)80018-X_bib3","first-page":"192","article-title":"Completion for rewriting modulo a congruence","volume":"256","author":"Bachmair","year":"1987"},{"key":"10.1016\/S0747-7171(88)80018-X_bib4","series-title":"Proc. Eurocal \u201987. Leipzig","article-title":"Critical pair criteria for rewriting modulo a. congruence. To appear","author":"Bachmair","year":"1987"},{"key":"10.1016\/S0747-7171(88)80018-X_bib5","first-page":"3","article-title":"A criterion for detecting unnecessary reductions in the construction, of Gr\u00f6bner bases","volume":"72","author":"Buchberger","year":"1979"},{"key":"10.1016\/S0747-7171(88)80018-X_bib6","first-page":"137","article-title":"A critical-pair\/completion algorithm for finitely generated ideals in rings","volume":"171","author":"Buchberger","year":"1984"},{"key":"10.1016\/S0747-7171(88)80018-X_bib7","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/S0019-9958(85)80003-6","article-title":"Computing with rewrite systems","volume":"64","author":"Dershowitz","year":"1985","journal-title":"Inf. Control"},{"key":"10.1016\/S0747-7171(88)80018-X_bib8","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","article-title":"Proving termination with multiset orderings","volume":"22","author":"Dershowitz","year":"1979","journal-title":"Comm. A CM"},{"key":"10.1016\/S0747-7171(88)80018-X_bib9","article-title":"Existence, uniqueness, and construction of rewrite systems","author":"Dershowitz","year":"1987","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0747-7171(88)80018-X_bib10","series-title":"Proc. 1985 Symp. on Logic Programming","first-page":"172","article-title":"SLOG: A logic programming language interpreter based on clausal superposition and rewriting","author":"Fribourg","year":"1985"},{"key":"10.1016\/S0747-7171(88)80018-X_bib11","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","article-title":"Refutational theorem proving using term-rewriting systems","volume":"25","author":"Hsiang","year":"1985","journal-title":"Artif. Intell."},{"key":"10.1016\/S0747-7171(88)80018-X_bib12","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","article-title":"Confluent reductions: abstract properties and applications to term rewriting systems","volume":"27","author":"Huet","year":"1980","journal-title":"J. ACM"},{"key":"10.1016\/S0747-7171(88)80018-X_bib13","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","article-title":"A complete proof of correctness of the Knuth and Bendix completion algorithm","volume":"23","author":"Huet","year":"1981","journal-title":"J. Comp. Syst. Sci."},{"key":"10.1016\/S0747-7171(88)80018-X_bib14","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","article-title":"Proofs by induction in equational theories with constructors","volume":"25","author":"Huet","year":"1982","journal-title":"J. Comp. Syst. Sci."},{"key":"10.1016\/S0747-7171(88)80018-X_bib15","series-title":"Tech. Rep. CSL-113","article-title":"A catalogue of canonical term rewriting systems","author":"Hullot","year":"1980"},{"key":"10.1016\/S0747-7171(88)80018-X_bib16","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","article-title":"Completion of a set of rules modulo a set of equations","volume":"15","author":"Jouannaud","year":"1986","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0747-7171(88)80018-X_bib17","series-title":"Only prime superpositions need be considered in the Knuth-Bendix proceduia","author":"Kapur","year":"1985"},{"key":"10.1016\/S0747-7171(88)80018-X_bib18","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/S0747-7171(88)80018-X_bib19","first-page":"378","article-title":"A confluence criterion based on the generalised Newman lemma","volume":"204","author":"K\u00fcchlin","year":"1985"},{"key":"10.1016\/S0747-7171(88)80018-X_bib20","series-title":"A generalized Knuth-Bendix algorithm.","author":"K\u00fcchlin","year":"1986"},{"key":"10.1016\/S0747-7171(88)80018-X_bib21","series-title":"Report 86-02","article-title":"Equational Cornpletion by Proof Simplification","author":"K\u00fcchlin","year":"1986"},{"key":"10.1016\/S0747-7171(88)80018-X_bib22","series-title":"Proc. Fourth Workshop on Automated Deduction","first-page":"168","article-title":"The refutation completeness of blocked permutative narrowing and resolution","author":"Lankford","year":"1979"},{"key":"10.1016\/S0747-7171(88)80018-X_bib23","series-title":"Canonical forms in finitely presented algebras","author":"Le Chenadec","year":"1986"},{"key":"10.1016\/S0747-7171(88)80018-X_bib24","series-title":"Proc. 7th ACM Symp. on Principles of Programming Languages","first-page":"154","article-title":"On proving inductive properties of abstract data types","author":"Musser","year":"1980"},{"key":"10.1016\/S0747-7171(88)80018-X_bib25","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reductions for some equational theories","volume":"28","author":"Peterson","year":"1981","journal-title":"J. ACM"},{"key":"10.1016\/S0747-7171(88)80018-X_bib26","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","article-title":"Automated theorem proving for theories with simplifiers, cornmutativity, and associativity","volume":"21","author":"Slagle","year":"1974","journal-title":"J. ACM"},{"key":"10.1016\/S0747-7171(88)80018-X_bib27","series-title":"Dissertation","article-title":"The Church-Rosser property in computer algebra and special theorem proving: An investigation of critical-pair\/completion algorithms","author":"Winkler","year":"1984"},{"key":"10.1016\/S0747-7171(88)80018-X_bib28","first-page":"378","article-title":"Reducing the complexity of the Knuth-Bendix completion algorithm: a \u2018unification\u2019 of different approaches","volume":"204","author":"Winkler","year":"1985"},{"key":"10.1016\/S0747-7171(88)80018-X_bib29","series-title":"Proc. Coll. on Algebra, Combinatorics and Logic in Computer Science","article-title":"A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm","author":"Winkler","year":"1983"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S074771718880018X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S074771718880018X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,28]],"date-time":"2018-12-28T07:24:38Z","timestamp":1545981878000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S074771718880018X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,8]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1988,8]]}},"alternative-id":["S074771718880018X"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(88)80018-x","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1988,8]]}}}