{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:51Z","timestamp":1725456051553},"publisher-location":"Berlin\/Heidelberg","reference-count":43,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354051662X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0018357","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T02:50:09Z","timestamp":1132627809000},"page":"273-299","source":"Crossref","is-referenced-by-count":3,"title":["Unification properties of commutative theories: A categorical treatment"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F. (1987). Unification in Varieties of Idempotent Semigroups. Semigroup Forum 36.","DOI":"10.1007\/BF02575010"},{"key":"17_CR2","unstructured":"Baader, F. (1988). Unification in Commutative Theories. To appear in J. Symbolic Computation."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F. (1989a). Characterizations of Unification Type Zero. Proceedings of the RTA '89 Chapel Hill (USA). Springer Lec. Notes Comp. Sci. 355.","DOI":"10.1007\/3-540-51081-8_96"},{"key":"17_CR4","unstructured":"Baader, F. (1989b). Unification in Commutative Theories, Hilbert's Basis Theorem and Gr\u00f6bner Bases. Preprint."},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., B\u00fcttner, W. (1988). Unification in Commutative Idempotent Monoids. TCS 56.","DOI":"10.1016\/0304-3975(88)90140-5"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Buchberger, B. (1985). Gr\u00f6bner Bases: An Algorithmic Method in Polynomial Ideal Theory. In Bose, N. K. (Ed.). Recent Trends in Multidimensional System Theory.","DOI":"10.1007\/978-94-009-5225-6_6"},{"key":"17_CR7","unstructured":"B\u00fcttner, W. (1986). Unification in the Data Structure Multiset. J. Automated Reasoning 2."},{"key":"17_CR8","unstructured":"Clausen, M., Fortenbacher, A. (1988). Efficient Solution of Linear Diophantine Equations. To appear in J. Symbolic Computation, Special Issue on Unification."},{"key":"17_CR9","unstructured":"Clifford, A.H., Preston, G.B. (1967). The Algebraic Theory of Semigroups, Vol. 2. AMS Mathematical Surveys 7."},{"key":"17_CR10","volume-title":"Universal Algebra","author":"P.M. Cohn","year":"1965","unstructured":"Cohn, P.M. (1965). Universal Algebra. New York: Harper and Row."},{"key":"17_CR11","unstructured":"Fages, F. (1984). Associative-Commutative Unification. Proceedings of the CADE '84 Napa (USA). Springer Lec. Notes Comp. Sci. 170."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Fages, F., Huet, G. (1986). Complete Sets of Unifiers and Matchers in Equational Theories. TCS 43.","DOI":"10.1016\/0304-3975(86)90175-1"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Fortenbacher, A. (1985). An Algebraic Approach to Unification under Associativity and Commutativity. Proceedings of the RTA '85 Dijon (France). Springer Lec. Notes Comp. Sci. 202.","DOI":"10.1007\/3-540-15976-2_19"},{"key":"17_CR14","volume-title":"Abelian Categories","author":"P. Freyd","year":"1964","unstructured":"Freyd, P. (1964). Abelian Categories. New York: Harper and Row."},{"key":"17_CR15","volume-title":"Universal Algebra","author":"G. Gr\u00e4tzer","year":"1968","unstructured":"Gr\u00e4tzer, G. (1968). Universal Algebra. Princeton: Van Nostrand Company."},{"key":"17_CR16","unstructured":"Herold, A. (1987). Combination of Unification Algorithms in Equational Theories. Ph.D. Dissertation, Universit\u00e4t Kaiserslautern."},{"key":"17_CR17","volume-title":"Category Theory","author":"H. Herrlich","year":"1973","unstructured":"Herrlich, H., Strecker, G.E. (1973). Category Theory. Boston: Allyn and Bacon Inc."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Huet, G. (1978). An Algorithm to Generate the Basis of Solutions to Homogeneous Diophantine Equations. Information Processing Letters 7.","DOI":"10.1016\/0020-0190(78)90078-9"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Huet, G. (1980). Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J. ACM 27.","DOI":"10.1145\/322217.322230"},{"key":"17_CR20","volume-title":"Basic Algebra II","author":"N. Jacobson","year":"1980","unstructured":"Jacobson, N. (1980). Basic Algebra II. San Francisco: Freeman and Company."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.L., Maher, M.J. (1984). A Theory of Complete Logic Programs with Equality. J. Logic Programming 1.","DOI":"10.1016\/0743-1066(84)90010-4"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.P. (1983). Confluent and Coherent Equational Term Rewriting Systems, Applications to Proofs in Abstract Data Types. Proceedings of the CAAP '83 Pisa (Italy). Springer Lec. Notes Comp. Sci. 159.","DOI":"10.1007\/3-540-12727-5_16"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.P., Kirchner, H. (1986). Completion of a Set of Rules Modulo a Set of Equations. SIAM J. Comp. 15.","DOI":"10.1137\/0215084"},{"key":"17_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69959-7","volume-title":"Semirings, Automata, Languages","author":"W. Kuich","year":"1986","unstructured":"Kuich, W., Salomaa, A. (1986). Semirings, Automata, Languages. Berlin: Springer Verlag."},{"key":"17_CR25","volume-title":"The Art of Computer Programming, Vol 2","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E. (1973). The Art of Computer Programming, Vol 2. Reading: Addison-Wesley."},{"key":"17_CR26","volume-title":"The Theory of Groups, Vol 1","author":"A.G. Kurosh","year":"1960","unstructured":"Kurosh, A.G. (1960). The Theory of Groups, Vol 1. New York: Chelsea Publishing Company."},{"key":"17_CR27","unstructured":"Lambert, J-L. (1987). Une borne pour les g\u00e9n\u00e9rateurs des solutions enti\u00e8res positives d' une \u00e9quation diophantienne lin\u00e9aire. CRASP 305."},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Lankford, D., Butler, G., Brady, B. (1984). Abelian Group Unification Algorithms for Elementary Terms. Contemporary Mathematics 29.","DOI":"10.1090\/conm\/029\/749246"},{"key":"17_CR29","unstructured":"Lawvere, F.W. (1963). Functional Semantics of Algebraic Theories. Ph.D. Dissertation, Columbia University."},{"key":"17_CR30","unstructured":"Livesey, M., Siekmann, J. (1978). Unification in Sets and Multisets. SEKI Technical Report, Universit\u00e4t Kaiserslautern."},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Makanin, G.S. (1977). The Problem of Solvability of Equations in a Free Semigroup. Mat. Sbornik 103. English transl. in Math USSR Sbornik 32 (1977).","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"17_CR32","unstructured":"Mora, F. (1986). Gr\u00f6bner Bases for Non-Commutative Polynomial Rings. Proceedings of the AAECC3. Springer Lec. Notes Comp. Sci. 228."},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Nash-Williams, C.St.J.A. (1963). On Well-Quasi-Ordering Finite Trees. Proc. Cambridge Philos. Soc. 59.","DOI":"10.1017\/S0305004100003844"},{"key":"17_CR34","unstructured":"Nevins, A.J. (1974). A Human Oriented Logic for Automated Theorem Proving. J. ACM 21."},{"key":"17_CR35","volume-title":"An Introduction to the Theory of Numbers","author":"I. Niven","year":"1972","unstructured":"Niven, I., Zuckerman, H.S. (1972). An Introduction to the Theory of Numbers. New York: John Wiley and Sons."},{"key":"17_CR36","unstructured":"Nutt, W. (1988). Talk at the Second Workshop on Unification, Val d' Ajol (France)."},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Peterson, G., Stickel, M. (1981). Complete Sets of Reductions for Some Equational Theories. J.ACM 28.","DOI":"10.1145\/322248.322251"},{"key":"17_CR38","unstructured":"Plotkin, G. (1972). Building-in Equational Theories. Machine Intelligence 7."},{"key":"17_CR39","unstructured":"Rydeheard, D.E., Burstall, R.M. (1985). A Categorical Unification Algorithm. Proceedings of the Workshop on Category Theory and Computer Programming. Springer Lec. Notes Comp. Sci. 240."},{"key":"17_CR40","unstructured":"Siekmann, J. (1986). Universal Unification. Proceedings of the 7th ECAI."},{"key":"17_CR41","unstructured":"Slage, J.R. (1974). Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity. J. ACM 21."},{"key":"17_CR42","doi-asserted-by":"crossref","unstructured":"Stickel, M. (1981). A Unification Algorithm for Associative-Commutative Functions. J. ACM 28.","DOI":"10.1145\/322261.322262"},{"key":"17_CR43","doi-asserted-by":"crossref","unstructured":"Stickel, M. (1985). Automated Deduction by Theory Resolution. J. Automated Reasoning 1.","DOI":"10.1007\/BF00244275"}],"container-title":["Lecture Notes in Computer Science","Category Theory and Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018357.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:41:12Z","timestamp":1607532072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018357"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354051662X"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/bfb0018357","relation":{},"subject":[]}}