{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:02:37Z","timestamp":1776553357443,"version":"3.51.2"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1994,5,1]],"date-time":"1994-05-01T00:00:00Z","timestamp":767750400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[1994,5]]},"DOI":"10.1007\/bf01190830","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T11:25:56Z","timestamp":1108725956000},"page":"213-253","source":"Crossref","is-referenced-by-count":63,"title":["Completeness results for basic narrowing"],"prefix":"10.1007","volume":"5","author":[{"given":"Aart","family":"Middeldorp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erik","family":"Hamoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"CR1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J. A. Bergstra","year":"1986","unstructured":"Bergstra, J. A., Klop, J. W.: Conditional Rewrite Rules: Confluence and Termination. J. Comput. Syst. Sci.32(3), 323?362 (1986)","journal-title":"J. Comput. Syst. Sci."},{"key":"CR2","unstructured":"Bockmayr, A.: Beitr\u00e4ge zur Theorie des Logisch-Funktionalen Programmierens. Ph.D. thesis, Universit\u00e4t Karlsruhe, 1990 (In German)"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(88)90095-3","volume":"59","author":"P. G. Bosco","year":"1988","unstructured":"Bosco, P. G., Giovannetti, E., Moiso, C.: Narrowing vs. SLD-Resolution. Theoret. Comput. Sci.59, 3?23 (1988)","journal-title":"Theoret. Comput. Sci."},{"key":"CR4","first-page":"112","volume-title":"Lecture Notes in Computer Science, vol. 488","author":"J. Chabin","year":"1991","unstructured":"Chabin, J., R\u00e9ty, P.: Narrowing Directed by a Graph of Terms. Proceedings of the 4th International Conference on Rewriting Techniques and Applications, Como. Lecture Notes in Computer Science, vol. 488, pp. 112?123, Berlin, Heidelberg, New York: Springer 1991"},{"key":"CR5","first-page":"243","volume-title":"Handbook of Theoretical Computer Science, Vol. B","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: Handbook of Theoretical Computer Science, Vol. B, pp. 243?320. van Leeuwen, J. (ed), Amsterdam: North-Holland 1990"},{"issue":"8","key":"CR6","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving Termination with Multiset Orderings. Commun. ACM22(8), 465?476 (1979)","journal-title":"Commun. ACM"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(90)90064-O","volume":"75","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Okada, M.: A Rationale for Conditional Equational Programming. Theoret. Comput. Sci.75, 111?138 (1990)","journal-title":"Theoret. Comput. Sci."},{"key":"CR8","first-page":"31","volume-title":"Lecture Notes in Computer Science, vol 308","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G.: Confluence of Conditional Rewrite Systems, Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, Orsay. Lecture Notes in Computer Science, vol 308, pp. 31?44. Berlin, Heidelberg, New York: Springer 1987"},{"key":"CR9","first-page":"538","volume-title":"Lecture Notes in Computer Science, vol. 310","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G.: Canonical Conditional Rewrite System. Proceedings of the 9th Conference on Automated Deduction, Argonne, Lecture Notes in Computer Science, vol. 310, pp. 538?549. Berlin, Heidelberg, New York: Springer 1987"},{"key":"CR10","unstructured":"Dershowitz, N., Plaisted, D. A.: Logic Programming cum Applicative Programming, Proceedings of the 2nd IEEE Symposium on Logic Programming, Boston, pp. 54?66, 1985"},{"key":"CR11","unstructured":"Dershowitz, N., Plaisted, D. A.: Equational Programming. In: Machine Intelligence, vol. 11, Hayes, J. E., Michie, D., Richards, J. (eds). Oxford University Press, pp. 21?56, 1987"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0304-3975(90)90032-D","volume":"72","author":"R. Echahed","year":"1990","unstructured":"Echahed, R.: On Completeness of Narrowing Strategies. Theoret. Comput. Sci.72, 133?146 (1990)","journal-title":"Theoret. Comput. Sci."},{"key":"CR13","first-page":"259","volume-title":"Lecture Notes in Computer Science, vol. 632","author":"E. Echahed","year":"1992","unstructured":"Echahed, E.: Uniform Narrowing Strategies. Proceedings of the 3rd International Conference of Algebraic and Logic Programming. Volterra, Lecture Notes in Computer Science, vol. 632, pp. 259?275. Berlin, Heidelberg, New York: Springer 1992"},{"key":"CR14","unstructured":"Fay, M.: First-Order Unification in Equational Theories. Proceedings of the 4th International Workshop on Automated Deduction, Austin, pp. 161?167, 1979"},{"key":"CR15","unstructured":"Fribourg, L.: SLOG: A Logic Programming Language Interpreter based on Clausal Super-position and Rewriting. Proceedings of the 2nd IEEE Symposium on Logic Programming, Boston, pp. 172?184, 1985"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/0022-0000(91)90009-T","volume":"42","author":"E. Giovannetti","year":"1991","unstructured":"Giovannetti, E., Levi, G., Moiso, C., Palamidessi, C.: Kernel-LEAF: A Logic plus Functional Language. J. Comput. Syst. Sci.42, 139?185 (1991)","journal-title":"J. Comput. Syst. Sci."},{"key":"CR17","first-page":"157","volume-title":"Lecture Notes in Computer Science, vol. 306","author":"E. Giovannetti","year":"1986","unstructured":"Giovannetti, E., Moiso, C.: A Completeness Result for E-Unification Algorithms based on Conditional Narrowing. Proceedings of the Workshop on Foundations of Logic and Functional Programming, Trento, Lecture Notes in Computer Science, vol. 306, pp. 157?167. Berlin, Heidelberg, New York: Springer 1986"},{"key":"CR18","unstructured":"Goguen, J. A., Meseguer, J.: EQLOG: Equality, Types and Generic Modules for Logic Programming. In: Logic Programming: Functions, Relations and Equations. De-Groot, D., Lindstrom, G. (eds). Prentice Hall, pp. 295?363, 1986"},{"key":"CR19","first-page":"387","volume-title":"Lecture Notes in Computer Science, vol. 456","author":"M. Hanus","year":"1990","unstructured":"Hanus, M.: Compling Logic Programs with Equality. Proceedings of the International Workshop on Language Implementation and Logic Programming, Link\u00f6ping, Lecture Notes in Computer Science, vol. 456, pp. 387?401. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR20","unstructured":"Herold, A.: Combination of Unification Algorithms in Equational Theories. Ph.D. thesis, Universit\u00e4t Kaiserslautern, 1987"},{"key":"CR21","unstructured":"Huet, G., L'evy, J. J.: Computations in Orthogonal Rewriting Systems, I and II. In: Computational Logic, Essays in Honor of Alan Robinson. Lassez, J.-L., Plotkin, G. (eds.) The MIT Press, pp. 396?443, 1991. Previous version: Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems, report 359, INRIA, 1979"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"H\u00f6lldobler, S.: Foundations of Equational Logic Programming. Lecture Notes in Artificial Intelligence, vol. 353, 1989","DOI":"10.1007\/BFb0015791"},{"key":"CR23","first-page":"318","volume-title":"Lecture Notes in Computer Science, vol. 87","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical Forms and Unification. Proceedings of the 5th Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 87, pp. 318?334. Berlin, Heidelberg, New York: Springer 1980"},{"key":"CR24","volume-title":"Th\u00e8se de troisi\u00e8me cycle","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Compilation de Formes Canoniques dans les Th\u00e9ories Equationelles. Th\u00e8se de troisi\u00e8me cycle, Universit\u00e9 de Paris Sud, Orsay, 1980 (In French)"},{"key":"CR25","first-page":"543","volume-title":"Lecture Notes in Computer Science, vol. 204","author":"H. Hu\u00dfmann","year":"1985","unstructured":"Hu\u00dfmann, H.: Unification in Conditional-Equational Theories. Proceedings of the European Conference on Computer Algebra. Lecture Notes in Computer Science, vol. 204, pp. 543?553. Berlin, Heidelberg, New York: Springer 1985"},{"key":"CR26","unstructured":"Hu\u00dfmann, H.: Corrigenda to MIP-8502 ?Unification in Conditional-Equational Theories?. Universit\u00e4t Passau, 1988"},{"issue":"2","key":"CR27","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(84)90087-2","volume":"33","author":"S. Kaplan","year":"1984","unstructured":"Kaplan, S.: Conditional Rewrite Rules. Theoret. Comput. Sci.33(2), 175?193 (1984)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"CR28","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(87)80010-X","volume":"4","author":"S. Kaplan","year":"1987","unstructured":"Kaplan, S.: Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence. J. Symbolic Comput.4(3), 295?334 (1987)","journal-title":"J. Symbolic Comput."},{"key":"CR29","unstructured":"Kirchner, C.: M\u00e9thodes et Outils de Conception Syst\u00e9matique d'Algorithmes d'Unification dans les Th\u00e9ories Equationelles, Th\u00e8se de d'\u00e9tat, Universit\u00e9 de NancyI, 1985 (In French)"},{"key":"CR30","first-page":"350","volume-title":"Lecture Notes in Computer Science, vol. 443","author":"J. W. Klop","year":"1990","unstructured":"Klop, J. W.: Term Rewriting Systems: from Church-Rosser to Knuth-Bendix and beyond. Proceedings of the 17th International Colloquium on Automata, Languages and Programming, Warwick. Lecture Notes in Computer Science, vol. 443, pp. 350?369. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR31","unstructured":"Klop, J. W.: Term Rewriting System. In: Handbook of Logic in Computer Science, Vol. II. Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Oxford University Press, pp. 1?112, 1992"},{"key":"CR32","first-page":"74","volume-title":"Lecture Notes in Computer Science, vol. 448","author":"S. Krischer","year":"1991","unstructured":"Krischer, S., Bockmayr, A.: Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test. Proceedings of the 4th International Conference on Rewriting Techniques and Applications, Como. Lecture Notes in Computer Science, vol. 448, pp. 74?85. Berlin, Heidelberg, New York: Springer 1991"},{"issue":"2","key":"CR33","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems4(2), 258?282 (1982)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR34","volume-title":"Ph.D. thesis","author":"A. Middeldorp","year":"1990","unstructured":"Middeldorp, A.: Modular Properties of Term Rewriting Systems. Ph.D. thesis, Vrije Universiteit, Amsterdam, 1990"},{"key":"CR35","first-page":"223","volume-title":"Lecture Notes in Computer Science, vol. 343","author":"J. J. Moreno-Navarro","year":"1989","unstructured":"Moreno-Navarro, J. J., Rodr\u00edguez-Artalejo, M.: BABEL: A Functional and Logic Programming Language based on Constructor Discipline and Narrowing. Proceedings of the 1st International Conference on Algebraic and Logic Programming, Gau\u00dfig, Lecture Notes in Computer Science, vol. 343, pp. 223?232. Berlin, Heidelberg, New York: Springer 1989"},{"key":"CR36","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W. Nutt","year":"1989","unstructured":"Nutt, W., R\u00e9ty, P., Smolka, G.: Basic Narrowing Revisited. J. Symbolic Comput.7, 295?317 (1989)","journal-title":"J. Symbolic Comput."},{"key":"CR37","first-page":"228","volume-title":"Lecture Notes in Computer Science, vol. 256","author":"P. R\u00e9ty","year":"1987","unstructured":"R\u00e9ty, P.: Improving Basic Narrowing Techniques. Proceedings of the 2nd International Conference on Rewriting Techniques and Applications, Bordeaux. Lecture Notes in Computer Science, vol. 256, pp. 228?241. Berlin, Heidelberg, New York: Springer 1987"},{"key":"CR38","unstructured":"R\u00e9ty, P.: M\u00e9thodes d'Unification par Surr\u00e9duction. Th\u00e8se de doctorat, Universit\u00e9 de Nancy I, 1988 (In French)"},{"issue":"1","key":"CR39","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM12(1), pp. 23?41 (1965)","journal-title":"J. ACM"},{"key":"CR40","unstructured":"Shepherdson, J. C.: Mistakes in Logic Programming: the Role of Standardizing Apart, manuscript, University of Bristol, 1991"},{"key":"CR41","doi-asserted-by":"crossref","unstructured":"Yamamoto, A.: Completeness of Extended Unification Based on Basic Narrowing. Proceedings of the 7th Logic Programming Conference, Jerusalem pp. 1?10, 1988","DOI":"10.1007\/3-540-51564-X_51"},{"key":"CR42","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/S0747-7171(89)80015-X","volume":"7","author":"Y. H. You","year":"1989","unstructured":"You, Y. H.: Enumerating Outer Narrowing Derivations for Constructor Based Term Rewriting Systems. J. Symbolic Comput.7, 319?343 (1989)","journal-title":"J. Symbolic Comput."}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01190830.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01190830\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01190830","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T20:53:45Z","timestamp":1586120025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01190830"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,5]]},"references-count":42,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1994,5]]}},"alternative-id":["BF01190830"],"URL":"https:\/\/doi.org\/10.1007\/bf01190830","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,5]]}}}