{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T15:57:04Z","timestamp":1794412624582,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540172208","type":"print"},{"value":"9783540474210","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1987]]},"DOI":"10.1007\/3-540-17220-3_18","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T14:14:46Z","timestamp":1330179286000},"page":"204-215","source":"Crossref","is-referenced-by-count":12,"title":["On equational theories, unification and decidability"],"prefix":"10.1007","author":[{"given":"Hans-J\u00fcrgen","family":"B\u00fcrckert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Herold","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,5,26]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1017\/S0305004100013463","volume":"31","author":"G. Birkhoff","year":"1935","unstructured":"Birkhoff, G.: On the Structure of Abstract Algebra, Proc. Cambridge Phil. Soc., Vol. 31, p. 433\u2013454, (1935)","journal-title":"Proc. Cambridge Phil. Soc."},{"key":"18_CR2","unstructured":"B\u00fcrckert, H.-J., Herold, A. and Schmidt-Schau\u00df, M.: On Equational Theories, Unification and Decidability, to appear as SEKI-Report SR-19-86, Universit\u00e4t Kaiserslautern, (1986)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Burris, S. and Sankappanavar, H.P.: A Course in Universal Algebra, Springer, (1981)","DOI":"10.1007\/978-1-4613-8130-3"},{"key":"18_CR4","unstructured":"Book, R. and Siekmann, J.H.: On the Unification Hierarchy, Proc. of GWAI'85, Springer, p. 111\u2013117, (1985)"},{"key":"18_CR5","unstructured":"B\u00fcrckert, H.-J.: Some Relationships between Unification, Restricted Unification and Matching, in Proc. of the 8th CADE, Springer, LNCS 230, p. 514\u2013524, (1986)"},{"key":"18_CR6","unstructured":"Fages, F. and Huet, G.: Unification and Matching in Equational Theories, Proc. of CAAP'83 (ed. G. Ausiello and M. Protasi), Springer, LNCS 159, p. 205\u2013220, (1983). Also in TCS 43, pp. 189\u2013200, (1986)"},{"key":"18_CR7","unstructured":"Goguen, J. A., Thatcher, J.W. and Wagner, E. G.: An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types, in Current Trends in Programming Methodology, Vol.4, Data Structuring (ed. R. T. Yeh), Prentice Hall, (1978)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Gr\u00e4tzer, G.: Universal Algebra, Springer, (1979)","DOI":"10.1007\/978-0-387-77487-9"},{"key":"18_CR9","unstructured":"Herold, A.: A Combination of Unification Algorithms, in Proc. of the 8th CADE, Springer, LNCS 230, p. 450\u2013469, (1986)"},{"key":"18_CR10","unstructured":"Hullot, J.M.: Canonical Forms and Unification, in Proc. of 5th CADE (eds. W. Bibel and R. Kowalski), Springer, LNCS 87, p. 318\u2013334, (1989)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Huet, G. and Oppen, D. C.: Equations and Rewrite Rules: A Survey, in Formal Languages: Perspectives and Open Problems (ed R. Book), Academic Press, (1980)","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"18_CR12","unstructured":"Huet, G.: R\u00e9solution d'\u00e9quations dans des langages d'ordre 1, 2 ... \u03c9, Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 Paris VII, (1976)"},{"key":"18_CR13","volume-title":"Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Reductions, Report ATP-37","author":"D. S. Lankford","year":"1977","unstructured":"Lankford, D.S. and Ballantyne, A.M.: Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Reductions, Report ATP-37, University of Texas, Austin, (1977)"},{"key":"18_CR14","unstructured":"Knuth, D.E. and Bendix, P.B.: Simple Word Problems in Universal Algebras, in Computational Problems in Abstract Algebras (ed. J. Leech), Pergamon Press, p. 263\u2013297, (1970)"},{"key":"18_CR15","unstructured":"Kirchner, C.: Methodes et outils de conception systematique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationelles, Th\u00e8se de doctorat d'\u00e9tat, (in French) Universit\u00e9 de Nancy 1, (1985)"},{"key":"18_CR16","unstructured":"Loveland, D.: Automated Theorem Proving: A Logical Basis, North-Holland, (1978)"},{"key":"18_CR17","first-page":"953","volume":"77","author":"R. Markov","year":"1951","unstructured":"Markov, R.: Impossibility of Algorithms for Recognizing Some Properties of Associative Systems, Dokl. Akad. Nauk SSSR 77, p. 953\u2013956, (1951).","journal-title":"Dokl. Akad. Nauk SSSR"},{"issue":"2","key":"18_CR18","doi-asserted-by":"crossref","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 TOPLAS, Vol.4, No 2, p. 258\u2013282, (1982)","journal-title":"ACM TOPLAS"},{"key":"18_CR19","doi-asserted-by":"crossref","first-page":"151","DOI":"10.2307\/2266280","volume":"17","author":"A. Mostowski","year":"1952","unstructured":"Mostowski, A.: Review of [Ma 51], J. Symbolic Logic 17, p. 151\u2013152, (1952)","journal-title":"J. Symbolic Logic"},{"key":"18_CR20","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0022-0000(85)90051-0","volume":"30","author":"P. Narendran","year":"1985","unstructured":"Narendran, P., O'D\u00fanlaing, C. and Rolletschek, H.: Complexity of Certain Decision Problems About Congruential Languages, Journal of Computer and System Sciences, Vol.30, p. 343\u2013358, (1985)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"18_CR21","doi-asserted-by":"crossref","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, No. 1, p. 23\u201341, (1965)","journal-title":"JACM"},{"issue":"3","key":"18_CR22","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/BF02328450","volume":"2","author":"M. Schmidt-Schau\u00df","year":"1986","unstructured":"Schmidt-Schau\u00df, M.: Unification under Associativity and Idempotence is of Type Nullary, Journal of Automated Reasoning 2,3, pp. 277\u2013281, (1986)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR23","unstructured":"Schmidt-Schau\u00df, M.: Unification Properties of Idempotent Semigroups, SEKI Report SR-86-07, Universit\u00e4t Kaiserslautern, (1986)"},{"key":"18_CR24","unstructured":"Siekmann, J.: Universal Unification, in Proc. of 7th CADE, Springer, LNCS 170, p. 1\u201342, (1984)"},{"key":"18_CR25","unstructured":"Siekmann, J.: Unification Theory, in Proc. of ECAI'86, Vol. II, p. vi\u2013xxxv, Brighton, (1986)"},{"key":"18_CR26","unstructured":"Szab\u00f3, P.: Unifikationstheorie Erster Ordnung, Dissertation (in German), Universit\u00e4t Karlsruhe, (1982)"},{"key":"18_CR27","unstructured":"Taylor, W.: Equational Logic, Houston Journal of Mathematics 5, (1979)"},{"key":"18_CR28","unstructured":"Tid\u00e9n, E.: Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols, in Proc. of 8th CADE, Springer, LCNS 230, p. 431\u2013449, (1986)"},{"key":"18_CR29","unstructured":"Tid\u00e9n, E.: First-Order Unification in Combinations of Equational Theories, Thesis, Stockholm, (1986)"},{"issue":"4","key":"18_CR30","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. Wos","year":"1967","unstructured":"Wos, L., Robinson, G.A., Carson, D. and Shalla, L.: The Concept of Demodulation in Theorem Proving, JACM 14, No. 4, p. 698\u2013709, (1967)","journal-title":"JACM"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Yelick, K.: Combining Unification Algorithms for Confined Regular Equational Theories, in Proc. of RTA'85 (ed J.-P. Jouannaud), Springer, LNCS 202, p. 365\u2013380, (1985)","DOI":"10.1007\/3-540-15976-2_18"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-17220-3_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T13:46:33Z","timestamp":1687268793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-17220-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987]]},"ISBN":["9783540172208","9783540474210"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-17220-3_18","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/3-540-17220-3","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987]]}}}