{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:51:29Z","timestamp":1725663089223},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540194880"},{"type":"electronic","value":"9783540392910"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-19488-6_153","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:15:05Z","timestamp":1330200905000},"page":"727-741","source":"Crossref","is-referenced-by-count":1,"title":["Outer narrowing for equational theories based on constructors"],"prefix":"10.1007","author":[{"given":"Jia-Huai","family":"You","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"51_CR1","doi-asserted-by":"crossref","unstructured":"Burckert, H., A. Herold and M. Schmidt-Schau\u03b2, \u201cOn equational theories, unification and decidability,\u201d in Proc. of RTA'87, LNCS 256, 1987.","DOI":"10.1007\/3-540-17220-3_18"},{"key":"51_CR2","doi-asserted-by":"crossref","unstructured":"Burstall, R.M. and D.T. Sannella,, \u201cHOPE user's manual,\u201d Dept. of Computer Science, University of Edinburgh, 1980.","DOI":"10.1145\/800087.802799"},{"key":"51_CR3","unstructured":"Dershowitz, H. and D. Plaited, \u201cLogic programming cum applicative programming,\u201d in Proc. 1985 International Symposium on Logic Programming, pp. 54\u201367, Boston, Mass., July, 1985."},{"key":"51_CR4","doi-asserted-by":"crossref","unstructured":"Dershowitz, H., \u201cComputing with rewrite rules,\u201d Information and Control, Vol. 65 No.2\/3, May\/June 1985.","DOI":"10.1016\/S0019-9958(85)80003-6"},{"key":"51_CR5","doi-asserted-by":"crossref","unstructured":"Dincbas, M. and P. van Hentenryck, \u201cExtended unification algorithms for the integration of functional programming into logic programming,\u201d Journal of Logic Programming, 1987.","DOI":"10.1016\/0743-1066(87)90002-1"},{"key":"51_CR6","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/3-540-12727-5_12","volume":"159","author":"F Fages","year":"1983","unstructured":"Fages, F and G. Huet, \u201cUnification and matching in equational theories,\u201d in Proc. CAAP '83, LNCS 159, pp. 205\u2013220, 1983.","journal-title":"Proc. CAAP '83, LNCS"},{"key":"51_CR7","unstructured":"Fay, M.J., \u201cFirst-order unification in an equational theory,\u201d in 4th Workshop on Automated Deduction, pp. 161\u2013167, 1979."},{"key":"51_CR8","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."},{"key":"51_CR9","first-page":"216","volume":"256","author":"J.H. Gallier","year":"1987","unstructured":"Gallier J.H. and Wayne Snyder, \u201cA general complete E-unification procedure,\u201d in Proc. of RTA '87, LNCS 256, pp. 216\u2013227, 1987.","journal-title":"Proc. of RTA '87, LNCS"},{"key":"51_CR10","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0743-1066(84)90004-9","volume":"2","author":"J. Goguen","year":"1984","unstructured":"Goguen, J. and J. Meseguer, \u201cEquality, types, modules and generics for logic programming,\u201d Journal of Logic Programming, Vol 2. 1984, pp 179\u2013210.","journal-title":"Journal of Logic Programming"},{"issue":"1","key":"51_CR11","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":"51_CR12","series-title":"Technical Report","volume-title":"Call by need computations in nonambiguous linear term rewriting systems","author":"G. Huet","year":"1979","unstructured":"Huet, G. and J-J. Levy, \u201cCall by need computations in nonambiguous linear term rewriting systems,\u201d Technical Report, 359, INRIA, Le Chesnay, France, 1979."},{"key":"51_CR13","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal Language Theory: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"Huet, G. and D.C. Oppen, \u201cEquations and rewrite rules: a survey,\u201d in Formal Language Theory: Perspectives and Open Problems, R.V. Book (ed.), pp. 349\u2013405, Academic Press, New York, 1980."},{"key":"51_CR14","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.21236\/ADA087640"},{"key":"51_CR15","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.P., C. Kirchner and H. Kirchner, \u201cIncremental construction of unification procedures in equational theories,\u201d in Proc. 10th Colloquium on Automata, Languages and Programming, 1983.","DOI":"10.1007\/BFb0036921"},{"key":"51_CR16","unstructured":"Lankford, D.S., \u201cCanonical inference,\u201d Technical Report ATP-32, Department of Mathematics and Computer Science, University of Texas at Austin, December, 1975."},{"issue":"2","key":"51_CR17","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., and U. Montanari, \u201cAn efficient unification algorithm\u201d, ACM Transaction on Programming Languages and Systems, Vol. 4, No. 2, pp. 258\u2013282, 1982.","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"51_CR18","unstructured":"Martelli, A., C. Moiso and G.F. Rossi \u201cAn algorithm for unification in equational theories\u201d, in Proc. 1986 International Symposium on Logic Programming, pp. 180\u2013186, Salt Lake City, Utah, 1986."},{"key":"51_CR19","doi-asserted-by":"crossref","unstructured":"Milner, R., \u201cA proposal for standard ML\u201d in Proc. of 1984 ACM Symposium on Lisp and Functional Programming, pp. 184\u2013197, August 1984.","DOI":"10.1145\/800055.802035"},{"key":"51_CR20","unstructured":"Nutt, Werner, Rierre Rety and Gert Smolka, \u201cBasic narrowing revisited,\u201d Technical Report SR-87-07, Universitat Kaiserslautern, 1987."},{"key":"51_CR21","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 Lecture notes in computer science, vol. 58, Springer-Verlag, New York, 1977."},{"key":"51_CR22","volume-title":"Equational Logic as a Programming Language","author":"M. O'Donnell","year":"1985","unstructured":"O'Donnell, M., \u201cEquational Logic as a Programming Language,\u201d The MIT Press, Cambridge, Massachusetts, 1985."},{"key":"51_CR23","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G., \u201cBuilding-in equational theories,\u201d in Machine Intelligence 7, pp. 73\u201390, Edinburgh University Press, 1972.","journal-title":"Machine Intelligence"},{"key":"51_CR24","unstructured":"Reddy, U., \u201cNarrowing as the operational semantics of functional languages,\u201d in Proc. 1985 International Symposium on Logic Programming, pp. 138\u2013151, Boston, Mass., July, 1985."},{"key":"51_CR25","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, also in Lecture Notes in Computer Science"},{"key":"51_CR26","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/3-540-17220-3_20","volume":"256","author":"P. Rety","year":"1987","unstructured":"Rety P., \u201cImproving basic narrowing techniques,\u201d in Proc. Rewriting Techniques and Applications, Lecture Notes in Computer Science 256, pp. 228\u2013241, 1987.","journal-title":"Proc. Rewriting Techniques and Applications, Lecture Notes in Computer Science"},{"key":"51_CR27","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"},{"issue":"4","key":"51_CR28","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J.R. Slagle","year":"1974","unstructured":"Slagle, J.R., \u201cAutomated theorem proving for theories with simplifier, commutativity, and associativity,\u201d Journal of ACM, Vol. 21, No. 4, October 1974, pp. 622\u2013642.","journal-title":"Journal of ACM"},{"key":"51_CR29","unstructured":"Turner, D.A., \u201cSASL language manual,\u201d University of St. Andrews, 1979."},{"key":"51_CR30","doi-asserted-by":"crossref","unstructured":"You, J.-H. and P.A. Subrahmanyam, \u201cEquational logic programming: an extension to equational programming,\u201d in Proc. ACM 13th POPL, pp. 209\u2013218, St. Petersburg, Florida, January, 1986.","DOI":"10.1145\/512644.512663"},{"key":"51_CR31","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, \u201cA class of confluent term rewriting systems and unification,\u201d in Journal of Automated Reasoning Vol. 2 (1986) 391\u2013418.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-19488-6_153.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:17:34Z","timestamp":1605644254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-19488-6_153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540194880","9783540392910"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-19488-6_153","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}