{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:47Z","timestamp":1767929267197,"version":"3.49.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1996,7,1]],"date-time":"1996-07-01T00:00:00Z","timestamp":836179200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[1996,7]]},"DOI":"10.1007\/bf01195536","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T06:10:49Z","timestamp":1108707049000},"page":"309-337","source":"Crossref","is-referenced-by-count":11,"title":["Combination problems for commutative\/monoidal theories or how algebra can help in equational unification"],"prefix":"10.1007","volume":"7","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Werner","family":"Nutt","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1016\/S0747-7171(89)80055-0","volume":"8","author":"F. Baader","year":"1989","unstructured":"Baader, F.: Unification in Commutative Theories. J. Symb. Computation8, 479?497 (1989)","journal-title":"J. Symb. Computation"},{"key":"CR2","series-title":"Lecture Notes in Computer Science, Vol. 389","volume-title":"Proceedings of the Conference on Category Theory and Computer Science","author":"F. Baader","year":"1989","unstructured":"Baader, F.: Unification Properties of Commutative Theories: A Categorical Treatment. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poign\u00e9, A. (eds.) Proceedings of the Conference on Category Theory and Computer Science. Lecture Notes in Computer Science, Vol. 389. Berlin, Heidelberg, New York: Springer 1989"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1145\/174130.174133","volume":"40","author":"F. Baader","year":"1993","unstructured":"Baader, F.: Unification in Commutative Theories, Hubert's Basis Theorem, and Gr\u00f6bner Bases. J. ACM40, 477?503 (1993)","journal-title":"J. ACM"},{"key":"CR4","series-title":"Lecture Notes in Computer Science, Vol 488","volume-title":"Proceedings of the 4th International Conference on Rewriting Techniques and Applications","author":"F. Baader","year":"1991","unstructured":"Baader, F., Nutt, W.: Adding Homomorphisms to Commutative\/Monoidal Theories or How Algebra Can Help in Equational Unification. In: Book, R. (ed.) Proceedings of the 4th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, Vol 488. Berlin, Heidelberg, New York: Springer 1991"},{"key":"CR5","series-title":"Lecture Notes in Computer Science, Vol. 607","volume-title":"Proceedings of the 11th International Conference on Automated Deduction","author":"F. Baader","year":"1992","unstructured":"Baader, F., Schulz, K. U.: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. In: Kapur, D. (ed.) Proceedings of the 11th International Conference on Automated Deduction. Lecture Notes in Computer Science, Vol. 607. Berlin, Heidelberg, New York: Springer 1992"},{"key":"CR6","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"F. Baader","year":"1994","unstructured":"Baader, F., Siekmann, J. H.: Unification Theory. In: Gabbay, D. M., Hogger, C. J., Robinson, J. A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford: Oxford University Press 1994"},{"key":"CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L.: Canonical Equational Proofs. Boston, Basel, Berlin: Birkh\u00e4user 1991"},{"key":"CR8","volume-title":"Universal Algebra","author":"P. M. Cohn","year":"1965","unstructured":"Cohn, P. M.: Universal Algebra. New York: Harper and Row 1965"},{"key":"CR9","volume-title":"Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science","author":"H. Comon","year":"1992","unstructured":"Comon, H., Haberstrau, M., Jouannaud, J.-P.: Decidable Problems in Shallow Equational Theories. In: Scedrov, A. (ed.) Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science. Washington D.C.: IEEE Computer Society Press 1992"},{"key":"CR10","volume-title":"Handbook of Mathematical Logic","author":"M. Davis","year":"1977","unstructured":"Davis, M.: Unsolvable Problems. In: Barwise, J. (ed.) Handbook of Mathematical Logic. Amsterdam: Elsevier Science Publishers 1977"},{"key":"CR11","unstructured":"Fay, M.: First-order Unification in an Equational Theory. In: Proceedings 4th Workshop on Automated Deduction 1979"},{"key":"CR12","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"M. Fitting","year":"1993","unstructured":"Fitting, M.: Basic Modal Logic. In: Gabbay, D. M., Hogger, C. J., Robinson, J. A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford: Oxford University Press 1993"},{"key":"CR13","volume-title":"Proceedings of the 3rd IEEE Symposium on Logic Programming","author":"J. Gallier","year":"1986","unstructured":"Gallier, J., Raatz, S.: SLD-Resolution Methods for Horn Clauses with Equality Based onE-Unification. In: Keller, R. M. (ed.) Proceedings of the 3rd IEEE Symposium on Logic Programming. Washington D.C.: IEEE Computer Society Press 1986"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"27","author":"J. Gallier","year":"1989","unstructured":"Gallier, J., Snyder, S.: Complete Sets of Transformations for General E-Unification. Theor. Comput. Sci.27, 203?260 (1989)","journal-title":"Theor. Comput. Sci."},{"key":"CR15","volume-title":"Universal Algebra","author":"G. Gr\u00e4tzer","year":"1968","unstructured":"Gr\u00e4tzer, G.: Universal Algebra. Princeton: Van Nostrand 1968"},{"key":"CR16","volume-title":"Category Theory","author":"H. Herrlich","year":"1973","unstructured":"Herrlich, H., Strecker, G. E.: Category Theory. Boston: Allyn and Bacon 1973"},{"key":"CR17","doi-asserted-by":"crossref","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. J. ACM27, 797?821 (1980)","journal-title":"J. ACM"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0743-1066(84)90010-4","volume":"1","author":"J. Jaffar","year":"1984","unstructured":"Jaffar, J., Lassez, J. L., Maher, M.: A Theory of Complete Logic Programs with Equality. J. Logic Programming1, 211?224 (1984)","journal-title":"J. Logic Programming"},{"key":"CR19","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. P. Jouannaud","year":"1986","unstructured":"Jouannaud, J. P., Kirchner, H.: Completion of a Set of Rules Modulo a Set of Equations. SIAM J. Comp.15, 1155?1194 (1986)","journal-title":"SIAM J. Comp."},{"key":"CR20","volume-title":"Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Klay, F.: Syntactic Theories and Unification. In: Mitchell, J. (ed.) Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. Washington D.C.: IEEE Computer Society Press 1990"},{"key":"CR21","volume-title":"Ph.D. Thesis","author":"F. W. Lawvere","year":"1963","unstructured":"Lawvere, F. W.: Functional Semantics of Algebraic Theories. Ph.D. Thesis, Columbia University, New York (1963)"},{"key":"CR22","doi-asserted-by":"crossref","first-page":"46","DOI":"10.2307\/2270619","volume":"31","author":"E. J. Lemmon","year":"1966","unstructured":"Lemmon, E. J.: Algebraic Semantics for Modal Logics I. J. Symbolic Logic31, 46?65 (1966)","journal-title":"J. Symbolic Logic"},{"key":"CR23","unstructured":"Livesey, M., Siekmann, J.: Unification of Bags and Sets. SEKI-MEMO 76-II, Institut f\u00fcr Informatik I, Universit\u00e4t Karlsruhe (1976)"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"606","DOI":"10.1145\/321850.321858","volume":"21","author":"A. J. Nevins","year":"1974","unstructured":"Nevins, A. J.: A Human Oriented Logic for Automated Theorem Proving. J. ACM21, 606?621 (1974)","journal-title":"J. ACM"},{"key":"CR25","volume-title":"Unification in Monoidal Theories, Presentation at the Second Workshop on Unification","author":"W. Nutt","year":"1988","unstructured":"Nutt, W.: Unification in Monoidal Theories, Presentation at the Second Workshop on Unification. Val d'Ajol, France, (1988)"},{"key":"CR26","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W. Nutt","year":"1989","unstructured":"Nutt, W., R\u00e9ty, P., Smolka, G.: Basic Narrowing Revisited. J. Symb. Computation7, 295?317 (1989)","journal-title":"J. Symb. Computation"},{"key":"CR27","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BF00249020","volume":"7","author":"W. Nutt","year":"1991","unstructured":"Nutt, W.: The Unification Hierarchy is Undecidable. J. Automated Reasoning7, 369?381 (1991)","journal-title":"J. Automated Reasoning"},{"key":"CR28","series-title":"Lecture Notes in Computer Science, Vol. 499","volume-title":"Proceedings 10th International Conference on Automated Deduction","author":"W. Nutt","year":"1990","unstructured":"Nutt, W.: Unification in Monoidal Theories. In: Stickel, M. (ed.) Proceedings 10th International Conference on Automated Deduction. Lecture Notes in Computer Science, Vol. 499. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR29","volume-title":"Technical Report RR-92-01","author":"W. Nutt","year":"1992","unstructured":"Nutt, W.: Unification in Monoidal Theories is Solving Linear Equations over Semirings. Technical Report RR-92-01, DFKI Saarbr\u00fccken (1992)"},{"key":"CR30","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson, G., Stickel, M.: Complete Sets of Reductions for Some Equational Theories. J. ACM28, 233?264 (1981)","journal-title":"J. ACM"},{"key":"CR31","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G.: Building in Equational Theories. Machine Intelligence7, 73?90 (1972)","journal-title":"Machine Intelligence"},{"key":"CR32","volume-title":"The Theory of Groups","author":"J. J. Rotman","year":"1973","unstructured":"Rotman, J. J.: The Theory of Groups. Boston: Allyn and Bacon 1973"},{"key":"CR33","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"Schmidt-Schau\u00df, M.: Combination of Unification Algorithms. J. Symbolic Computation8, 51?99 (1989)","journal-title":"J. Symbolic Computation"},{"key":"CR34","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. R. Slagle","year":"1974","unstructured":"Slagle, J. R.: Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity. J. ACM21, 622?642 (1974)","journal-title":"J. ACM"},{"key":"CR35","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"Stickel, M.: Automated Deduction by Theory Resolution. J. Automated Reasoning1, 333?355 (1985)","journal-title":"J. Automated Reasoning"},{"key":"CR36","first-page":"1","volume":"5","author":"W. Taylor","year":"1979","unstructured":"Taylor, W.: Equational Logic. Houston J. Math.5, 1?51 (1979)","journal-title":"Houston J. Math."}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01195536.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01195536\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01195536","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T09:09:55Z","timestamp":1556615395000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01195536"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,7]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1996,7]]}},"alternative-id":["BF01195536"],"URL":"https:\/\/doi.org\/10.1007\/bf01195536","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,7]]}}}