{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:51:18Z","timestamp":1725663078595},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167617"},{"type":"electronic","value":"9783540398592"}],"license":[{"start":{"date-parts":[[1986,1,1]],"date-time":"1986-01-01T00:00:00Z","timestamp":504921600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16761-7_95","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:53:18Z","timestamp":1330177998000},"page":"454-463","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["E-unification algorithms for a class of confluent term rewriting systems"],"prefix":"10.1007","author":[{"given":"Jia-Huai","family":"You","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. A.","family":"Subrahmanyam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"47_CR1","unstructured":"Fay, M.J., \u201cFirst-order unification in an equational theory,\u201d in 4th Workshop on Automated Deduction, pp. 161\u2013167, Austin, Texas, February, 1979."},{"key":"47_CR2","unstructured":"Fribourg, L., \u201cA superposition oriented theorem prover,\u201d Tech. Report 11, L.I.T.P., 1983, To appear in Theoretical Compute Science, short version in Proc. IJCAI-83, pp. 923\u2013925."},{"key":"47_CR3","unstructured":"Fribourg, L., \u201cSLOG: A logic programming language interpreter based on clausal superposition and rewriting,\u201d in Proc. 1985 International Symposium on Logic Programming, pp. 172\u2013184, Boston, Mass., July, 1985."},{"issue":"1","key":"47_CR4","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/357153.357158","volume":"4","author":"C.M. Hoffmann","year":"1982","unstructured":"Hoffmann, C.M. and M. O'Donnell, \u201cProgramming with equations,\u201d ACM TOPLAS, vol. 4, no. 1, pp. 83\u2013112, January, 1982.","journal-title":"ACM TOPLAS"},{"key":"47_CR5","doi-asserted-by":"crossref","unstructured":"Hullot, J.M., \u201cCanonical forms and unification,\u201d in Proc. 5th Conference on Automated Deduction, pp 318\u2013334, 1980.","DOI":"10.1007\/3-540-10009-1_25"},{"key":"47_CR6","doi-asserted-by":"crossref","unstructured":"Hussmann, H., \u201cUnification in conditional-equational theories,\u201d Tech. Report MIP 8502, Universitat Passau, January, 1985.","DOI":"10.1007\/3-540-15984-3_328"},{"key":"47_CR7","unstructured":"Knuth, D. and P. Bendix, \u201cSimple word problems in universal algebras,\u201d in Computational problems in abstract algebra, ed. J. Leech, pp. 163\u2013279, Pergamon Press, 1970."},{"key":"47_CR8","unstructured":"Jouannaud, J.P., C. Kirchner and H. Kirchner, \u201cIncremental construction of unification algorithms in equational theories,\u201d in Proc. 10th Colloquium on Automata, Languages and Programming, 1983."},{"key":"47_CR9","unstructured":"Lankford, D.S., \u201cCanonical inference,\u201d Technical Report ATP-32, Department of Mathematics and Computer Science, University of Texas at Austin, December, 1975."},{"key":"47_CR10","unstructured":"Plotkin, G., \u201cBuilding-in equational theories,\u201d in Machine Intelligence 7, pp. 73\u201390, Edinburgh University Press, 1972."},{"key":"47_CR11","volume-title":"Lecture notes in computer science, vol. 58","author":"M. O'Donnell","year":"1977","unstructured":"O'Donnell, M., \u201cComputing in systems described by equations,\u201d in Lecture notes in computer science, vol. 58, Springer-Verlag, New York, 1977."},{"key":"47_CR12","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-15976-2_7","volume":"202","author":"P Rety","year":"1985","unstructured":"Rety P, C. Kirchner, H. Kirchner and P. Lescanne, \u201cNARROWER: a new algorithm and its application to logic programming,\u201d in Proc. Rewriting Techniques and Applications, also in Lecture Notes in Computer Science 202, pp. 141\u2013157, 1985.","journal-title":"Proc. Rewriting Techniques and Applications"},{"issue":"1","key":"47_CR13","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A., \u201cA machine oriented logic based on the resolution,\u201d in Journal of ACM, vol 12, no. 1 pp. 23\u201341, January, 1965.","journal-title":"Journal of ACM"},{"key":"47_CR14","doi-asserted-by":"crossref","unstructured":"Siekmann, J., \u201cUniversal unification,\u201d in Proc. 7th International Conference on Automated Deduction, pp. 1\u201342, Napa, California, May, 1984.","DOI":"10.1007\/978-0-387-34768-4_1"},{"key":"47_CR15","unstructured":"Subrahmanyam, P.A. and Jia-Huai You, \u201cFUNLOG: a computational model integrating logic programming and functional programming,\u201d in Logic programming: relations, functions and equations, eds. D. DeGroot and G. Lindstrom, Prentice-Hall, 1986."},{"key":"47_CR16","unstructured":"You, J.-H. and P.A. Subrahmanyam, \u201cA class of term rewriting systems and unification,\u201d unpublished manuscript, 1985."},{"key":"47_CR17","doi-asserted-by":"crossref","unstructured":"You, J.-H. and P.A. Subrahmanyam, \u201cEquational logic programming: an extension to equational programming,\u201d in Proc. 13th POPL, pp. 209\u2013218, St. Petersburg, Florida, January, 1986.","DOI":"10.1145\/512644.512663"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16761-7_95","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:10:34Z","timestamp":1558253434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16761-7_95"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167617","9783540398592"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-16761-7_95","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}