{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:00Z","timestamp":1767927720940,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540567301","type":"print"},{"value":"9783540476368","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56730-5_29","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:27:33Z","timestamp":1330255653000},"page":"23-42","source":"Crossref","is-referenced-by-count":3,"title":["General A- and AX-unification via optimized combination procedures"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus U.","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"3_CR1","volume-title":"Deduktionssysteme","author":"K.H. Bl\u00c4sius","year":"1987","unstructured":"K.H. Bl\u00c4sius, H.-J. B\u00fcrckert, \u201cDeduktionssysteme,\u201d Oldenbourg Verlag, M\u00fcnchen Wien (1987)."},{"key":"3_CR2","unstructured":"F. Baader, K.U. Schulz, \u201cUnification in the Union of Disjoint Equational Theories: Combining Decision Procedures,\u201d DFKI-Research Report RR-91-33, to appear in the Proceedings of the 11th International Conference on Automated Deduction, LNCS (1992)."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"J.A. Brzozowski, K. Culik, A. Gabrielian, \u201cClassification of Noncounting Events,\u201d J. Computer and System Science 5, 1971.","DOI":"10.1016\/S0022-0000(71)80006-5"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert, \u201cA Resolution Principle for Clauses with Constraints,\u201d Proceedings of the 10th International Conference on Automated Deduction, LNCS 449, 1990.","DOI":"10.1007\/3-540-52885-7_87"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"A. Colmerauer, \u201cAn Introduction to PROLOG III,\u201d C. ACM 33, 1990.","DOI":"10.1145\/79204.79210"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"W.F. Dowling, J. Gallier, \u201cLinear Time Algorithms for Testing Satisfiability of Propositional Horn Formula,\u201d J. Logic Programming 3, 1984.","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"F. Fages, \u201cAssociative-Commutative Unification,\u201d Proceedings of the 7th International Conference on Automated Deduction, LNCS 170, 1984.","DOI":"10.1007\/978-0-387-34768-4_12"},{"key":"3_CR8","unstructured":"J.P. Jouannaud, C. Kirchner, \u201cSolving Equations in Abstract Algebras: A Rule-Based Survey of Unification,\u201d Preprint, 1990. To appear in the Festschrift to Alan Robinson's birthday."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"J. Jaffar, J.L. Lassez, \u201cConstraint Logic Programming,\u201d Proceedings of 14th POPL Conference, Munich, 1987.","DOI":"10.1145\/41625.41635"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"D. Kapur, P. Narendran, \u201cComplexity of Unification Problems with Associative-Commutative Operators,\u201d Preprint, 1991. To appear in J. Automated Reasoning.","DOI":"10.1007\/BF00245463"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"C. Kirchner, H. Kirchner, \u201cConstrained Equational Reasoning,\u201d Proceedings of SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ACM Press, 1989.","DOI":"10.1145\/74540.74585"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"G.S. Makanin, \u201cThe Problem of Solvability of Equations in a Free Semigroup,\u201d Mat. USSR Sbornik 32, 1977.","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"D. McLean, \u201cIdempotent Semigroups,\u201d Am. Math. Mon. 61, 1954.","DOI":"10.2307\/2307797"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\\, \u201cCombination of Unification Algorithms,\u201d J. Symbolic Computation 8, 1989.","DOI":"10.1016\/S0747-7171(89)80037-9"},{"key":"3_CR15","volume-title":"LNCS 572","author":"K.U. Schulz","year":"1990","unstructured":"K.U. Schulz, \u201cMakanin's Algorithm \u2014 Two Improvements and a Generalization,\u201d Proceedings of the First International Workshop on Word Equations and Related Topics IWWERT '90, T\u00fcbingen 1990, Springer LNCS 572."},{"key":"3_CR16","unstructured":"K.U. Schulz, \u201cWord Unification and Transformation of Generalized Equations,\u201d CIS-Report 91-46, University of Munich, 1991 (see also this issue)."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"M. Stickel, \u201cA Unification Algorithm for Associative-Commutative Functions,\u201d J. ACM 28, 1981.","DOI":"10.1145\/322261.322262"}],"container-title":["Lecture Notes in Computer Science","Word Equations and Related Topics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56730-5_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:05:24Z","timestamp":1605647124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56730-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540567301","9783540476368"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-56730-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}