{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:34:27Z","timestamp":1759638867841},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,9,1]],"date-time":"1993-09-01T00:00:00Z","timestamp":746841600000},"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":[[1993,9]]},"DOI":"10.1007\/bf01202035","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T10:49:11Z","timestamp":1109328551000},"page":"147-168","source":"Crossref","is-referenced-by-count":10,"title":["Conditional narrowing modulo a set of equations"],"prefix":"10.1007","volume":"4","author":[{"given":"Alexander","family":"Bockmayr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","volume-title":"Technical Report MPI-1-91-209","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L.: Associative-commutative reduction orderings. Technical Report MPI-1-91-209, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken 1991"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. Ben Cherifa","year":"1987","unstructured":"Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Programming9, 137?159 (1987)","journal-title":"Sci. Comput. Programming"},{"key":"CR3","unstructured":"Brand, D., Darringer, J. A., Joyner, W. H.: Completeness of conditional reductions. Research report RC 7404, IBM, 1978"},{"key":"CR4","series-title":"Lecture Notes in Computing Science, vol. 355","volume-title":"Proc. Rewriting Techniques and Applications, Chapel Hill","author":"H. Bertling","year":"1989","unstructured":"Bertling, H., Ganzinger, H.: Completion-time optimization of rewrite-time goal solving. In: Proc. Rewriting Techniques and Applications, Chapel Hill. Lecture Notes in Computing Science, vol. 355. Berlin, Heidelberg, New York: Springer 1989"},{"key":"CR5","volume-title":"A computational logic","author":"R. S. Boyer","year":"1979","unstructured":"Boyer, R. S., Moore, J. S.: A computational logic. New York: Academic Press 1979"},{"key":"CR6","unstructured":"Bockmayr, A.: Conditional rewriting and narrowing as a theoretical framework for logic-functional programming: A survey. Technical Report 10\/86, Fakult\u00e4t f\u00fcr Informatik, Univ. Karlsruhe, 1986"},{"key":"CR7","series-title":"Lecture Notes in Computing Science, vol. 343","volume-title":"First Int. Workshop Algebraic and Logic Programming, Gau\u00dfig","author":"A. Bockmayr","year":"1988","unstructured":"Bockmayr, A.: Narrowing with built-in theories. In: First Int. Workshop Algebraic and Logic Programming, Gau\u00dfig. Lecture Notes in Computing Science, vol. 343. Berlin, Heidelberg, New York: Springer 1988"},{"key":"CR8","unstructured":"Bockmayr, A.: Contributions to the Theory of Logic-Functional Programming. PhD thesis, Fakult\u00e4t f\u00fcr Informatik, Univ. Karlsruhe, 1990. (in German)"},{"key":"CR9","series-title":"Lecture Notes in Computing Science, vol. 449","volume-title":"Proc. 10th CADE, Kaiserslautern","author":"A. Boudet","year":"1990","unstructured":"Boudet, A.: Unification in a combination of equational theories: an efficient algorithm. In: Proc. 10th CADE, Kaiserslautern. Lecture Notes in Computing Science, vol. 449. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., Plaisted, D. A.: Termination orderings for associative-commutative rewriting systems. J. Symb. Comput.1, 329?349 (1985)","journal-title":"J. Symb. Comput."},{"key":"CR11","volume-title":"4th Annual ESPRIT Conference, Bruxelles","author":"A. Colmerauer","year":"1987","unstructured":"Colmerauer, A.: Introduction to PROLOG III. In: 4th Annual ESPRIT Conference, Bruxelles. Amsterdam: North Holland, 1987"},{"key":"CR12","volume-title":"A new perspective on integrating functional and logic languages","author":"J. Darlington","year":"1991","unstructured":"Darlington, J., Guo, Y., Paul, H.: A new perspective on integrating functional and logic languages. Imperial College, London, September 1991"},{"key":"CR13","volume-title":"Logic Programming. Functions, Relations and Equations","year":"1986","unstructured":"DeGroot, D., Lindstrom, G. (eds.): Logic Programming. Functions, Relations and Equations. Englewood: Prentice Hall 1986"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Providing termination with multiset orderings. Comm. ACM22, 465?476 (1979)","journal-title":"Comm. ACM"},{"key":"CR15","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. Theoretical Comput. Sci.75, 111?138 (1990)","journal-title":"Theoretical Comput. Sci."},{"key":"CR16","volume-title":"Proc. Intern. Symposium on Logic Programming","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N., Plaisted, D. A.: Logic programming cum applicative programming. In: Proc. Intern. Symposium on Logic Programming, Boston. IEEE, 1985"},{"key":"CR17","unstructured":"L\u00f3pez Fraguas, F. J., Rodriguez Artalejo, M.: An approach to constraint functional logic programming. Technical Report DIA 91\/4, Univ. Compl. Madrid, October 1991"},{"key":"CR18","unstructured":"Fay, M.: First-order unification in an equational theory. In: 4th Workshop on Automated Deduction, Austin, Texas, 1979"},{"key":"CR19","series-title":"Lecture Notes in Computing Science, vol. 247","volume-title":"Proc. STACS'87","author":"H. Ganzinger","year":"1987","unstructured":"Ganzinger, H.: Ground term confluence in parametric conditional equational specifications. In: Proc. STACS'87. Lecture Notes in Computing Science, vol. 247. Berlin, Heidelberg, New York: Springer 1987"},{"key":"CR20","unstructured":"Geser, A.: Termination Relative. PhD thesis, Univ. Passau, 1990"},{"key":"CR21","series-title":"Lecture Notes in Computing Science, vol. 306","volume-title":"Foundations of Logic and Functional Programming, Trento","author":"E. Giovannetti","year":"1986","unstructured":"Giovannetti, E., Moiso, C.: A completeness result forE-unification algorithms based on conditional narrowing. In: Foundations of Logic and Functional Programming, Trento. Lecture Notes in Computing Science, vol. 306. Berlin, Heidelberg, New York: Springer 1986"},{"key":"CR22","unstructured":"Gnaedig, I.: Investigations on termination of equational rewriting. Technical Report 732, INRIA, 1987"},{"key":"CR23","volume-title":"Formal Language Theory","author":"G. Huet","year":"1980","unstructured":"Huet, G., Oppen, D. C.: Equations and rewrite rules, A survey. In: Book, R. V. (ed.) Formal Language Theory. New York: Academic Press 1980"},{"key":"CR24","volume-title":"Lecture Notes in Computing Science, vol. 353","author":"S. H\u00f6lldobler","year":"1989","unstructured":"H\u00f6lldobler, S.: Foundations of Equational Logic Programming. Lecture Notes in Computing Science, vol. 353. Berlin, Heidelberg, New York: Springer 1989"},{"key":"CR25","volume-title":"Lecture Notes in Computing Science, vol. 87","author":"J. M. Hullot","year":"1980","unstructured":"Hullot, J. M.: Canonical forms and unification. In: Proc. 5th Conference on Automated Deduction, Les Arcs. Lecture Notes in Computing Science, vol. 87. Berlin, Heidelberg, New York: Springer 1980"},{"key":"CR26","series-title":"Lecture Notes in Computing Science, vol. 204","volume-title":"Technical Report MIP-8502, Univ. Passau, Jan. 1985. Short version: EUROCAL 85, Linz","author":"H. Hussmann","year":"1985","unstructured":"Hussmann, H.: Unification in conditional-equational theories. Technical Report MIP-8502, Univ. Passau, Jan. 1985. Short version: EUROCAL 85, Linz, Lecture Notes in Computing Science, vol. 204. Berlin, Heidelberg, New York: Springer 1985"},{"key":"CR27","unstructured":"Hussmann, H.: Corrigenda to MIP-8502 ?Unification in conditional equational theories?. Univ. Passau, April\/October, 1988"},{"issue":"4","key":"CR28","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. P. Jouannaud","year":"1986","unstructured":"Jouannaud, J. P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput.15(4), 1155?1194 (1986)","journal-title":"SIAM J. Comput."},{"key":"CR29","series-title":"Lecture Notes in Computing Science, vol. 154","volume-title":"Proc. 10th ICALP, Barcelona","author":"J. P. Jouannaud","year":"1983","unstructured":"Jouannaud, J. P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Proc. 10th ICALP, Barcelona. Lecture Notes in Computing Science, vol. 154. Berlin, Heidelberg, New York: Springer 1983"},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Proc. 14th ACM Symp. Principles of Programming Languages, Munich, 1987","DOI":"10.1145\/41625.41635"},{"key":"CR31","volume-title":"Lecture Notes in Computing Science, vol. 154","author":"J. P. Jouannaud","year":"1984","unstructured":"Jouannaud, J. P., Munoz, M.: Termination of a set of rules modulo a set of equations. In: Proc. 7th Conference on Automated Deduction, Napa Valley. Lecture Notes in Computing Science, vol. 154. Berlin, Heidelberg, New York: Springer 1984"},{"key":"CR32","series-title":"Lecture Notes in Computing Science, vol. 159","volume-title":"Proc. 8th CAAP, L'Aquila","author":"J. P. Jouannaud","year":"1983","unstructured":"Jouannaud, J. P.: Church-Rosser computations with equational term rewriting systems. In: Proc. 8th CAAP, L'Aquila. Lecture Notes in Computing Science, vol. 159. Berlin, Heidelberg, New York: Springer 1983"},{"key":"CR33","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, 175?193 (1984)","journal-title":"Theoret. Comput. Sci."},{"key":"CR34","volume-title":"Technical Report 194","author":"S. Kaplan","year":"1984","unstructured":"Kaplan, S.: Fair conditional term rewriting systems: Unification, termination and confluence. Technical Report 194, L. R. I., Univ. Paris-Sud, 1984"},{"key":"CR35","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. Symb. Comput.4, 295?334 (1987)","journal-title":"J. Symb. Comput."},{"key":"CR36","series-title":"Como. Lecture Notes in Computing Science, vol. 488","volume-title":"Proc. Rewriting Techniques and Applications","author":"S. Krischer","year":"1991","unstructured":"Krischer, S., Bockmayr, A.: Detecting redundant narrowing derivations by the LSE-SL reducibility test. In: Proc. Rewriting Techniques and Applications, Como. Lecture Notes in Computing Science, vol. 488. Berlin, Heidelberg, New York: Springer 1991"},{"key":"CR37","unstructured":"Kirchner, G.: Methodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories equationnelles, 1985. Th\u00e8se d'Etat, Univ. Nancy"},{"key":"CR38","series-title":"Lecture Notes in Computing Science, vol. 472","volume-title":"Foundations of Software Technology and Theoretical Computer Science, New Delhi","author":"D. Kapur","year":"1990","unstructured":"Kapur, D., Sivakumar, G., Zhang, H.: A new method for proving termination of AC-rewrite systems. In: Foundations of Software Technology and Theoretical Computer Science, New Delhi. Lecture Notes in Computing Science, vol. 472. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR39","volume-title":"Technical Report CS-R9154","author":"A. Middeldorp","year":"1991","unstructured":"Middeldorp, A., Hamoen, E.: Counterexamples to completeness results for basic narrowing. Technical Report CS-R9154, CWI Amsterdam, December 1991"},{"key":"CR40","series-title":"Como. Lecture Notes in Computing Science, vol. 488","volume-title":"Proc. Rewriting Techniques and Applications","author":"P. Narendran","year":"1991","unstructured":"Narendran, P., Rusinowitsch, M.: A ground associative-commutative theory has a finite canonical system. In: Proc. Rewriting Techniques and Applications, Como. Lecture Notes in Computing Science, vol. 488. Berlin, Heidelberg, New York: Springer 1991"},{"key":"CR41","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-73824-1","volume-title":"Computing in Horn Clause Theories, vol. 16 of EATCS Monograph","author":"P. Padawitz","year":"1988","unstructured":"Padawitz, P.: Computing in Horn Clause Theories, vol. 16 of EATCS Monograph. Berlin, Heidelberg, New York: Springer 1988"},{"key":"CR42","volume-title":"Lecture Notes in Computing Science, vol. 230","author":"S., Francez, N. Porat","year":"1986","unstructured":"Porat, S., Francez, N.: Full-commutation and fair-termination in equational and combined term rewriting systems. In: Proc. 8th Conference on Automated Deduction, Oxford. Lecture Notes in Computing Science, vol. 230. Berlin, Heidelberg, New York: Springer 1986"},{"key":"CR43","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"Peterson, G. E., Stickel, M.: Complete sets of reductions for some equational theories. J. Assoc. Comput. Machinery28, 182?215 (1981)","journal-title":"J. Assoc. Comput. Machinery"},{"key":"CR44","volume-title":"Th\u00e8se de Doctorat d'Etat","author":"J. L. Remy","year":"1982","unstructured":"Remy, J. L.: Etude des syst\u00e8mes de r\u00e9\u00e9criture conditionnels et applications. Th\u00e8se de Doctorat d'Etat, Institut National de Polytechnique de Lorraine, Nancy, 1982"},{"key":"CR45","volume-title":"Lecture Notes in Computing Science, vol. 463","author":"J. Steinbach","year":"1990","unstructured":"Steinbach, J.: AC-termination of rewrite systems: a modified Knuth-Bendix-ordering. In: Proc. Algebraic and Logic Programming, Nancy. Lecture Notes in Computing Science, vol. 463. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR46","volume-title":"Diplomarbeit","author":"A. Werner","year":"1991","unstructured":"Werner, A.: Termersetzung und Narrowing mit geordneten Sorten. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Univ. Karlsruhe, 1991"},{"key":"CR47","unstructured":"Zhang, H.: REVEUR 4: Etude et mise en oeuvre de la r\u00e9\u00e9criture conditionnelle. Th\u00e8se de Doctorat de 3\u00e8me cycle, Univ. de Nancy, CRIN, 1984"},{"key":"CR48","series-title":"Lecture Notes in Computing Science, vol. 310","volume-title":"Proc. 9th CADE, Oxford","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D.: First-order theorem proving using conditional rewriting rules. In: Proc. 9th CADE, Oxford. Lecture Notes in Computing Science, vol. 310. Berlin, Heidelberg, New York: Springer 1988"},{"key":"CR49","series-title":"Lecture Notes in Computing Science, vol. 202","volume-title":"Proc. Rewriting Techniques and Applications, Dijon","author":"H. Zhang","year":"1985","unstructured":"Zhang, H., R\u00e9my, J. L.: Contextual rewriting. In: Proc. Rewriting Techniques and Applications, Dijon. Lecture Notes in Computing Science, vol. 202. Berlin, Heidelberg, New York: Springer 1985"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01202035.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01202035\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01202035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T13:01:40Z","timestamp":1556715700000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01202035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,9]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,9]]}},"alternative-id":["BF01202035"],"URL":"https:\/\/doi.org\/10.1007\/bf01202035","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,9]]}}}