{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:43Z","timestamp":1725456223107},"publisher-location":"Berlin\/Heidelberg","reference-count":47,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012845","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"378-396","source":"Crossref","is-referenced-by-count":7,"title":["Unification in a combination of arbitrary disjoint equational theories"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert, H.-J., Herold A., Schmidt-Schau\u00df, M., On Equational Theories, Unification and Decidability, LNCS 256, pp. 204\u2013215. (Also to appear in JSC, special issue on unification)","DOI":"10.1007\/3-540-17220-3_18"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert, H.-J., Some relationships between Unification, Restricted Unification and Matching, in Proc. of 8th CADE, Springer, LNCS 230, pp. 514\u2013524, (1986)","DOI":"10.1007\/3-540-16780-3_116"},{"key":"26_CR3","unstructured":"B\u00fcrckert, H.-J., Matching \u2014 A special case of unification?, Technical report, SR-87-08"},{"key":"26_CR4","unstructured":"B\u00fcttner, W., Simonis, H., Embedding Boolean Expressions in Logic Programming, preprint, Siemens AG, M\u00fcnchen, (1986)"},{"key":"26_CR5","unstructured":"Colmerauer, A., Equations and inequations on finite and infinite trees, Proc. of the int. Conf. on FGCS, (ed. ICOT), (1984)"},{"key":"26_CR6","unstructured":"Chang, C., Lee, R. C., Symbolic Logic and Mechanical Theorem Proving, Academic Press, (1973)"},{"key":"26_CR7","unstructured":"Crone-Rawe, Bernhard, \u2018Unification algorithms for Boolean rings', Diplom-arbeit, Universit\u00e4t Kaiserslautern, (to appear)"},{"key":"26_CR8","unstructured":"Fay, M., \u2018First Order Unification in an Equational Theory', Proc. 4th CADE, Texas, pp. 161\u2013167, (1979)"},{"key":"26_CR9","first-page":"194","volume":"170","author":"F. Fages","year":"1984","unstructured":"Fages, F., Associative-Commutative Unification, Proc. of 7th CADE (ed. Shostak, R.E.), LNCS 170, pp. 194\u2013208, (1984)","journal-title":"LNCS"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Fages, F., Associative-Commutative Unification, Technical report, INRIA, (1985)","DOI":"10.1007\/978-0-387-34768-4_12"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Fages, F., Huet G., Complete sets of unifiers and matchers in equational theories. Proc. CAAP-83, LNCS 159, (1983). Also in Theoretical Computer Science 43, pp. 189\u2013200, (1986)","DOI":"10.1016\/0304-3975(86)90175-1"},{"key":"26_CR12","unstructured":"Gallier, J. H., Logic for Computer Science, Harper & Row, (1986)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Gr\u00e4tzer, G. Universal Algebra, Springer-Verlag, (1979)","DOI":"10.1007\/978-0-387-77487-9"},{"key":"26_CR14","first-page":"450","volume":"230","author":"A. Herold","year":"1986","unstructured":"Herold, A., \u2018Combination of Unification Algorithms', Proc. 8th CADE, ed. J. Siekmann, LNCS 230, pp. 450\u2013469, (1986). Also: MEMO-SEKI 86-VIII-KL, Universit\u00e4t Kaiserslautern, 1985","journal-title":"Proc. 8th CADE"},{"issue":"3","key":"26_CR15","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/BF00243791","volume":"3","author":"A. Herold","year":"1987","unstructured":"Herold, A., Siekmann, J., Unification in Abelian Semigroups, JAR 3 (3), pp. 247\u2013283, (1987)","journal-title":"JAR"},{"key":"26_CR16","unstructured":"Huet, G., Oppen, D.C., Equations and Rewrite Rules, SRI Technical Report CSL-111, (1980) also in:Formal Languages: Perspectives and open problems, R. Book.(ed), Academic Press, (1982)"},{"key":"26_CR17","unstructured":"Huet, G. R\u00e9solution d'\u00c9quations dans des langages d'ordre 1,2,...,\u03c9, Th\u00e8se d'\u00c9tat, Univ. de Paris VII, (1976)"},{"issue":"4","key":"26_CR18","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, JACM 27, 4, pp. 797\u2013821, (1980)","journal-title":"JACM"},{"key":"26_CR19","first-page":"318","volume":"87","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M., Canonical Forms and Unification, Proc. 5th CADE, LNCS 87, pp.318\u2013334, (1980)","journal-title":"LNCS"},{"key":"26_CR20","first-page":"361","volume":"154","author":"J.-P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H., \u2018Incremental Construction of Unification Algorithms in Equational Theories', Proc. of 10th ICALP ed J.Diaz, LNCS 154, pp. 361\u2013373, (1983)","journal-title":"LNCS"},{"key":"26_CR21","first-page":"224","volume":"170","author":"C. Kirchner","year":"1984","unstructured":"Kirchner, C., A New Equational Unification Method: A generalization of Martelli-Montanari's Algorithm. 7th CADE, LNCS 170, pp. 224\u2013247, (1984)","journal-title":"LNCS"},{"key":"26_CR22","unstructured":"Kirchner, C.,: \u2018Computing Unification Algorithms', Conf. on Logic in Computer Science, pp. 206\u2013216, (1986)"},{"key":"26_CR23","unstructured":"Kirchner, C., Methods and Tools for Equational Unification, CNRS technical report Nr. 87-R-008, University of Nancy I, (1987)"},{"key":"26_CR24","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.B., \u2018Simple Word Problems in Universal Algebras', in: Computational Problems in Abstract Algebra, J. Leech ed., Pergamon Press, Oxford, (1970)"},{"key":"26_CR25","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1090\/conm\/029\/749246","volume":"29","author":"D. Lankford","year":"1984","unstructured":"Lankford, D., Butler, D., Brady, B., Abelian group unification algorithms for elementary terms., Contemporary Math. 29, pp. 193\u2013199, (1984)","journal-title":"Contemporary Math."},{"key":"26_CR26","unstructured":"Lankford D.S., Ballantyne A.M., Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions. Report ATP-39, Dept. of Mathematics, Universoty of Texas, Austin, Texas, (1977)"},{"key":"26_CR27","unstructured":"Livesey, M., Siekmann, J., Unification of Sets and Multisets, SEKI technical report, Universit\u00e4t Karslruhe, (1978)"},{"issue":"2","key":"26_CR28","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., and Montanari, U., An Efficient Unification Algorithm, ACM Trans. Programming Languages and Systems 4, 2, pp. 258\u2013282, (1982)","journal-title":"Programming Languages and Systems"},{"key":"26_CR29","unstructured":"Martin, U., Unification in Boloean rings and unquantified formluae of the first order predicate calculus, (to appear in JAR)"},{"key":"26_CR30","first-page":"506","volume":"230","author":"U. Martin","year":"1986","unstructured":"Martin, U., Nipkov, T., Unification in Boolean Rings,Proc. 8th CADE, LNCS 230, pp. 506\u2013513, (1986)","journal-title":"LNCS"},{"key":"26_CR31","unstructured":"Nutt, W., R\u00e9ty, P., Smolka, G., Basic Narrowing Revisited, Technical report SR-87-07, Universit\u00e4t Kaiserslautern, (1987)"},{"issue":"2","key":"26_CR32","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G.E. Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel M.E., Complete sets of reductions for some equational theories, JACM 28,2, pp. 233\u2013264, (1981)","journal-title":"JACM"},{"key":"26_CR33","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G., Building in equational theories, Machine Intelligence 7, pp.73\u201390, (1972)","journal-title":"Machine Intelligence"},{"issue":"1","key":"26_CR34","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson. J.A. A machine-Oriented Logic Based on the resolution principle. JACM 12,1 pp.23\u201341, (1965)","journal-title":"JACM"},{"issue":"3","key":"26_CR35","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/BF02328450","volume":"2","author":"M. Schmidt-Schauss","year":"1986","unstructured":"Schmidt-Schauss, M., Unification under Associativity and Idempotence is of Type Nullary, JAR 2,3, pp. 277\u2013281, (1986)","journal-title":"JAR"},{"key":"26_CR36","unstructured":"Schmidt-Schauss, M., Computational aspects of an order-sorted logic with term declarations, thesis, (1987), (to appear)"},{"key":"26_CR37","unstructured":"Schmidt-Schauss, M., Unification in a Combination of Arbitrary Disjoint Equational Theories, SEKI report SR-87-16, Universit\u00e4t Kaiserslautern, (1987)"},{"key":"26_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E., Deciding Combinations of Theories, JACM 31, pp. 1\u201312, (1984)","journal-title":"JACM"},{"key":"26_CR39","unstructured":"Siekmann, J., Stringunification, Essex university, Memo CSM-7, (1975)"},{"key":"26_CR40","first-page":"vi","volume":"II","author":"J.H. Siekmann","year":"1986","unstructured":"Siekmann, J.H., Unification Theory, Proc. of ECAT86, Vol II, p. vi\u2013xxxv, Brighton, (1986)","journal-title":"Proc. of ECAT"},{"key":"26_CR41","unstructured":"Siekmann, J.H., Unification Theory, Journal of Symbolic Computation, (to appear)"},{"issue":"3","key":"26_CR42","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. Stickel","year":"1981","unstructured":"Stickel, M., \u2018A unification algorithm for associative-commutative functions', Journal of the ACM 28 (3), pp. 423\u2013434 (1981)","journal-title":"Journal of the ACM"},{"key":"26_CR43","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00243792","volume":"3","author":"M. Stickel","year":"1987","unstructured":"Stickel, M., \u2018A comparison of the variable-abstraction and constant-abstraction method for associative-commutative unification', JAR 3, pp. 285\u2013289, (1987)","journal-title":"JAR"},{"key":"26_CR44","unstructured":"Szabo, P., Theory of first order unification, (in German), Thesis, University of Karlsruhe, (1982)"},{"key":"26_CR45","unstructured":"Tid\u00e9n, E., First-Order Unification in Combinations of Equational Theories, Thesis, Stockholm, (1986)"},{"key":"26_CR46","first-page":"431","volume":"230","author":"E. Tid\u00e9n","year":"1986","unstructured":"Tid\u00e9n, E.: \u2018Unification in Combination of Collapse Free Theories with Disjoint Sets of Function Symbols', Proc. 8th CADE, LNCS 230, pp. 431\u2013449, (1986)","journal-title":"LNCS"},{"key":"26_CR47","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0747-7171(87)80025-1","volume":"3","author":"K.A. Yelick","year":"1987","unstructured":"Yelick, K.A. Unification in Combinations of Collapse-free Regular Theories. J. of Symbolic Computation 3, pp. 153\u2013181, (1987)","journal-title":"J. of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012845","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T15:35:12Z","timestamp":1683300912000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012845"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/bfb0012845","relation":{},"subject":[]}}