{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:40:06Z","timestamp":1752460806862},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:21:47Z","timestamp":1330251707000},"page":"267-281","source":"Crossref","is-referenced-by-count":20,"title":["Combination techniques for non-disjoint equational theories"],"prefix":"10.1007","author":[{"given":"Eric","family":"Domenjoud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francis","family":"Klay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Franz Baader and Klaus Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 50\u201365, 1992.","DOI":"10.1007\/3-540-55602-8_155"},{"key":"19_CR2","first-page":"301","volume-title":"LNCS 690","author":"F. Baader","year":"1993","unstructured":"Franz Baader and Klaus U. Schulz. Combination techniques and decision problems for disunification. In Claude Kirchner, editor. Rewriting Techniques and Applications, 5th International Conference, RTA-93, LNCS 690, pages 301\u2013315, Montreal, Canada, June 16\u201318, 1993. Springer-Verlag."},{"key":"19_CR3","volume-title":"Th\u00e8se de Doctorat d'Universit\u00e9","author":"A. Boudet","year":"1990","unstructured":"A. Boudet. Unification dans les m\u00e9langes de th\u00e9ories \u00e9quationelles. Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 de Paris-Sud, Orsay (France), February 1990."},{"key":"19_CR4","first-page":"261","volume-title":"volume 449 of Lecture Notes in Computer Science","author":"D. Dougherty","year":"1990","unstructured":"D. Dougherty and P. Johann. An improved general E-unification method. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 261\u2013275. Springer-Verlag, July 1990."},{"issue":"2\u20133","key":"19_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. Theoretical Computer Science, 67(2\u20133):203\u2013260, October 1989.","journal-title":"Theoretical Computer Science"},{"key":"19_CR6","unstructured":"Claude Kirchner. M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles. Th\u00e8se de Doctorat d'Etat, Universit\u00e9 de Nancy I, 1985."},{"issue":"2","key":"19_CR7","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0304-3975(92)90015-8","volume":"103","author":"M. Kurihara","year":"1992","unstructured":"M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems with shared constructors. Theoretical Computer Science, 103(2):273\u2013282, 1992.","journal-title":"Theoretical Computer Science"},{"key":"19_CR8","first-page":"343","volume-title":"volume 355 of Lecture Notes in Computer Science","author":"T. Nipkow","year":"1989","unstructured":"T. Nipkow. Combining matching algorithms: The regular case. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), volume 355 of Lecture Notes in Computer Science, pages 343\u2013358. Springer-Verlag, April 1989."},{"key":"19_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2267170","volume":"12","author":"E. Post","year":"1947","unstructured":"E. Post. Recursive unsolvability of a problem of thue. The Journal of Symbolic Logic, 12:1\u201311, 1947.","journal-title":"The Journal of Symbolic Logic"},{"key":"19_CR10","first-page":"261","volume-title":"volume 624 of Lecture Notes in Artificial Intelligence","author":"Ch. Ringeissen","year":"1992","unstructured":"Ch. Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Proceedings of the 1st International Conference on Logic Programming and Automated Reasoning, St. Petersburg (Russia), volume 624 of Lecture Notes in Artificial Intelligence, pages 261\u2013272. Springer-Verlag, 1992."},{"key":"19_CR11","unstructured":"Ch. Ringeissen. Combinaison de R\u00e9solutions de Contraintes. Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 de Nancy I, December 1993."},{"key":"19_CR12","first-page":"187","volume-title":"volume 775 of Lecture Notes in Computer Science","author":"Ch. Ringeissen","year":"1994","unstructured":"Ch. Ringeissen. Combination of matching algorithms. In P. Enjalbert, E. W. Mayr, and K. W. Wagner, editors, Proceedings 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen (France), volume 775 of Lecture Notes in Computer Science, pages 187\u2013198. Springer-Verlag, February 1994."},{"issue":"1","key":"19_CR13","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schau\\","year":"1989","unstructured":"M. Schmidt-Schau\\. Combination of unification algorithms. Journal of Symbolic Computation, 8(1 & 2):51\u2013100, 1989. Special issue on unification. Part two.","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"19_CR14","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0747-7171(87)80025-1","volume":"3","author":"K. Yelick","year":"1987","unstructured":"K. Yelick. Unification in combinations of collapse-free regular theories. Journal of Symbolic Computation, 3(1 & 2):153\u2013182, April 1987.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:11:50Z","timestamp":1619557910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}