{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:46:19Z","timestamp":1752461179822},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_155","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:21:46Z","timestamp":1330251706000},"page":"50-65","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Unification in the union of disjoint equational theories: Combining decision procedures"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus U.","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"unstructured":"F. Baader, K.U. Schulz, \u201cUnification in the Union of Disjoint Equational Theories: Combining Decision Procedures,\u201d DFKI Research Report RR-91\u201333.","key":"5_CR1"},{"key":"5_CR2","volume-title":"Ph.D. Thesis","author":"L. Bachmair","year":"1987","unstructured":"L. Bachmair, Proof Methods for Equational Theories, Ph.D. Thesis, Dept. of Comp. Sci., University of Illinois at Urbana-Champaign, 1987."},{"doi-asserted-by":"crossref","unstructured":"A. Boudet, \u201cUnification in a Combination of Equational Theories: An Efficient Algorithm,\u201d Proceedings of the 10th International Conference on Automated Deduction, LNCS\n449, 1990.","key":"5_CR3","DOI":"10.1007\/3-540-52885-7_95"},{"doi-asserted-by":"crossref","unstructured":"A. Boudet, J.P. Jouannaud, M. Schmidt-Schau\u00df, \u201cUnification in Boolean Rings and Abelian Groups,\u201d J. Symbolic Computation\n8, 1989.","key":"5_CR4","DOI":"10.1016\/S0747-7171(89)80054-9"},{"doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert, \u201cSome Relationships Between Unification, Restricted Unification, and Matching,\u201d Proceedings of the 8th International Conference on Automated Deduction, LNCS\n230, 1986.","key":"5_CR5","DOI":"10.1007\/3-540-16780-3_116"},{"doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert, \u201cA Resolution Principle for Clauses with Constraints,\u201d Proceedings of the 10th International Conference on Automated Deduction, LNCS\n449, 1990.","key":"5_CR6","DOI":"10.1007\/3-540-52885-7_87"},{"doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J.P. Jouannaud, \u201cRewrite Systems,\u201d In J. van Leeuwen (editor), Volume B of Handbook of Theoretical Computer Science, NorthHolland, 1990.","key":"5_CR7","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"doi-asserted-by":"crossref","unstructured":"F. Fages, \u201cAssociative-Commutative Unification,\u201d Proceedings of the 7th International Conference on Automated Deduction, LNCS\n170, 1984.","key":"5_CR8","DOI":"10.1007\/978-0-387-34768-4_12"},{"doi-asserted-by":"crossref","unstructured":"A. Herold, \u201cCombination of Unification Algorithms,\u201d Proceedings of the 8th International Conference on Automated Deduction, LNCS\n230, 1986.","key":"5_CR9","DOI":"10.1007\/3-540-16780-3_111"},{"doi-asserted-by":"crossref","unstructured":"A. Herold, J.H. Siekmann, \u201cUnification in Abelian Semigroups,\u201d J. Automated Reasoning\n3, 1987.","key":"5_CR10","DOI":"10.1007\/BF00243791"},{"key":"5_CR11","volume-title":"An Introduction to Semigroup Theory","author":"J.M. Howie","year":"1976","unstructured":"J.M. Howie, An Introduction to Semigroup Theory, London: Academic Press, 1976."},{"doi-asserted-by":"crossref","unstructured":"J. Jaffar, J.L. Lassez, M. Maher, \u201cA Theory of Complete Logic Programs with Equality,\u201d J. Logic Programming\n1, 1984.","key":"5_CR12","DOI":"10.1016\/0743-1066(84)90010-4"},{"doi-asserted-by":"crossref","unstructured":"J. Jaffar, J.L. Lassez, \u201cConstraint Logic Programming,\u201d Proceedings of 14th POPL Conference, Munich, 1987","key":"5_CR13","DOI":"10.1145\/41625.41635"},{"doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud, H. Kirchner, \u201cCompletion of a Set of Rules Modulo a Set of Equations,\u201d SIAM J. Computing\n15, 1986.","key":"5_CR14","DOI":"10.1137\/0215084"},{"unstructured":"J.P. Jouannaud, C. Kirchner, \u201cSolving Equations in Abstract Algebras: A Rule-Based Survey of Unification,\u201d In J.-L. Lassez, G. Plotkin (editors), Alan Robinson's Anniversary Book, 1991.","key":"5_CR15"},{"doi-asserted-by":"crossref","unstructured":"D. Kapur, P. Narendran, \u201cComplexity of Unification Problems with Associative-Commutative Operators,\u201d Preprint, 1991. To appear in J. Automated Reasoning.","key":"5_CR16","DOI":"10.1007\/BF00245463"},{"key":"5_CR17","volume-title":"Th\u00e8se d'Etat","author":"C. Kirchner","year":"1985","unstructured":"C. Kirchner, M\u00e9thodes et Outils de Conception Syst\u00e9matique d'Algorithmes d'Unification dans les Th\u00e9ories equationnelles, Th\u00e8se d'Etat, Univ. Nancy, France, 1985."},{"doi-asserted-by":"crossref","unstructured":"C. Kirchner, H. Kirchner, \u201cConstrained Equational Reasoning,\u201d Proceedings of SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ACM Press, 1989.","key":"5_CR18","DOI":"10.1145\/74540.74585"},{"unstructured":"M. Livesey, J.H. Siekmann, \u201cUnification of AC-Terms (bags) and ACITerms (sets),\u201d Internal Report, University of Essex, 1975, and Technical Report 3-76, Universit\u00e4t Karlsruhe, 1976.","key":"5_CR19"},{"doi-asserted-by":"crossref","unstructured":"G.S. Makanin, \u201cThe Problem of Solvability of Equations in a Free Semigroup,\u201d Mat. USSR Sbornik\n32, 1977.","key":"5_CR20","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"unstructured":"G. Plotkin, \u201cBuilding in Equational Theories,\u201d Machine Intelligence\n7, 1972.","key":"5_CR21"},{"doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df, \u201cCombination of Unification Algorithms,\u201d J. Symbolic Computation\n8, 1989.","key":"5_CR22","DOI":"10.1016\/S0747-7171(89)80037-9"},{"unstructured":"K.U. Schulz, \u201cMakanin's Algorithm \u2014 Two Improvements and a Generalization,\u201d CIS-Report 91-39, CIS, University of Munich, 1991.","key":"5_CR23"},{"doi-asserted-by":"crossref","unstructured":"J.H. Siekmann, \u201cUnification Theory: A Survey,\u201d in C. Kirchner (ed.), Special Issue on Unification, Journal of Symbolic Computation\n7, 1989.","key":"5_CR24","DOI":"10.1016\/S0747-7171(89)80012-4"},{"doi-asserted-by":"crossref","unstructured":"M. Stickel, \u201cA Complete Unification Algorithm for Associative-Commutative Functions,\u201d Proceedings of the International Joint Conference on Artificial Intelligence, 1975.","key":"5_CR25","DOI":"10.21236\/ADA015846"},{"doi-asserted-by":"crossref","unstructured":"M.E. Stickel, \u201cA Unification Algorithm for Associative-Commutative Functions,\u201d J. ACM\n28, 1981.","key":"5_CR26","DOI":"10.1145\/322261.322262"},{"doi-asserted-by":"crossref","unstructured":"M.E. Stickel, \u201cAutomated Deduction by Theory Resolution,\u201d J. Automated Reasoning\n1, 1985.","key":"5_CR27","DOI":"10.1007\/BF00244275"},{"doi-asserted-by":"crossref","unstructured":"E. Tiden, \u201cUnification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols,\u201d Proceedings of the 8th International Conference on Automated Deduction, LNCS\n230, 1986.","key":"5_CR28","DOI":"10.1007\/3-540-16780-3_110"},{"doi-asserted-by":"crossref","unstructured":"K. Yelick, \u201cUnification in Combinations of Collapse Free Regular Theories,\u201d J. Symbolic Computation\n3, 1987.","key":"5_CR29","DOI":"10.1016\/S0747-7171(87)80025-1"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_155","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:39:07Z","timestamp":1558269547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_155"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_155","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}