{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T11:47:58Z","timestamp":1757591278629},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bf00881872","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T23:44:45Z","timestamp":1104191085000},"page":"333-351","source":"Crossref","is-referenced-by-count":6,"title":["Automated proofs of equality problems in Overbeek's competition"],"prefix":"10.1007","volume":"11","author":[{"given":"Hantao","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00302643","volume":"6","author":"S. Anantharaman","year":"1990","unstructured":"Anantharaman, S. and Hsiang, J., ?Automated proofs of the Moufang identities in alternative rings?,J. Automated Reasoning 6 79?109 (1990).","journal-title":"J. Automated Reasoning"},{"key":"CR2","unstructured":"Bonacina, M. P., ?Problems in Lukasiewicz logic?,AAR Newsletter, No. 18 (1991)."},{"key":"CR3","first-page":"548","volume":"355","author":"J. Christian","year":"1989","unstructured":"Christian, J., ?Fast Knuth-Bendix completion: summary?,Proc. Third International Conference of Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 355, Springer-Verlag, pp. 548?610 (1989).","journal-title":"Proc. Third International Conference of Rewriting Techniques and Applications, Lecture Notes in Computer Science"},{"key":"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., ?Termination of rewriting?,J. Symbolic Computation 3 69?116 (1987).","journal-title":"J. Symbolic Computation"},{"key":"CR5","unstructured":"Dershowitz, N. and Jouannaud, J. P., ?Rewriting systems?, in Leuven, V. (Ed.),Handbook of Theoretical Computer Science, North Holland (1990)."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Knuth, D. E. and Bendix, P. B., ?Simple word problems in universal algebras?, in Leech, J. (Ed.),Computational Problems in Abstract Algebras, Pergamon Press, pp. 263?297 (1970).","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Kapur, D., Sivakumar, G. and Zhang, H., ?A new method for proving termination of AC-rewrite systems?,Proc. 10th Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, India (1990).","DOI":"10.1007\/3-540-53487-3_40"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1007\/3-540-51081-8_129","volume":"355","author":"D. Kapur","year":"1989","unstructured":"Kapur, D. and Zhang, H., ?An overview of RRL: Rewrite Rule Laboratory?,Proc. of the Third International Conference on Rewriting Techniques and Its Applications, Lecture Notes in Computer Science, Vol. 355, Springer-Verlag, pp. 513?529 (1989).","journal-title":"Proc. of the Third International Conference on Rewriting Techniques and Its Applications"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BF00244946","volume":"4","author":"D. Kapur","year":"1988","unstructured":"Kapur, D. and Zhang, H., ?Proving equivalence of different axiomatizations of free groups?,J. Automated Reasoning 4 331?352 (1988).","journal-title":"J. Automated Reasoning"},{"key":"CR10","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"D. Kapur","year":"1991","unstructured":"Kapur, D. and Zhang, H., ?A case study of the completion procedure: Proving ring commutativity problems?, in Lassez, J.-L. and Plotkin, G. (Eds.),Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, Mass. (1991)."},{"key":"CR11","first-page":"209","volume":"1","author":"E. L. Lusk","year":"1985","unstructured":"Lusk, E. L. and Overbeek, R. A., ?Reasoning about equality?,J. Automated Reasoning 1, 209?228 (1985).","journal-title":"J. Automated Reasoning"},{"key":"CR12","unstructured":"Martin, U., ?Doing algebra with REVE?,Technical Report UMCS-86-10-4, Dept. of Computer Science, University of Manchester (1986)."},{"key":"CR13","series-title":"Technical Report","volume-title":"OTTER 2.0 Users' Guide","author":"W. McCune","year":"1990","unstructured":"McCune, W.,OTTER 2.0 Users' Guide.Technical Report, ANL-90\/9, Argonne National Laboratory, Argonne, Illinois (1990)."},{"issue":"2","key":"CR14","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W., ?Experiments with discrimination-tree indexing and path indexing for term retrieval?,J. Automated Reasoning 9 (2), 147?168 (1992).","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"CR15","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BF00381147","volume":"3","author":"W. McCune","year":"1987","unstructured":"McCune, W. and Wos, L., ?A case study in automated theorem proving: Finding sages in combinatory logic?,J. Automated Reasoning 3 (1), 91?108 (1987).","journal-title":"J. Automated Reasoning"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1017\/S0004972700006912","volume":"23","author":"B. H. Neumann","year":"1981","unstructured":"Neumann, B. H., ?Another single law for groups?,Bull. Austr. Math. Soc. 23 81?102 (1981).","journal-title":"Bull. Austr. Math. Soc."},{"key":"CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/3-540-52885-7_101","volume-title":"Proc. 10th International Conference on Automated Deduction","author":"G.L. Peterson","year":"1990","unstructured":"Peterson, G.L., ?Complete sets of reductions with constriants?,Proc. 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 449, Springer-Verlag, Berlin, pp. 381?395 (1990)."},{"issue":"2","key":"CR18","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. L. Peterson","year":"1981","unstructured":"Peterson, G. L. and Stickel, M. E., ?Complete sets of reductions for some equational theories?,J. ACM 28 (2), 233?264 (1981).","journal-title":"J. ACM"},{"key":"CR19","first-page":"248","volume":"170","author":"M. Stickel","year":"1984","unstructured":"Stickel, M., ?A case study of theorem proving by the Knuth-Bendix method: Discovering thatx 3=x implies ring commutativity?,Proc. 7th Conf. on Automated Deduction, Lecture Notes in Computer Science, Vol. 170, Springer-Verlag, pp. 248?258 (1984).","journal-title":"Proc. 7th Conf. on Automated Deduction"},{"key":"CR20","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.2172\/6898399","volume-title":"Canonicalization and demodulation","author":"R. Veroff","year":"1981","unstructured":"Veroff, R., ?Canonicalization and demodulation?,Technical Report ANL-81-6, Argonne National Laboratory, Argonne, Illinois (1981)."},{"key":"CR21","first-page":"437","volume":"3","author":"T. C. Wang","year":"1987","unstructured":"Wang, T. C., ?Case studies of Z-module reasoning: Proving benchmark theorems from ring theory?,J. Automated Reasoning 3 437?451 (1987).","journal-title":"J. Automated Reasoning"},{"key":"CR22","first-page":"141","volume":"5","author":"T. C. Wang","year":"1989","unstructured":"Wang, T. C. and Stevens, R., ?Solving open problems in right alternative rings with Z-module reasoning?,J. Automated Reasoning 5 141?165 (1989).","journal-title":"J. Automated Reasoning"},{"issue":"4","key":"CR23","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00244359","volume":"6","author":"S. Winker","year":"1990","unstructured":"Winker, S., ?Robbins algebra: Conditions that make a near-Boolean algebra Boolean?,J. Automated Reasoning 6 (4), 465?489 (1990).","journal-title":"J. Automated Reasoning"},{"key":"CR24","unstructured":"Winkler, S. and Wos, L., ?Automated generation of models and counterexamples and its application to open questions in ternary Boolean algebra?, in:Proc. Eighth International Symposium on Multiple-Valued Logic. Rosemont, Ill., pp. 251?256 (1978)."},{"key":"CR25","unstructured":"Wos, L., ?New challenge problem in sentential calculus?,AAR Newsletter, No. 16 (1990)."},{"key":"CR26","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.2172\/6852789","volume-title":"Searching for fixed point combinators by using automated theorem proving: A preliminary report","author":"L. Wos","year":"1988","unstructured":"Wos, L. and McCune, W., ?Searching for fixed point combinators by using automated theorem proving: A preliminary report?,Technical Report ANL-88-10, Argonne National Laboratory, Argonne, Illinois (1988)."},{"key":"CR27","volume-title":"Automated reasoning: Introduction and applications","author":"L. Wos","year":"1992","unstructured":"Wos, L., Overbeek, R., Lusk, E. and Boyle, J., ?Automated reasoning: Introduction and applications?, 2nd edn., McGraw-Hill, New York (1992).","edition":"2nd edn."},{"key":"CR28","unstructured":"Zhang, H., ?Criteria of critical pair criteria: A practical approach and a comparative study?,Internal Report, Dept. of Computer Science, University of Iowa (1991)."},{"key":"CR29","unstructured":"Zhang, H., ?Herky: High-performance rewriting techniques in RRL; in Kapur, D. (Ed.),Proc. 1992 International Conference of Automated Deduction, Lecture Notes in Artificial Intelligence, Springer-Verlag, pp. 696?700 (1992)."},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"Zhang, H., ?A case study of completion modulo distributivity and Abelian groups?, in Kirchner, C. (Ed.).Proc. International Conference on Rewrite Techniques and Applications, Lecture Notes in Computer Science, Vol. 690, Springer-Verlag, pp. 32?46 (1993).","DOI":"10.1007\/3-540-56868-9_4"},{"key":"CR31","volume-title":"Rings That are Nearly Associative","author":"K. A. Zhevlakov","year":"1982","unstructured":"Zhevlakov, K. A.et al., Rings That are Nearly Associative (Tr. by H. F. Smith from the Russian), Academic Press, New York (1982)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881872.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881872\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881872","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T00:16:22Z","timestamp":1586045782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881872"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881872"],"URL":"https:\/\/doi.org\/10.1007\/bf00881872","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}