{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:54:37Z","timestamp":1725663277207},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540505174"},{"type":"electronic","value":"9783540460305"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-50517-2_95","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:26:58Z","timestamp":1330183618000},"page":"435-454","source":"Crossref","is-referenced-by-count":8,"title":["Semi-unification"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Musser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Stillman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0022-0000(86)90003-6","volume":"32","author":"D. Champeaux De","year":"1986","unstructured":"De Champeaux, D., \u201cAbout the Paterson-Wegman Linear Unification Algorithm,\u201d in J. of Computer and System Sciences 32, 1986, pp. 79\u201390.","journal-title":"J. of Computer and System Sciences"},{"key":"29_CR2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N., \u201cOrderings for term-rewriting systems,\u201d in Theoretical Computer Science 17, 1982, pp. 279\u2013301.","journal-title":"Theoretical Computer Science"},{"key":"29_CR3","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-15976-2_9","volume-title":"Rewriting Techniques and Applications","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N., \u201cTermination,\u201d in Rewriting Techniques and Applications, Jean-Pierre Jouannaud, ed., Springer Verlag, Berlin, 1985, pp. 180\u2013224."},{"doi-asserted-by":"crossref","unstructured":"Henglein, F., \u201cType Inference and Semi-Unification,\u201d in Proceedings, ACM Conference on LISP and Functional Programming, ACM, ACM Press, June 1988.","key":"29_CR4","DOI":"10.1145\/62678.62701"},{"unstructured":"Hsiang, J., and Dershowitz, N., \u201cRewrite methods for clausal and non-clausal theorem proving,\u201d in Proc. 10th EATCS Intl. Colloq. on Automata, Languages, and Programming, Barcelona, Spain, 1983.","key":"29_CR5"},{"key":"29_CR6","series-title":"Rapport Laboria","volume-title":"On the Uniform Halting Problem for Term Rewriting Systems","author":"G. Huet","year":"1978","unstructured":"Huet, G., and Lankford, D.S., \u201cOn the Uniform Halting Problem for Term Rewriting Systems,\u201d Rapport Laboria 283, INRIA, Paris, 1978."},{"key":"29_CR7","volume-title":"Formal Languages: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"Huet, G., and Oppen, D., \u201cEquations and rewrite rules: a survey,\u201d in Formal Languages: Perspectives and Open Problems (R. Book, ed.), Academic Press, New York, 1980."},{"doi-asserted-by":"crossref","unstructured":"Kapur, D., and Narendran, P., \u201cAn equational approach to theorem proving in first-order predicate calculus,\u201d in 9th Intl. Joint Conference on Artificial Intelligence, Los Angeles, California, 1985.","key":"29_CR8","DOI":"10.1145\/1012497.1012521"},{"doi-asserted-by":"crossref","unstructured":"Kapur, D., Sivakumar, G., and Zhang, H., \u201cRRL: a rewrite rule laboratory,\u201d in Proceedings of the 8th Intl. Conference on Automated Deduction, Oxford, U.K., 1986, LNCS 230, Springer-Verlag.","key":"29_CR9","DOI":"10.1007\/3-540-16780-3_140"},{"key":"29_CR10","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., and Bendix, P.B., \u201cSimple word problems in universal algebras,\u201d in Computational Problems in Abstract Algebra (J. Leech, ed.), Pergamon Press, Oxford, 1970, pp. 263\u2013297."},{"key":"29_CR11","first-page":"210","volume":"95","author":"J.B. Kruskal","year":"1960","unstructured":"Kruskal, J.B., \u201cWell-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture,\u201d in Transactions of the American Mathematical Society 95, 1960, pp. 210\u2013225.","journal-title":"Transactions of the American Mathematical Society"},{"key":"29_CR12","volume-title":"A finite termination criterion","author":"D.S. Lankford","year":"1978","unstructured":"Lankford, D.S., and Musser, D.R. \u201cA finite termination criterion,\u201d Unpublished Draft, USC Information Sciences Institute, Marina Del Rey, California, 1978."},{"key":"29_CR13","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M.S. Paterson","year":"1978","unstructured":"Paterson, M.S., and Wegman, M.N., \u201cLinear Unification,\u201d in J. of Computer and System Sciences 16, 1978, pp. 158\u2013167. (see also [1]).","journal-title":"J. of Computer and System Sciences"},{"key":"29_CR14","first-page":"79","volume-title":"A simple non-termination test for the Knuth-Bendix method","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., \u201cA simple non-termination test for the Knuth-Bendix method,\u201d in Proceedings of the 8th Intl. Conf. on Automated Deduction, Oxford, U.K., 1986, LNCS 230, Springer Verlag, NY, 79\u201388."},{"key":"29_CR15","first-page":"54","volume":"250","author":"P.W. Purdom Jr.","year":"1987","unstructured":"Purdom, P.W., Jr., \u201cDetecting Looping Simplifications,\u201d in Proc. 2nd Conference on Rewrite Rule Theory and Applications (RTA), Bordeaux, France, May 1987, LNCS 250, Springer-Verlag, 54\u201362.","journal-title":"LNCS"},{"volume-title":"AFFIRM Reference Manual","year":"1981","unstructured":"Thompson, D.H., and Erickson, R.W. (eds.), AFFIRM Reference Manual, USC Information Sciences Institute, Marina Del Rey, California, 1981.","key":"29_CR16"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50517-2_95.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:56:19Z","timestamp":1619556979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50517-2_95"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540505174","9783540460305"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-50517-2_95","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}