{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T05:30:16Z","timestamp":1768282216751,"version":"3.49.0"},"reference-count":35,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"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":7868,"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":[[1992,1]]},"DOI":"10.1016\/0747-7171(92)90007-q","type":"journal-article","created":{"date-parts":[[2004,12,9]],"date-time":"2004-12-09T22:58:50Z","timestamp":1102633130000},"page":"81-100","source":"Crossref","is-referenced-by-count":4,"title":["Some experiments with a completion theorem prover"],"prefix":"10.1016","volume":"13","author":[{"given":"Ursula","family":"Martin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Lai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0747-7171(92)90007-Q_BIB1","series-title":"3rd Inter. Conf., RTA-89, Proceedings","first-page":"533","article-title":"SbReve2: A Term Rewriting Laboratory with (AC-)Unfailing Completion","author":"Anantharaman","year":"1989"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB2","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1016\/0001-8708(78)90010-5","article-title":"The diamond lemma for ring theory","volume":"29","author":"Bergman","year":"1978","journal-title":"Adv Math"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(87)80020-2","article-title":"History and Basic Features of the Critical-Pair Completion Procedure","volume":"3","author":"Buchberger","year":"1987","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB4","series-title":"The Geometry of Rewriting Systems","author":"Brown","year":"1989"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB5","series-title":"Proceedings of the Conference on Topology in Low Dimensions","article-title":"Higher Dimensional Group Theory","author":"Brown","year":"1979"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB6","series-title":"A Language for Group Theory","author":"Canon","year":"1982"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of Rewriting","volume":"3","author":"Dershowits","year":"1987","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB8","author":"Dick","year":"1988"},{"key":"10.1016\/0747-7171(92)90007-Q_NEWBIB35","unstructured":"D. B. A. Epstein, D. F. Holt and S. E. Rees, The use of Knuth-Bendix methods to solve the word problem in automatic groups, to appear, Journal of Symbolic Computation"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB9","series-title":"3rd Inter. Conf., RTA-89, Proceedings","article-title":"The Larch Prover, Lecture Notes in Computer Science","author":"Garland","year":"1989"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB10","series-title":"The Theory of Groups","author":"Hall","year":"1959"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB11","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1093\/comjnl\/34.1.20","article-title":"Implementations of Term Rewriting Systems","volume":"34","author":"Hermann","year":"1991","journal-title":"Computer Journal"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB12","first-page":"33","article-title":"The word problem for one-relator semigroups","volume":"99","author":"Howie","year":"1986"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB13","series-title":"Formal Languages: Perspectives and Open Problems","article-title":"Equations and Rewrite Rules \u2014 a survey","author":"Huet","year":"1980"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB14","first-page":"433","article-title":"Some one relator semigroups with soluble word problems","volume":"99","author":"Jackson","year":"1986"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB15","article-title":"Confluent String Rewriting","volume":"Vol. 14","author":"Jantsen","year":"1988"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB16","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0085406","article-title":"Topics in the theory of group presentations","volume":"42","author":"Johnson","year":"1979","journal-title":"London Mathematical Society Lecture Note Series"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB17","article-title":"A case study of the completion procedure: proving ring commutstivity problems","author":"Kapur","year":"1989"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB18","series-title":"Computational Problems in Abstract Algebra","article-title":"Simple Word Problems in Universal Algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB19","first-page":"331","article-title":"Proving equivalence of different axiomatisations of free groups","author":"Kapur","year":"1988","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB20","series-title":"3rd Inter. Conf., RTA-89, Proceedings","article-title":"An Overview of the Rewrite Rule Laboratory (RRL)","volume":"355","author":"Kapur","year":"1989"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB21","series-title":"8th Intl. Conf. on Automated Deduction","article-title":"RRL: A Rewrite Rule Laboratory","volume":"230","author":"Kapur","year":"1986"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB22","series-title":"7th International Conference on Automated Deduction","article-title":"Canonical Forms in Finitely presented Algebras","volume":"170","author":"Le Chenadec","year":"1984"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB23","series-title":"7th International Conference on Automated Deduction","article-title":"Term Rewriting Systems and Algebra","volume":"170","author":"Lescanne","year":"1984"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB24","article-title":"The Automated Reasoning System ITP","author":"Lusk","year":"1984","journal-title":"Argonne National laboratory ANL-84-27"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB25","series-title":"Doing Algebra with REVE","author":"Martin","year":"1986"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB26","doi-asserted-by":"crossref","DOI":"10.1007\/BF01188513","article-title":"Proving a group infinite","author":"Newman","year":"1988"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB27","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1098\/rsta.1954.0007","article-title":"An essay on free products with amalgamations","volume":"246","author":"Neumann","year":"1954","journal-title":"Phil Trans Royal Soc London Ser A"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB28","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1017\/S0004972700006912","article-title":"Another single law for groups","volume":"23","author":"Neumann","year":"1981","journal-title":"hBull Austr Math Soc"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB29","series-title":"seminar at the University of Oxford","author":"Neumann","year":"1986"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB30","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/S0747-7171(87)80002-0","article-title":"Verifying Nilpotence","volume":"3","author":"Sims","year":"1987","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB31","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00243209","article-title":"Some experiments in non-associative ring theory with an automated theorem prover","volume":"3","author":"Stevens","year":"1987","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB32","series-title":"Automated Reasoning: 33 Basic Research Problems","author":"Woo","year":"1988"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB33","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1090\/conm\/029\/05","article-title":"Open questions solved with the assistance of AURA","volume":"29","author":"Woo","year":"1984","journal-title":"Contemporary Mathematics"},{"key":"10.1016\/0747-7171(92)90007-Q_BIB34","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/BF02090774","article-title":"Unnecessary inferences in associative-commutative completion procedures","volume":"23","author":"Zhang","year":"1990","journal-title":"J Math System Theory"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:074771719290007Q?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:074771719290007Q?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T00:26:52Z","timestamp":1548980812000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/074771719290007Q"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,1]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,1]]}},"alternative-id":["074771719290007Q"],"URL":"https:\/\/doi.org\/10.1016\/0747-7171(92)90007-q","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1992,1]]}}}