{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:17:59Z","timestamp":1725455879104},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540528504"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0018388","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T05:31:37Z","timestamp":1132637497000},"page":"296-305","source":"Crossref","is-referenced-by-count":0,"title":["On the completeness of narrowing for E-unification"],"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","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D., Proving theorems by the modification method. SIAM J. of Computing, Vol. 4, pp. 412\u2013430, 1975.","journal-title":"SIAM J. of Computing"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Dershowitz, H., Computing with rewrite rules. Information and Control, May\/June, 65, 2\/3, 1985.","DOI":"10.1016\/S0019-9958(85)80003-6"},{"key":"25_CR3","unstructured":"Fay, M.J., First-order unification in an equational theory. in 4th Workshop on Automated Deduction, pp. 161\u2013167, 1979."},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/0743-1066(84)90003-7","volume":"2","author":"L. Fribourg","year":"1984","unstructured":"Fribourg, L., Oriented equational clauses as a programming language. J. of Logic Programming, Vol 2, pp. 165\u2013177, 1984.","journal-title":"J. of Logic Programming"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Fribourg, L., A superposition oriented theorem prover. Theoretical Computer Science, Vol. 1, 1985.","DOI":"10.1016\/0304-3975(85)90011-8"},{"key":"25_CR6","unstructured":"Fribourg, L., SLOG: A logic programming language interpreter based on clausal superposition and rewriting. Proc. Symposium on Logic Programming, pp. 172\u2013184, Boston, Mass., July, 1985."},{"key":"25_CR7","unstructured":"Henschen, L., Private communication, 1985."},{"key":"25_CR8","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-16780-3_86","volume":"230","author":"J. Hsiang","year":"1986","unstructured":"Hsiang J. and M. Rusinowitch, A new method for establishing refutational completeness in theorem proving. Proc. of 8th Conference on Automated Deduction, LNCS 230, pp. 141\u2013152, 1986.","journal-title":"Proc. of 8th Conference on Automated Deduction, LNCS"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Hullot, J.M., Canonical forms and unification. Proc. 5th Conference on Automated Deduction, pp. 318\u2013334, 1980.","DOI":"10.21236\/ADA087640"},{"key":"25_CR10","unstructured":"Knuth, D. and P. Bendix, Simple word problems in universal algebras. Computational problems in abstract algebra, ed. J. Leech, pp. 163\u2013279, Pergamon Press, 1970."},{"key":"25_CR11","volume-title":"Automated theorem proving: a logical basis","author":"D.W. Loveland","year":"1978","unstructured":"Loveland, D.W., Automated theorem proving: a logical basis, Norther-Holland, New York, 1978."},{"key":"25_CR12","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08531-9","volume-title":"Computing in systems described by equations","author":"M. O'Donnell","year":"1977","unstructured":"O'Donnell, M., Computing in systems described by equations. LNCS 58, Springer-Verlag, New York, 1977."},{"issue":"1","key":"25_CR13","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G.E. Peterson","year":"1983","unstructured":"Peterson, G.E., A technique for establishing completeness results in theorem proving with equality. SIAM J. of Computing, Vol. 12, No. 1, pp.82\u2013100, 1983.","journal-title":"SIAM J. of Computing"},{"key":"25_CR14","unstructured":"Plotkin, G., Building-in equational theories. Machine Intelligence 7, pp. 73\u201390, Edinburgh University Press, 1972."},{"key":"25_CR15","unstructured":"Reddy, U., Narrowing as the operational semantics of functional languages. Proc. Symposium on Logic Programming, pp. 138\u2013151, Boston, Mass., July, 1985."},{"key":"25_CR16","series-title":"Machine Intelligence","first-page":"135","volume-title":"Paramodulation and theorem-proving in first order theories with equality","author":"G. Robinson","year":"1969","unstructured":"Robinson, G. and L. Wos, Paramodulation and theorem-proving in first order theories with equality. Machine Intelligence 4, B. Meltzer and D. Michie, eds., Edinburgh University Press, Edinburgh, 1969, pp. 135\u2013150."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Siekmann, J., Universal unification, Proc. 7th International Conference on Automated Deduction, pp. 1\u201342, Napa, Califomia, May, 1984.","DOI":"10.1007\/978-0-387-34768-4_1"},{"key":"25_CR18","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/BF00248250","volume":"2","author":"J.-H. You","year":"1986","unstructured":"You, J.-H. and P.A. Subrahmanyam, A class of confluent term rewriting systems and unification. J. Automated Reasoning Vol. 2, 391\u2013418, 1986.","journal-title":"J. Automated Reasoning"},{"key":"25_CR19","unstructured":"You, J.-H., Unification Modulo an Equality Theory for Equational Logic Programming. To appear in J. Computer and System Sciences."}],"container-title":["Lecture Notes in Computer Science","Knowledge Based Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018388.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:41:22Z","timestamp":1607550082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018388"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540528504"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0018388","relation":{},"subject":[]}}