{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:47Z","timestamp":1725456227582},"publisher-location":"Berlin\/Heidelberg","reference-count":22,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012863","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"643-657","source":"Crossref","is-referenced-by-count":1,"title":["A new approach to universal unfication and its application to AC-unification"],"prefix":"10.1007","author":[{"given":"Mark","family":"Franzen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence J.","family":"Henschen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"44_CR1","doi-asserted-by":"crossref","unstructured":"Burris, S., Sankappanavar, H.P. (1981). A Course in Universal Algebra, Springer-Verlag.","DOI":"10.1007\/978-1-4613-8130-3"},{"key":"44_CR2","unstructured":"B\u00fcrckert, H.-J., Herold, A., and Schmidt-Schau\u00df, M. (1987). On Equational Theories, Unification and Decidability, Proc. of RTA'87, Pierre Lescanne, ed., Springer-Verlag, LNCS 256, 204\u2013215."},{"key":"44_CR3","unstructured":"Fages, F. and Huet, G. (1983). Unification and Matching in Equational Theories, Proc. of CAAP'83, Springer-Verlag, LNCS 159, 205\u2013220."},{"key":"44_CR4","unstructured":"Fay, M. (1979). First Order Unification in an Equational Theory, Proc. of 4th Workshop on Automated Deduction, 161\u2013167."},{"key":"44_CR5","unstructured":"Franzen, M. (1988). A Unification Algorithm for Simple Equational Theories, Doctoral Thesis, Northwestern University, forthcoming."},{"key":"44_CR6","first-page":"216","volume":"256","author":"J.H. Gallier","year":"1987","unstructured":"Gallier, J.H. and Snyder, W. (1987). A Genereal Complete E-Unification Procedure, Proc. of RTA'87, Pierre Lescanne, ed., Springer-Verlag, LNCS 256, 216\u2013227.","journal-title":"LNCS"},{"key":"44_CR7","doi-asserted-by":"crossref","unstructured":"Herold, A. (1982). Universal Unification and a Class of Equational Theories, Proc. of GWAI-82 (ed. W. Wahlster), Springer-Verlag, IFB-82, 177\u2013190.","DOI":"10.1007\/978-3-642-68826-3_13"},{"key":"44_CR8","first-page":"450","volume":"230","author":"A. Herold","year":"1985","unstructured":"Herold, A. (1985). A Combination of Unification Algorithms, in Proc. of 8th CADE, Springer-Verlag, LNCS 230, 450\u2013469.","journal-title":"LNCS"},{"key":"44_CR9","doi-asserted-by":"crossref","unstructured":"Huet, G., Oppen, D.C. (1980). Equations and Rewrite Rules: A Survey, in Formal Languages: Perspectives and Open Problems, R. Book, ed., Academic Press, 349\u2013405.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"44_CR10","first-page":"318","volume":"87","author":"J.M. Hullot","year":"1980","unstructured":"Hullot, J.M. (1980). Canonical Forms and Unification, Proc. of 5th CADE, Springer-Verlag, LNCS 87, 318\u2013334.","journal-title":"LNCS"},{"key":"44_CR11","unstructured":"Kirchner, C. (1985). M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories equationelles, Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 de Nancy I."},{"key":"44_CR12","unstructured":"Kirchner, C. (1986). Computing Unification Algorithms, 1st IEEE Symposium on Logic in Computer Science, Cambridge, Massachusetts, June 1986, 206\u2013216."},{"key":"44_CR13","unstructured":"Livesey, M., Siekmann, J. (1976). Unification of A + C Terms (Bags) and A + C + I Terms (Sets), Technical Report Interner Bericht Nr. 3\/76, Institut f\u00fcr Informatik I, Universit\u00e4t Karlsruhe."},{"key":"44_CR14","unstructured":"Martelli, A., Moiso, C., Rossi, G.F. (1986). An Algorithm for Unification in Equational Theories, Proc. 1986 Symposium on Logic Programming, Salt Lake City, 180\u2013186."},{"issue":"2","key":"44_CR15","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U. (1982). An Efficient Unification Algorithm, ACM TOPLAS, Vol. 4, No. 2, 258\u2013282.","journal-title":"ACM TOPLAS"},{"key":"44_CR16","unstructured":"Siekmann, J., Szabo, P. (1981). Universal Unification and Regular ACFM Theories, Proc. of IJCAI-81, Vancouver."},{"key":"44_CR17","first-page":"1","volume":"170","author":"J. Siekmann","year":"1984","unstructured":"Siekmann, J. (1984). Universal Unification, Proc. of 7th CADE, Springer-Verlag, LNCS 170, 1\u201342.","journal-title":"LNCS"},{"key":"44_CR18","unstructured":"Siekmann, J. (1986). Unification Theory, Proc. of ECAI'86, Vol. II, vi-xxxv."},{"key":"44_CR19","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M.E. Stickel","year":"1981","unstructured":"Stickel, M.E. (1981). A Unification Algorithm for Associative-Commutative Functions, JACM, vol. 28, 423\u2013434.","journal-title":"JACM"},{"key":"44_CR20","first-page":"431","volume":"230","author":"E. Tiden","year":"1986","unstructured":"Tiden, E. (1986). Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols, Proc. of 8th CADE, Springer-Verlag, LNCS 230, 431\u2013449.","journal-title":"LNCS"},{"key":"44_CR21","first-page":"365","volume":"202","author":"K. Yelick","year":"1985","unstructured":"Yelick, K. (1985). Combining Unification Algorithms for Confined Regular Equational Theories, Proc. of RTA'85, Springer-Verlag, LNCS 202, 365\u2013380.","journal-title":"LNCS"},{"key":"44_CR22","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0747-7171(87)80025-1","volume":"3","author":"K. Yelick","year":"1987","unstructured":"Yelick, K. (1987). Unification in Combinations of Collapse-Free Regular Theories, J. Symbolic Computation, vol. 3, 153\u2013181.","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012863.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:43Z","timestamp":1607353603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0012863","relation":{},"subject":[]}}