{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:32:38Z","timestamp":1742635958115,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540592938"},{"type":"electronic","value":"9783540492337"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59293-8_209","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:12:19Z","timestamp":1330276339000},"page":"394-408","source":"Crossref","is-referenced-by-count":4,"title":["Lazy narrowing: Strong completeness and eager variable elimination (extended abstract)"],"prefix":"10.1007","author":[{"given":"Satoshi","family":"Okui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tetsuo","family":"Ida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"26_CR1","first-page":"462","volume":"607","author":"L. Bachmair","year":"1992","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder, Basic Paramodulation and Superposition, Proc. 11th CADE, LNCS 607, pp. 462\u2013476, 1992.","journal-title":"Proc. 11th CADE, LNCS"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, in: Handbook of Theoretical Computer Science, Vol. B, ed. J. van Leeuwen), North-Holland, pp. 243\u2013320, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"8","key":"26_CR3","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz and Z. Manna, Proving Termination with Multiset Orderings, Communications of the ACM 22(8), pp. 465\u2013476, 1979.","journal-title":"Communications of the ACM"},{"key":"26_CR4","unstructured":"M. Fay, First-Order Unification in Equational Theories, Proc. 4th CADE, Austin, pp. 161\u2013167, 1979."},{"key":"26_CR5","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. Gallier","year":"1989","unstructured":"J. Gallier and W. Snyder, Complete Sets of Transformations for General E-Unification, TCS 67, pp. 203\u2013260, 1989.","journal-title":"TCS"},{"key":"26_CR6","first-page":"344","volume":"567","author":"M. Hanus","year":"1991","unstructured":"M. Hanus, Efficient Implementation of Narrowing and Rewriting, Proc. PDK-91, LNAI 567, pp. 344\u2013365, 1991.","journal-title":"Proc. PDK-91, LNAI"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"M. Hanus, The Integration of Functions into Logic Programming: From Theory to Practice, JLP 19 & 20, pp. 583\u2013628, 1994.","DOI":"10.1016\/0743-1066(94)90034-5"},{"key":"26_CR8","first-page":"31","volume":"267","author":"S. H\u00f6lldobler","year":"1987","unstructured":"S. H\u00f6lldobler, A Unification Algorithm for Conflnent Theories, Proc. 14th ICALP, LNCS 267, pp. 31\u201341, 1987.","journal-title":"Proc. 14th ICALP, LNCS"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"S. H\u00f6lldobler, Foundations of Equational Logic Programming, LNAI 353, 1989.","DOI":"10.1007\/BFb0015791"},{"key":"26_CR10","unstructured":"G. Huet and J.-J. L\u00e9vy, Computations in Orthogonal Rewriting Systems, I and II, in: Computational Logic, Essays in Honor of Alan Robinson (eds. J.-L. Lassez and G. Plotkin), The MIT Press, pp. 396\u2013443, 1991."},{"key":"26_CR11","first-page":"318","volume":"87","author":"J.-M. Hullot","year":"1980","unstructured":"J.-M. Hullot, Canonical Forms and Unification, Proc. 5th CADE, LNCS 87, pp. 318\u2013334, 1980.","journal-title":"Proc. 5th CADE, LNCS"},{"key":"26_CR12","unstructured":"J.W. Klop, Term Rewriting Systems, in: Handbook of Logic in Computer Science, Vol. II (eds. S. Abramsky, D. Gabbay, and T. Maibaum), Oxford University Press, pp. 1\u2013116, 1992."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"A. Martelli, C. Moiso, and G.F. Rossi, Lazy Unification Algorithms for Canonical Rewrite Systems, in: Resolution of Equations in Algebraic Structures, Vol. II (eds. H. A\u00eft-Kaci and M. Nivat), Academic Press, pp. 245\u2013274, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50014-6"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari, An Efficient Unification Algorithm, ACM TOPLAS 4(2), pp. 258\u2013282, 1982.","journal-title":"ACM TOPLAS"},{"key":"26_CR15","unstructured":"A. Martelli, G.F. Rossi, and C. Moiso, An Algortihm for Unification in Equational Theories, Proc. 1986 Symposium on Logic Programming, pp. 180\u2013186, 1986."},{"key":"26_CR16","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01190830","volume":"5","author":"A. Middeldorp","year":"1994","unstructured":"A. Middeldorp and E. Hamoen, Completeness Results for Basic Narrowing, AAECC 5, pp. 213\u2013253, 1994.","journal-title":"AAECC"},{"key":"26_CR17","first-page":"92","volume":"690","author":"M. Moser","year":"1993","unstructured":"M. Moser, Improving Transformation Systems for General E-Unification, Proc. 5th RTA, LNCS 690, pp. 92\u2013105, 1993.","journal-title":"Proc. 5th RTA, LNCS"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"S. Okui, A. Middeldorp, and T. Ida, Lazy Narrowing: Strong Completeness and Eager Variable Elimination, Report ISE-TR-94-114, University of Tsukuba, 1994.","DOI":"10.1007\/3-540-59293-8_209"},{"key":"26_CR19","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J.R. Slagle","year":"1974","unstructured":"J.R. Slagle, Automatic Theorem Proving in Theories with Simplifieras, Commutativity and Associativity, Journal of the ACM 21, pp. 622\u2013642, 1974.","journal-title":"Journal of the ACM"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"W. Snyder, A Proof Theory for General Unification, Birkh\u00e4user, 1991.","DOI":"10.1007\/978-1-4612-0435-0"},{"key":"26_CR21","first-page":"665","volume":"814","author":"R. Socher-Ambrosius","year":"1994","unstructured":"R. Socher-Ambrosius, A Refined Version of General E-Unification, Proc. 12th CADE, LNAI 814, pp. 665\u2013677, 1994.","journal-title":"Proc. 12th CADE, LNAI"},{"key":"26_CR22","first-page":"319","volume":"7","author":"Y.H. You","year":"1989","unstructured":"Y.H. You, Enumerating Outer Narrowing Derivations for Constructor Based Term Rewriting Systems, JSC 7, pp. 319\u2013343, 1989.","journal-title":"JSC"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '95: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59293-8_209.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:45:31Z","timestamp":1742597131000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59293-8_209"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592938","9783540492337"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-59293-8_209","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}