{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:41Z","timestamp":1725663341424},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540506676"},{"type":"electronic","value":"9783540460633"}],"license":[{"start":{"date-parts":[[1988,1,1]],"date-time":"1988-01-01T00:00:00Z","timestamp":567993600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-50667-5_60","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:30:38Z","timestamp":1330183838000},"page":"83-92","source":"Crossref","is-referenced-by-count":1,"title":["Narrowing with built-in theories"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Bockmayr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0743-1066(86)90014-2","volume":"3","author":"M. Bellia","year":"1986","unstructured":"M. Bellia, G. Levi: The Relation between Logic and Functional languages: A Survey. J. Logic Programming 3 (1986), 217\u2013236","journal-title":"J. Logic Programming"},{"unstructured":"A. Bockmayr: Conditional rewriting and narrowing as a theoretical framework for logic-functional programming: A Survey. Int. Bericht 10\/86, Fak. f. Informatik, Univ. Karlsruhe, 1986","key":"8_CR2"},{"unstructured":"A. Bockmayr: Narrowing with Inductively Defined Functions. Int. Bericht 25\/86, Fak. f. Informatik, Univ. Karlsruhe, 1986","key":"8_CR3"},{"key":"8_CR4","first-page":"379","volume":"3","author":"A. Bockmayr","year":"1987","unstructured":"A. Bockmayr: A Note on a Canonical Theory with Undecidable Unification and Matching Problem. J. Autom. Reas. 3 (1987), 379\u2013381","journal-title":"J. Autom. Reas."},{"key":"8_CR5","series-title":"LNCS","volume-title":"Refined Strategies for Semantic Unification","author":"P. G. Bosco","year":"1987","unstructured":"P. G. Bosco, E. Giovannetti, C. Mosio: Refined Strategies for Semantic Unification. TAPSOFT 87, Pisa, 1987, Springer LNCS 250"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/S0747-7171(87)80065-2","volume":"4","author":"W. B\u00fcttner","year":"1987","unstructured":"W. B\u00fcttner, H. Simonis: Embedding Boolean Equations into Logic Programming. J. Symb. Comput. 4 (1987), 191\u2013205","journal-title":"J. Symb. Comput."},{"unstructured":"A. Colmerauer: Opening the Prolog III Universe. BYTE, Aug. 1987, 177\u2013182","key":"8_CR7"},{"unstructured":"M. Clausen, A.Fortenbacher: Efficient Solution of Linear Diophantine Equations. Int. Ber. 32\/87, Fak. f. Informatik, Univ. Karlsruhe, 1987; to appear in J. Symb. Comput.","key":"8_CR8"},{"unstructured":"D. DeGroot, G. Lindstrom: LOGIC PROGRAMMING \u2014 Functions, Relations and Equations. Prentice Hall 1986","key":"8_CR9"},{"unstructured":"N. Dershowitz, D. A. Plaisted: Logic Programming cum Applicative Programming. Symp. on Logic Programming, Boston 1985, IEEE","key":"8_CR10"},{"unstructured":"M. Fay: First Order Unification in an Equational Theory. 4th Workshop on Automated Deduction, Austin, Texas, 1979","key":"8_CR11"},{"doi-asserted-by":"crossref","unstructured":"L. Fribourg: Handling Function Definitions Through Innermost Superposition and Rewriting. Rewriting Techniques and Applications, Dijon 1985, Springer LNCS 202","key":"8_CR12","DOI":"10.1007\/3-540-15976-2_16"},{"unstructured":"E. Giovannetti, C. Moiso: A Completeness Result for E-Unification Algorithms Based on Conditional Narrowing. Foundations of Logic and Functional Programming, Trento 1986, Springer LNCS 306","key":"8_CR13"},{"doi-asserted-by":"crossref","unstructured":"G. Huet, D. C. Oppen: Equations and Rewrite Rules, A Survey. Formal Language Theory (Ed. R. V. Book), Academic Press 1980","key":"8_CR14","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"doi-asserted-by":"crossref","unstructured":"J.M. Hullot: Canonical Forms and Unification. 5th Conference on Automated Deduction, Les Arcs 1980, Springer LNCS 87","key":"8_CR15","DOI":"10.21236\/ADA087640"},{"doi-asserted-by":"crossref","unstructured":"H. Hussmann: Unification in Conditional-Equational Theories. Technical Report MIP-8502, Univ. Passau, Jan.1985 short version: EUROCAL 85, Linz, Springer LNCS 204","key":"8_CR16","DOI":"10.1007\/3-540-15984-3_328"},{"doi-asserted-by":"crossref","unstructured":"J. Jaffar, J.-L. Lassez: Constraint Logic Programming. POPL 87, M\u00fcnchen, 1987","key":"8_CR17","DOI":"10.1145\/41625.41635"},{"unstructured":"J. Jaffar, J.-L. Lassez M. S. Maher: Logic Programming Language Scheme. In [DeGroot\/Lindstrom 86]","key":"8_CR18"},{"unstructured":"J. P. Jouannaud: Church-Rosser computations with equational term rewriting systems. 8th CAAP, L'Aquila, 1983, Springer LNCS 159","key":"8_CR19"},{"issue":"4","key":"8_CR20","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. P. Jouannaud","year":"1986","unstructured":"J. P. Jouannaud, H. Kirchner: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15,4 (1986), 1155\u20131194","journal-title":"SIAM J. Comput."},{"unstructured":"J. P. Jouannaud, C. Kirchner and H. Kirchner: Incremental construction of unification algorithms in equational theories. 10th ICALP, Barcelona, 1983, Springer LNCS 154","key":"8_CR21"},{"doi-asserted-by":"crossref","unstructured":"J. P. Jouannaud, M. Munoz: Termination of a set of rules modulo a set of equations. 7th CADE, Napa Valley, 1984, Springer LNCS 170","key":"8_CR22","DOI":"10.1007\/978-0-387-34768-4_11"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1016\/S0747-7171(87)80010-X","volume":"4","author":"S. Kaplan","year":"1987","unstructured":"S. Kaplan: Simplifying Conditional Term Rewriting Systems: Unification, Termination and Confluence. J. Symb. Comput. 4 (1987), 295\u2013334","journal-title":"J. Symb. Comput."},{"unstructured":"T. K\u00e4ufl: Reasoning about systems of linear inequalities. Int. Ber. 16\/87, Fak. f. Informatik, Univ. Karlsruhe, 1987","key":"8_CR24"},{"unstructured":"C. Kirchner: Methodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories equationnelles. Th\u00e8se d'\u00e9tat, Univ. Nancy, 1985","key":"8_CR25"},{"doi-asserted-by":"crossref","unstructured":"U. Martin, T. Nipkow: Unification in Boolean Rings. CADE-8, Oxford 1986, Springer LNCS 230","key":"8_CR26","DOI":"10.1007\/3-540-16780-3_115"},{"unstructured":"T. Nipkow: Unification in Primal Algebras. CAAP 88, Nancy 1988, Springer LNCS 299","key":"8_CR27"},{"unstructured":"W. Nutt, P. R\u00e9ty, G. Smolka: Basic Narrowing Revisited. SEKI-Report SR 87-07, Univ. Kaiserslautern, 1987","key":"8_CR28"},{"key":"8_CR29","series-title":"LNCS","volume-title":"Strategy-Controlled Reduction and Narrowing. Rewriting Techniques and Applications","author":"P. Padawitz","year":"1987","unstructured":"P. Padawitz: Strategy-Controlled Reduction and Narrowing. Rewriting Techniques and Applications, Bordeaux 1987, Springer LNCS 256"},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"G. E. Peterson, M. Stickel: Complete Sets of Reductions for Some Equational Theories. J.ACM 28 (1981), 233\u2013264","journal-title":"J.ACM"},{"unstructured":"G. D. Plotkin: Building-In Equational Theories. Machine Intelligence 7 (1972)","key":"8_CR31"},{"doi-asserted-by":"crossref","unstructured":"P. R\u00e9ty, C. Kirchner, H. Kirchner, P. Lescanne: NARROWER: a new algorithm for unification and its application to Logic Programming. Rewriting Techniques and Applications, Dijon 1985, Springer LNCS 202","key":"8_CR32","DOI":"10.1007\/3-540-15976-2_7"},{"unstructured":"M. Schmidt-Schauss: Unification in a Combination of Arbitrary Disjoint Equational Theories. CADE-9, Argonne 1988, Springer LNCS 310","key":"8_CR33"},{"key":"8_CR34","first-page":"333","volume":"1","author":"M. Stickel","year":"1985","unstructured":"M. Stickel: Automated Deduction by Theory Resolution. J. Autom. Reas. 1 (1985), 333\u2013355","journal-title":"J. Autom. Reas."}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50667-5_60","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,24]],"date-time":"2019-06-24T06:08:36Z","timestamp":1561356516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50667-5_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540506676","9783540460633"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-50667-5_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}