{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:11:53Z","timestamp":1725631913318},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540517436"},{"type":"electronic","value":"9783642751004"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/978-3-642-75100-4_13","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T18:09:29Z","timestamp":1320862169000},"page":"107-116","source":"Crossref","is-referenced-by-count":0,"title":["Linear Paramodulation modulo Equality"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Furbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steffen","family":"H\u00f6lldobler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Schreiber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"REPSY-REwrite Programm SYnthesis. Workshop Verifikation","author":"J Avenhaus","year":"1989","unstructured":"J. Avenhaus, J. M\u00fcller, M. Vierling: REPSY-REwrite Programm SYnthesis. Workshop \u201cVerifikation, Konstruktion und Synthese von Programmen\u201d, Karlsruhe: 1989"},{"key":"13_CR2","volume-title":"Narrowing with built-in Theories. Proc","author":"A Bockmayr","year":"1988","unstructured":"A. Bockmayr: Narrowing with built-in Theories. Proc. First International Workshop on Algebraic and Logic Programming, Gaussig (DDR ): 1988"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"H. J. B\u00fcrckert: Lazy Theory Unification in Prolog: An Extension of the Warren Abstract Machine. Proceedings GWAI\u201986, IFB 124, 277\u2013288: 1986","DOI":"10.1007\/978-3-642-71385-9_28"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"B. IVonh\u00f6fer, U. Furbach: Knuth-Bendix Completion versus Fold-Unfold: A Comparative Study in Program Synthesis. GWAF86, IFB 124, 289\u2013300: 1986","DOI":"10.1007\/978-3-642-71385-9_29"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"U. Furbach, S. H\u00f6lldobler: Modelling the Combination of Functional and Logic Programming Languages. Journal of Symbolic Computation, 123\u2013138: 1986","DOI":"10.1016\/S0747-7171(86)80018-9"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"U. Rirbach, S. H\u00f6lldobler, J. Schreiber: Horn Equality Theories and Paramodulation. To appear in Journal of Automated Reasoning: 1989","DOI":"10.1007\/BF00248322"},{"key":"13_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0743-1066(89)90028-9","volume":"6","author":"JH Gallier","year":"1989","unstructured":"J. H. Gallier, S. Raatz: Extending SLD-resolution to Equational Horn Clauses using E-unification. Journal of Logic Programming 6, 3\u201343: 1989","journal-title":"Journal of Logic Programming"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"J. H. Gallier, W. Snyder: A Complete E-Unification Procedure. Proc. RTA, LNCS 256: 1987","DOI":"10.1007\/3-540-17220-3_19"},{"key":"13_CR9","unstructured":"S. H\u00f6lldobler: From Paramodulation to Narrowing. Proc. 5th International Conference\/Symposium on Logic Programming, 327\u2013342: 1988"},{"key":"13_CR10","unstructured":"S. H\u00f6lldobler: Horn Equality Theories and Complete Sets of Transformations. Proc. Fifth Generation Computer Systems, 405\u2013412: 1988"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"S. H\u00f6lldobler: Foundations of Equational Logic Programming. To appear in: Lecture Notes in Artificial Intelligence 353: 1989","DOI":"10.1007\/BFb0015791"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"J. Hsiang, M. Rusinowitch: On Word Problems in Equational Theories. Proc. International Conference on Automata, Languages and Programming, LNCS 267, 54\u201371: 1987","DOI":"10.1007\/3-540-18088-5_6"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"G. Huet, D. Oppen: Equations and Rewrite Rules: a Survey in: Formal Languages: Perspectives and Open Problems (Book, ed.), Academic Presss, 349\u2013405 (1980)","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"J. M. Hullot: Canonical Forms and Unification. Proc. 5th Conference on Automated Deduction, 318\u2013334: 1980","DOI":"10.21236\/ADA087640"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud, Claude Kirchner, Helene Kirchner: Incremental Construction of Unification Algorithms in Equational Theories. Proc. International Conference on Automata, Languages and Program-ming, LNCS 154, 361\u2013373: 1983","DOI":"10.1007\/BFb0036921"},{"key":"13_CR16","volume-title":"Springer","author":"JW Lloyd","year":"1984","unstructured":"J. W. Lloyd: Foundations of Logic Programming. Springer: 1984."},{"key":"13_CR17","unstructured":"A. Martelli, C. Moiso, C. F. Rossi: An Algorithm for Unification in Equational Theories. Proc. Sym-posium on Logic Programming, 180\u2013186: 1986"},{"key":"13_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-73824-1","volume-title":"Computing in Horn Clause Theories, EATCS Monograph","author":"P Padawitz","year":"1988","unstructured":"P. Padawitz: Computing in Horn Clause Theories, EATCS Monograph, Springer, Berlin: 1988"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"G. E. Peterson, M. E. Stickel: Complete Sets of Reductions for Some Equational Theories. Journal of the ACM, 233\u2013264: 1981","DOI":"10.1145\/322248.322251"},{"issue":"1","key":"13_CR20","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"GE Peterson","year":"1983","unstructured":"G. E. Peterson: A Technique For Establishing Completeness Results in Theorem Proving With Equality, SIAM Journal of Computing, 12 (1), 82\u2013100, 1983","journal-title":"SIAM Journal of Computing"},{"key":"13_CR21","first-page":"73","volume-title":"Machine Intelligence 7 (Meitzer, Mitchie, eds.)","author":"GD Plotkin","year":"1972","unstructured":"G. D. Plotkin: Building-In Equational Theories. In: Machine Intelligence 7 (Meitzer, Mitchie, eds.), 73\u201390: 1972"},{"key":"13_CR22","unstructured":"J. H. Siekmann: Unification Theory. Proceedings EC AI, 365\u2013400: 1986"},{"key":"13_CR23","volume-title":"Siekmann","author":"J. H","year":"1989","unstructured":"J. H. Siekmann: Unification Theory. To appear in Journal of Symbolic Computation: 1989"},{"key":"13_CR24","volume-title":"Press","author":"JE Stoy","year":"1977","unstructured":"J. E. Stoy: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, M.I.T. Press: 1977"},{"key":"13_CR25","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0743-1066(84)90001-3","volume":"1","author":"MH Emden van","year":"1984","unstructured":"M. H. van Emden, J. W. Lloyd: A Logical Reconstruction of Prolog II. Journal of Logic Programming 1, 143\u2013149: 1984","journal-title":"Journal of Logic Programming"}],"container-title":["Informatik-Fachberichte","GWAI-89 13th German Workshop on Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-75100-4_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T22:26:44Z","timestamp":1639607204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-75100-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540517436","9783642751004"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-75100-4_13","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1989]]}}}