{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:29Z","timestamp":1725456209268},"publisher-location":"Berlin\/Heidelberg","reference-count":12,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012821","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"21-40","source":"Crossref","is-referenced-by-count":0,"title":["Elements of Z-module reasoning"],"prefix":"10.1007","author":[{"given":"Tie Cheng","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"W. W. Bledsoe, \u201cNon-resolution theorem proving,\u201d Artificial Intelligence (9), pp. 1\u201335, 1977.","journal-title":"Artificial Intelligence"},{"key":"2_CR2","unstructured":"E. Lusk and R. Overbeek, \u201cThe automated reasoning system ITP\u201d, ANL-84-27, Argonne National Laboratory (April, 1984)."},{"issue":"1","key":"2_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00381147","volume":"3","author":"W. McCune","year":"1987","unstructured":"W. McCune and L. Wos, \u201cA case study in automated theorem proving: searching for sages in combinatory logic,\u201d Journal of Automated Reasoning, 3(1) pp. 91\u2013107 (1987).","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR4","doi-asserted-by":"crossref","first-page":"939","DOI":"10.1090\/S0002-9939-1953-0059888-X","volume":"4","author":"E. Kleinfeld","year":"1953","unstructured":"E. Kleinfeld, \u201cRight alternative rings,\u201d Proc. Amer. Math. Soc., Vol. 4, pp. 939\u2013944 (1953).","journal-title":"Proc. Amer. Math. Soc."},{"issue":"2","key":"2_CR5","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00243209","volume":"3","author":"R. L. Stevens","year":"1987","unstructured":"R. L. Stevens, \u201cSome experiments in nonassociative ring theory with an automated theorem prover,\u201d Journal of Automated Reasoning, 3(2) PP. 211\u2013223 (1987).","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0021-8693(75)90086-1","volume":"1","author":"A. Thedy","year":"1975","unstructured":"A. Thedy, \u201cRight alternative rings\u201d, Journal of Algebra, Vol. 1, pp. 1\u201343 (1975).","journal-title":"Journal of Algebra"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"M. E. Stickel, \u201cA Unification Algorithm for associative commutative functions,\u201d J. ACM, Vol. 28, No. 3, pp 423\u20134343.","DOI":"10.1145\/322261.322262"},{"issue":"1","key":"2_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/BF00381144","volume":"3","author":"T. C. Wang","year":"1987","unstructured":"T. C. Wang and W. W. Bledsoe, \u201cHierarchical Deduction\u201d, Journal of Automated Reasoning, Vol. 3, No. 1, pp. 35\u201371 (1987).","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"2_CR9","first-page":"437","volume":"3","author":"T. C. Wang","year":"1987","unstructured":"T. C. Wang, \u201cCase studies of Z-module reasoning: proving benchmark theorems from ring theory,\u201d Journal of Automated Reasoning, Vol. 3, No. 4, pp. 437\u2013451 (1987).","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR10","unstructured":"T. C. Wang and R. Stevens, \u201cSolving open problems in right alternative rings with Z-module reasoning,\u201d Submitted for publication."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"L. Wos, and W. W. McCune,, \u201cSearching for Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report,\u201d ANL-88-10 (1988).","DOI":"10.2172\/6852789"},{"key":"2_CR12","volume-title":"Rings that are nearly associative","author":"K. A. Zhevlakov","year":"1982","unstructured":"K. A. Zhevlakov, et al., \u201cRings that are nearly associative,\u201d Academic Press, New York, 1982."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012821","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:23:50Z","timestamp":1586579030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0012821","relation":{},"subject":[]}}