{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T07:16:08Z","timestamp":1768288568745,"version":"3.49.0"},"reference-count":30,"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)80019-1","type":"journal-article","created":{"date-parts":[[2008,5,29]],"date-time":"2008-05-29T10:22:56Z","timestamp":1212056576000},"page":"19-36","source":"Crossref","is-referenced-by-count":36,"title":["Only prime superpositions need be considered in the Knuth-Bendix completion procedure"],"prefix":"10.1016","volume":"6","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]},{"given":"David R.","family":"Musser","sequence":"additional","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(88)80019-1_bib1","series-title":"Critical pair criteria for the Knuth-Bendix completion procedure","author":"Bachmair","year":"1986"},{"key":"10.1016\/S0747-7171(88)80019-1_bib2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","article-title":"Non-resolution theorem proving","volume":"9","author":"Bledsoe","year":"1977","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0747-7171(88)80019-1_bib3","series-title":"Proceedings of EUROSAM 79","first-page":"3","article-title":"A criterion for detecting unnecessary reductions in the construction of Gr\u00f6bner Bases","author":"Buchberger","year":"1979"},{"key":"10.1016\/S0747-7171(88)80019-1_bib4","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","article-title":"Proving termination with multiset orderings","volume":"22\/8","author":"Dershowitz","year":"1979","journal-title":"Comm. ACM"},{"key":"10.1016\/S0747-7171(88)80019-1_bib5","series-title":"Proc. of 7th International Conference on Automated Deduction","first-page":"3","article-title":"Associative-commutative unification","author":"Fages","year":"1984"},{"key":"10.1016\/S0747-7171(88)80019-1_bib6","series-title":"Proc. of First International Conference on Rewriting Techniques and Applications","article-title":"An algebraic approach to unification under associativity and commutativity","author":"Fortenbacher","year":"1985"},{"key":"10.1016\/S0747-7171(88)80019-1_bib7","series-title":"Proceedings of an NSF Workshop on the Rewrite Rule Laboratory","year":"1984"},{"key":"10.1016\/S0747-7171(88)80019-1_bib8","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\/4","author":"Huet","year":"1980","journal-title":"J ACM"},{"key":"10.1016\/S0747-7171(88)80019-1_bib9","series-title":"21st IEEE Symposium on Foundations of Computer Science","first-page":"96","article-title":"Proofs by induction in equational theories with constructors","author":"Huet","year":"1980"},{"key":"10.1016\/S0747-7171(88)80019-1_bib10","series-title":"Technical Report CSL-13, Computer Science Laboratory","article-title":"A catalogue of canonical term rewriting systems","author":"Hullot","year":"1980"},{"key":"10.1016\/S0747-7171(88)80019-1_bib11","series-title":"Proc. of Principles of Programming Languages (POPL)","article-title":"Completion of a set of rules modulo a set of equations","author":"Jouannaud","year":"1984"},{"key":"10.1016\/S0747-7171(88)80019-1_bib12","series-title":"Proc. of Symposium on Logic in Computer Science","first-page":"358","article-title":"Automatic proofs by induction in equational theories without constructors","author":"Jouannaud","year":"1986"},{"key":"10.1016\/S0747-7171(88)80019-1_bib13","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","article-title":"Proof by consistency","volume":"31","author":"Kapur","year":"1987","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0747-7171(88)80019-1_bib14","series-title":"8th Intl. Conf. on Automated Deduction","article-title":"Proof by induction using test sets","author":"Kapur","year":"1986"},{"key":"10.1016\/S0747-7171(88)80019-1_bib15","first-page":"33","article-title":"Architecture of and experiments with RRL, a Rewrite Rule Laboratory","volume":"4","author":"Kapur","year":"1984","journal-title":"Comm. ACM"},{"key":"10.1016\/S0747-7171(88)80019-1_bib16","series-title":"8th Intl. Conf. on Automated Deduction","article-title":"RRL: A Rewrite Rule Laboratory","author":"Kapur","year":"1986"},{"key":"10.1016\/S0747-7171(88)80019-1_bib17","series-title":"Computational Problems in Abstract Algebras","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/S0747-7171(88)80019-1_bib18","first-page":"390","article-title":"A confluence criterion based on the generalized Newman Lemma","volume":"2","author":"K\u00fcchlin","year":"1985"},{"key":"10.1016\/S0747-7171(88)80019-1_bib19","article-title":"Canonical inference","author":"Lankford","year":"1975","journal-title":"Univ. of Texas, Math. Dept. Automatic Theorem Proving Project, Austin, Texas, Report ATP-32"},{"key":"10.1016\/S0747-7171(88)80019-1_bib20","series-title":"Report ATP-39","article-title":"Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions","author":"Lankford","year":"1977"},{"key":"10.1016\/S0747-7171(88)80019-1_bib21","series-title":"Proc. of Fourth Workshop on Automated Deduction","article-title":"The refutation completeness of blocked permutative narrowing and resolution","author":"Lankford","year":"1979"},{"key":"10.1016\/S0747-7171(88)80019-1_bib22","article-title":"Computer experiments with the REVE term rewriting system generator","author":"Lescanne","year":"1983","journal-title":"Proc. of 10th Principles of Programming Languages (POPL)"},{"key":"10.1016\/S0747-7171(88)80019-1_bib23","article-title":"On proving inductive properties of abstract data types","author":"Musser","year":"1980","journal-title":"Proc. 7th Principles of Programming Languages (POPL)"},{"key":"10.1016\/S0747-7171(88)80019-1_bib24","doi-asserted-by":"crossref","DOI":"10.1109\/TSE.1980.230459","article-title":"Abstract data types in the AFFIRM system","author":"Musser","year":"1980","journal-title":"IEEE Trans, on Software Engineering, SE-6\/1"},{"key":"10.1016\/S0747-7171(88)80019-1_bib25","series-title":"Computer Algebra, EUROCAM, 1982","first-page":"77","article-title":"Rewrite rule theory and abstract data type analysis","author":"Musser","year":"1982"},{"key":"10.1016\/S0747-7171(88)80019-1_bib26","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reductions for some equational theories","volume":"28\/2","author":"Peterson","year":"1981","journal-title":"J ACM"},{"key":"10.1016\/S0747-7171(88)80019-1_bib27","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","article-title":"Automated theorem proving for theories with simplifiers, commutativity and associativity","volume":"4","author":"Slagle","year":"1974","journal-title":"J. ACM"},{"issue":"3","key":"10.1016\/S0747-7171(88)80019-1_bib28","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","article-title":"A unification algorithm for associative-commutative functions","volume":"28","author":"Stickel","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/S0747-7171(88)80019-1_bib29","series-title":"Proc. of the 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"},{"key":"10.1016\/S0747-7171(88)80019-1_bib30","series-title":"Dissertation der J. Kepler-Universitaet, Linz, Austria","article-title":"The Church-Rosser property in computer algebra and special theorem proving: an investigation of critical pair, completion algorithms","author":"Winkler","year":"1984"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717188800191?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717188800191?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:36Z","timestamp":1545981876000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717188800191"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,8]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1988,8]]}},"alternative-id":["S0747717188800191"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(88)80019-1","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1988,8]]}}}