{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T16:52:45Z","timestamp":1773939165120,"version":"3.50.1"},"reference-count":184,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50010-2","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"445-533","source":"Crossref","is-referenced-by-count":200,"title":["Unification Theory"],"prefix":"10.1016","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Wayne","family":"Snyder","sequence":"additional","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]},{"given":"Manfred","family":"Schmidt-Schauss","sequence":"additional","affiliation":[]},{"given":"Klaus","family":"Schulz","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"5","key":"10.1016\/B978-044450813-3\/50010-2_bb0010","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1016\/S0747-7171(89)80056-2","article-title":"Solving word equations","volume":"8","author":"Abdulrab","year":"1989","journal-title":"J. Symbolic Computation"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_bb0015","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","article-title":"Modal theorem proving: An equational viewpoint","volume":"2","author":"Auffray","year":"1992","journal-title":"J. Logic and Computation"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_bb0020","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BF02328451","article-title":"Unification in idempotent semigroups is of type zero","volume":"2","author":"Baader","year":"1986","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0025","series-title":"Proceedings of the 3rd International Conference on Rewriting Techniques and Applications","first-page":"2","article-title":"Characterizations of unification type zero","author":"Baader","year":"1989"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50010-2_bb0030","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1016\/S0747-7171(89)80055-0","article-title":"Unification in commutative theories","volume":"8","author":"Baader","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0035","series-title":"Proceedings of the 4th International Conference on Rewriting Techniques and Applications","first-page":"86","article-title":"Unification, weak unification, upper bound, lower bound, and generalization problems","author":"Baader","year":"1991"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_bb0040","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1145\/174130.174133","article-title":"Unification in commutative theories, Hilbert's basis theorem and Gr\u00f6bner bases","volume":"40","author":"Baader","year":"1993","journal-title":"J. of the ACM"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0045","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/S0020-0190(98)00106-9","article-title":"On the complexity of Boolean unification","volume":"67","author":"Baader","year":"1998","journal-title":"Information Processing Letters"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0050","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1016\/0304-3975(88)90140-5","article-title":"Unification in commutative idempotent monoids","volume":"56","author":"Baader","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0055","series-title":"Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98)","first-page":"331","article-title":"Unification of concept terms in description logics","author":"Baader","year":"1998"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0060","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF01195536","article-title":"Combination problems for commutative\/monoidal theories: How algebra can help in equational reasoning","volume":"7","author":"Baader","year":"1996","journal-title":"J. Applicable Algebra in Engineering, Communication and Computing"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0065","series-title":"Proceedings of the 11th International Conference on Automated Deduction","first-page":"50","article-title":"Unification in the union of disjoint equational theories: Combining decision procedures","author":"Baader","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0070","series-title":"Proceedings of the 5th International Conference on Rewriting Techniques and Applications","first-page":"301","article-title":"Combination techniques and decision problems for disunification","author":"Baader","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50010-2_rf0075","series-title":"Proceedings of the Second International Workshop on Word Equations and Related Topics","first-page":"23","article-title":"General A- and AX-unification via optimized combination procedures","author":"Baader","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0080","series-title":"Proceedings of the 6th International Conference on Rewriting Techniques and Applications","first-page":"352","article-title":"Combination of constraint solving techniques: An algebraic point of view","author":"Baader","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0085","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0304-3975(94)00277-0","article-title":"Combination techniques and decision problems for disunification","volume":"142","author":"Baader","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0090","series-title":"Proceedings of the International Conference on Principles and Practice of Constraint Programming, CP95","first-page":"380","article-title":"On the combination of symbolic constraints, solution domains, and constraint solvers","author":"Baader","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0095","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1006\/jsco.1996.0009","article-title":"Unification in the union of disjoint equational theories: Combining decision procedures","volume":"21","author":"Baader","year":"1996","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0100","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/S0304-3975(97)00147-3","article-title":"Combination of constraint solvers for free and quasi-free structures","volume":"192","author":"Baader","year":"1998","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0105","first-page":"41","article-title":"Unification theory","author":"Baader","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0110","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0115","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","article-title":"Basic paramodulation","volume":"121","author":"Bachmair","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0120","series-title":"Proceedings of the 1st International Conference on Rewriting Techniques and Applications","first-page":"417","article-title":"Complexity of matching problems","author":"Benanav","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0125","series-title":"Proceedings of the 1st International Workshop on Word Equations and Related Topics (IWWERT '90)","first-page":"171","article-title":"Algebraic and logical aspects of unification","author":"Bockmayr","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0130","series-title":"Proceedings of the 3rd International Workshop on Conditional and Typed Term Rewriting Systems","article-title":"An optimal narrowing strategy for general canonical systems","author":"Bockmayr","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0135","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1016\/S0747-7171(89)80054-9","article-title":"Combining unification algorithms","volume":"8","author":"Boudet","year":"1993","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0140","series-title":"Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science","first-page":"141","article-title":"A new AC-unification algorithm with a new algorithm for solving diophantine equations","author":"Boudet","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0145","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1016\/S0747-7171(89)80054-9","article-title":"Unification in Boolean rings and Abelian groups","volume":"8","author":"Boudet","year":"1989","journal-title":"J. Symbolic Computation"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0150","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1145\/179812.179813","article-title":"On solving equations and disequations","volume":"41","author":"Buntine","year":"1994","journal-title":"J. of the ACM"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0155","series-title":"Proceedings of the 9th International Conference on Automated Deduction","article-title":"Solving disequations in equational theories","author":"B\u00fcrckert","year":"1988"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50010-2_bb0160","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1016\/S0747-7171(89)80057-4","article-title":"Matching\u2014a special case of unification?","volume":"8","author":"B\u00fcrckert","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_rf0165","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-55034-8","article-title":"A resolution Principle for a Logic with Restricted Quantifiers","author":"B\u00fcrckert","year":"1991"},{"issue":"3,4","key":"10.1016\/B978-044450813-3\/50010-2_bb0170","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(89)80021-5","article-title":"On equational theories, unification, and decidability","volume":"8","author":"B\u00fcrckert","year":"1989","journal-title":"J. Symbolic Computation"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0175","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0020-0190(90)90183-X","article-title":"Unification in commutative rings is not finitary","volume":"36","author":"Burris","year":"1990","journal-title":"Information Processing Letters"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0180","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF00246024","article-title":"Unification in the data structure multiset","volume":"2","author":"B\u00fcttner","year":"1986","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0185","series-title":"Proceedings of the 8th International Conference on Automated Deduction","first-page":"470","article-title":"Unification in the data structure sets","author":"B\u00fcttner","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0190","series-title":"Proceedings of the 9th International Conference on Automated Deduction","first-page":"368","article-title":"Unification in finite algebras is unitary(?)","author":"B\u00fcttner","year":"1988"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0195","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF01810294","article-title":"Symbolic constraint handling through unification in finite algebras","volume":"1","author":"B\u00fcttner","year":"1990","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0200","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/S0747-7171(87)80065-2","article-title":"Embedding Boolean expressions into logic programming","volume":"4","author":"B\u00fcttner","year":"1987","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0205","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0022-0000(86)90003-6","article-title":"About the Paterson-Wegman linear unification algorithm","volume":"32","author":"Champeaux","year":"1986","journal-title":"J. Computer and System Sciences"},{"issue":"1,2","key":"10.1016\/B978-044450813-3\/50010-2_bb0210","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0747-7171(89)80025-2","article-title":"Efficient solution of linear diophantine equations","volume":"8","author":"Clausen","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0215","series-title":"Universal Algebra","author":"Cohn","year":"1965"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0220","series-title":"Proceedings of the International Conference on Fifth Generation Computer Systems","first-page":"85","article-title":"Equations and inequations on finite and infinite trees","author":"Colmerauer","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0225","article-title":"Unification et Disunification: Th\u00e9orie et Applications","author":"Comon","year":"1988","journal-title":"Ph.D. thesis, Institut National Polytechnique de Grenoble, Grenoble, France"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0230","series-title":"Proceedings of the 3rd International Conference on Rewriting Techniques and Applications","first-page":"76","article-title":"Inductive proofs by specification transformation","author":"Comon","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0235","series-title":"Computational Logic: Essays in Honor of Alan Robinson","first-page":"322","article-title":"Disunification: A survey","author":"Comon","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0240","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","article-title":"Equational problems and disunification","volume":"7","author":"Comon","year":"1989","journal-title":"J. Symbolic Computation"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50010-2_bb0245","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1006\/jsco.1993.1060","article-title":"Solving \u2217-Problems Modulo Distributivity by a Reduction to AC1-Unification","volume":"16","author":"Contejean","year":"1993","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0250","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1006\/inco.1994.1067","article-title":"An efficient incremental algorithm for solving systems of linear diophantine equations","volume":"113","author":"Contejean","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0255","series-title":"Proceedings of the 9th World Computer Congress, IFIP'83","first-page":"909","article-title":"A rehabilitation of Robinson's unification algorithm","author":"Corbin","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50010-2_rf0260","doi-asserted-by":"crossref","first-page":"233","DOI":"10.2307\/2318447","article-title":"Hilbert's tenth problem is unsolvable","volume":"80","author":"Davis","year":"1973","journal-title":"American Mathematical Monthly"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0265","first-page":"609","article-title":"Equality reasoning in sequent-based calculi","volume":"Vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0270","series-title":"\u2018Handbook of Theoretical Computer Science\u2019, Vol. B: Formal Methods and Semantics","first-page":"243","article-title":"Rewrite systems","author":"Dershowitz","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0275","first-page":"162","article-title":"Notations for rewriting","volume":"43","author":"Dershowitz","year":"1991","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0280","first-page":"533","article-title":"Rewriting","volume":"Vol. I","author":"Dershowitz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0285","doi-asserted-by":"crossref","first-page":"413","DOI":"10.2307\/2370405","article-title":"Finiteness of the odd perfect and primitive abundant numbers with r distinct prime factors","volume":"35","author":"Dickson","year":"1913","journal-title":"Amer. Journal of Math."},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0290","article-title":"Outils pour la d\u00e9duction automatique dans les th\u00e9ories associatives-commutatives","author":"Domenjoud","year":"1991","journal-title":"Th\u00e8se de Doctorat, Universit\u00e9 de Nancy I, France"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0295","series-title":"Proceedings of the 12th International Conference on Automated Deduction","first-page":"267","article-title":"Combination techniques for non-disjoint equational theories","author":"Domenjoud","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0300","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0747-7171(92)90010-2","article-title":"An improved general E-unification method","volume":"14","author":"Dougherty","year":"1992","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0305","first-page":"1009","article-title":"Higher-order unification and matching","volume":"Vol. II","author":"Dowek","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0310","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0743-1066(84)90022-0","article-title":"On the sequential nature of unification","volume":"1","author":"Dwork","year":"1984","journal-title":"J. Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0315","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0747-7171(85)80027-4","article-title":"Properties of substitutions and unifications","volume":"1","author":"Eder","year":"1985","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0320","article-title":"Formes Canoniques dans les Alg\u00e8bres Bool\u00e9ennes, et Application \u00e0 la D\u00e9monstration Automatique en Logique de Premier Ordre","author":"Fages","year":"1983","journal-title":"Th\u00e8se de 3\u00e8me cycle, Universit\u00e9 Paris VI"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0325","series-title":"Proceedings of the 7th International Conference on Automated Deduction","first-page":"194","article-title":"Associative-commutative unification","author":"Fages","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0330","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0747-7171(87)80004-4","article-title":"Associative-commutative unification","volume":"3","author":"Fages","year":"1987","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0335","series-title":"Proceedings of the 5th Colloquium on Automata, Algebra, and Programming","first-page":"205","article-title":"Complete sets of unifiers and matchers in equational theories","author":"Fages","year":"1983"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0340","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0304-3975(86)90175-1","article-title":"Complete sets of unifiers and matchers in equational theories","volume":"43","author":"Fages","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0345","series-title":"Proceedings 4th Workshop on Automated Deduction","first-page":"161","article-title":"First-order unification in an equational theory","author":"Fay","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0350","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1006\/jsco.1995.1029","article-title":"A fast method for finding the basis of nonnegative solutions to a linear diophantine equation","volume":"19","author":"Filgueira","year":"1995","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0355","series-title":"Proceedings of the 1st International Conference on Rewriting Techniques and Applications","first-page":"381","article-title":"An algebraic approach to unification under associativity and commutativity","author":"Fortenbacher","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0360","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/BF00245459","article-title":"Hilbert's tenth problem is of unification type zero","volume":"9","author":"Franzen","year":"1992","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0365","series-title":"Proceedings of the 11th International Conference on Automated Deduction","first-page":"178","article-title":"An abstract view of sorted unification","author":"Frisch","year":"1992"},{"issue":"2,3","key":"10.1016\/B978-044450813-3\/50010-2_bb0370","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","article-title":"Complete sets of transformations for general E-unification","volume":"67","author":"Gallier","year":"1989","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0375","series-title":"Computers and Intractability. A Guide to the Theory of NP-completeness","author":"Garey","year":"1979"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50010-2_bb0380","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1093\/logcom\/7.6.733","article-title":"Unification through projectivity","volume":"7","author":"Ghilardi","year":"1997","journal-title":"J. Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0385","series-title":"Resolution of Equations in Algebraic Structures, Volume 1, Algebraic Techniques","first-page":"217","article-title":"What is unification?","author":"Goguen","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50010-2_rf0390","series-title":"Universal Algebra","author":"Gr\u00e4tzer","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0395","article-title":"Automated logic for semi-automated mathematics","author":"Guard","year":"1964","journal-title":"Scientific Report 1, AFCRL 64-411, Air Force Cambridge Lab."},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0400","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/321495.321500","article-title":"Semi-automated mathematics","volume":"16","author":"Guard","year":"1969","journal-title":"J. of the ACM"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0405","series-title":"Proceedings of the 9th International Conference on Rewriting Techniques and Applications","first-page":"91","article-title":"Unification and matching in process algebras","author":"Guo","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0410","series-title":"Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science FOCS'98","article-title":"Solvability of word equations is in exponential space","author":"Guti\u00e9rrez","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0415","article-title":"Recherches sur la Th\u00e9orie de la D\u00e9monstration","author":"Herbrand","year":"1930","journal-title":"Ph.D. thesis, Sorbonne, Paris"},{"issue":"128","key":"10.1016\/B978-044450813-3\/50010-2_bb0420","article-title":"Recherches sur la th\u00e9orie de la D\u00e9monstration","volume":"33","author":"Herbrand","year":"1930","journal-title":"Travaux de la Soci\u00e9t\u00e9 des Sciences et des Lettres de Varsovie, Classe III"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0425","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","first-page":"525","article-title":"Investigations in proof theory: The properties of true propositions","author":"Herbrand","year":"1967"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0430","series-title":"Logical Writings","article-title":"Recherches sur la th\u00e9orie de la d\u00e9monstration","author":"Herbrand","year":"1971"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0435","series-title":"Proceedings of the 13th International Conference on Automated Deduction","first-page":"246","article-title":"Unification algorithms cannot be combined in polynomial time","author":"Hermann","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0440","series-title":"Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP'97)","first-page":"283","article-title":"On the complexity of unification and disunification in commutative idempotent semigroups","author":"Hermann","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0445","series-title":"Proceedings of the 8th International Conference on Automated Deduction","first-page":"450","article-title":"Combination of unification algorithms","author":"Herold","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0450","article-title":"Combination of Unification Algorithms in Equational Theories","author":"Herold","year":"1987","journal-title":"Ph.D. thesis, Universit\u00e4t Kaiserslautern, Kaiserslautern, Germany"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0455","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/BF00243791","article-title":"Unification in Abelian semigroups","volume":"3","author":"Herold","year":"1987","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0460","series-title":"Category Theory","author":"Herrlich","year":"1973"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0465","article-title":"R\u00e9solution d'\u00c9quations dans des Langages d'ordre 1,2,\u2026,\u03c9","author":"Huet","year":"1976","journal-title":"Th\u00e8se d\u2018\u00c9tat, Universit\u00e9 de Paris VII"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_bb0470","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/0020-0190(78)90078-9","article-title":"An algorithm to generate the basis of solutions to homogeneous linear diophantine equations","volume":"7","author":"Huet","year":"1978","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0475","series-title":"Proceedings of the 5th International Conference on Automated Deduction","first-page":"318","article-title":"Canonical forms and unification","author":"Hullot","year":"1980"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0480","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1137\/0218045","article-title":"Worst-case complexity bounds on algorithms for computing the canonical structure of finite Abelian groups and the Hermite and Smith normal forms of an integer matrix","volume":"18","author":"Iliopoulos","year":"1989","journal-title":"SIAM J. Computing"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0485","doi-asserted-by":"crossref","first-page":"670","DOI":"10.1137\/0218046","article-title":"Worst-case complexity bounds on algorithms for computing the canonical structure of infinite Abelian groups and solving systems of linear diophantine equations","volume":"18","author":"Iliopoulos","year":"1989","journal-title":"SIAM J. Computing"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0490","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/78935.78938","article-title":"Minimal and complete word unification","volume":"37","author":"Jaffar","year":"1990","journal-title":"J. of the ACM"},{"key":"10.1016\/B978-044450813-3\/50010-2_rf0495","series-title":"Computational Logic: Essays in Honor of A. Robinson","article-title":"Solving equations in abstract algebras: A rule-based survey of unification","author":"Jouannaud","year":"1991"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0500","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","article-title":"Completion of a set of rules modulo a set of equations","volume":"15","author":"Jouannaud","year":"1986","journal-title":"SIAM J. Computing"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0505","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1137\/0208040","article-title":"Algorithms for computing the Smith and Hermite normal forms of an integer matrix","volume":"8","author":"Kannan","year":"1979","journal-title":"SIAM J. Computing"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0510","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BF00245463","article-title":"Complexity of unification problems with associative-commutative operators","volume":"9","author":"Kapur","year":"1992","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0515","series-title":"Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science","first-page":"11","article-title":"Double exponential complexity of computing complete sets of AC-unifiers","author":"Kapur","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0520","series-title":"Frontiers of Combining Systems 2, Papers presented at FroCoS'98","first-page":"117","article-title":"Negation in combining constraint systems","author":"Kepser","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0525","series-title":"Frontiers of Combining Systems 2, Papers presented at FroCoS'98","first-page":"193","article-title":"Optimisation techniques for combining constraint solvers","author":"Kepser","year":"1999"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0530","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1006\/inco.1993.1003","article-title":"The undecidability of the semi-unification problem","volume":"102","author":"Kfoury","year":"1993","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0535","article-title":"M\u00e9thodes et Outils de Conception Syst\u00e9matique d'Algorithmes d'Unification dans les Th\u00e9ories Equationelles","author":"Kirchner","year":"1985","journal-title":"Th\u00e8se d'\u00c9tat, Universit\u00e9 de Nancy I, l France"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0540","series-title":"Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation","article-title":"Constrained equational reasoning","author":"Kirchner","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0545","series-title":"Proceedings of the Annual IEEE Symposium on Logic in Computer Science","first-page":"347","article-title":"Solving disequations","author":"Kirchner","year":"1987"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0550","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1006\/jsco.1994.1040","article-title":"Combining symbolic constraint solvers on algebraic domains","volume":"18","author":"Kirchner","year":"1994","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0555","series-title":"Computer Science and Information Processing","article-title":"The Art of Computer Programming, Vol. 2: Seminumerical Algorithms","author":"Knuth","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0560","series-title":"Computational Problems in Abstract Algebra","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0565","series-title":"Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science","first-page":"824","article-title":"Complexity of unification in free groups and free semigroups","author":"Koscielski","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0570","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1147\/rd.254.0327","article-title":"Positive first-order logic is NP-complete","volume":"25","author":"Kozen","year":"1981","journal-title":"IBM Journal for Research and Development"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0575","first-page":"39","article-title":"Une borne pour les g\u00e9n\u00e9rateurs des solutions enti\u00e8res positives d'une \u00e9quation diophantienne lin\u00e9aire","volume":"305","author":"Lambert","year":"1987","journal-title":"Comptes Rendus de l'Acad\u00e9mie des Sciences de Paris"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0580","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1090\/conm\/029\/749246","article-title":"Abelian group unification algorithms for elementary terms","volume":"29","author":"Lankford","year":"1984","journal-title":"Contemporary Mathematics"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0585","series-title":"Foundations of Deductive Databases and Logic Programming","first-page":"587","article-title":"Unification revisited","author":"Lassez","year":"1987"},{"issue":"1,2","key":"10.1016\/B978-044450813-3\/50010-2_bb0590","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0747-7171(89)80026-4","article-title":"Adventures in associative-commutative unification","volume":"8","author":"Lincoln","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0595","article-title":"Unification of AC-terms (bags) and ACI-terms (sets), Internal report, University of Essex","author":"Livesey","year":"1975","journal-title":"Also published as Technical Report 3-76, Universit\u00e4t Karlsruhe"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0600","first-page":"147","article-title":"The problem of solvability of equations in a free semigroup","volume":"103","author":"Makanin","year":"1977","journal-title":"Math. Sbornik"},{"key":"10.1016\/B978-044450813-3\/50010-2_rf0605","article-title":"The Metamathematics of Algebraic Systems","author":"Mal'cev","year":"1971"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0610","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-65374-2","article-title":"Algebraic Systems","author":"Mal'cev","year":"1973"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0615","article-title":"Unification in linear time and space: A structured presentation","author":"Martelli","year":"1976","journal-title":"Technical Report B76-16, University of Pisa"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0620","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3,4","key":"10.1016\/B978-044450813-3\/50010-2_bb0625","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/S0747-7171(89)80013-6","article-title":"Boolean unification\u2014The story so far","volume":"7","author":"Martin","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0630","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF00297246","article-title":"Unification in Boolean rings","volume":"4","author":"Martin","year":"1989","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0635","first-page":"3","article-title":"Diophantine representation of recursively enumerable predicates","volume":"35","author":"Matiyasevich","year":"1971","journal-title":"Ak. Nauk USSR, Ser. Math."},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0640","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1016\/S0747-7171(89)80036-7","article-title":"Order-sorted unification","volume":"8","author":"Meseguer","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0645","series-title":"Proceedings of the 5th International Conference on Rewriting Techniques and Applications","first-page":"92","article-title":"Improving transformation systems for general E-unification","author":"Moser","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0650","series-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science","first-page":"466","article-title":"Solving linear equations over polynomial semirings","author":"Narendran","year":"1996"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0655","doi-asserted-by":"crossref","first-page":"49","DOI":"10.3233\/FI-1996-25105","article-title":"Unification modulo ACI+1+0","volume":"25","author":"Narendran","year":"1996","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0660","series-title":"Proceedings of the 10th International Conference on Automated Deduction","first-page":"276","article-title":"Some results on equational unification","author":"Narendran","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0665","series-title":"Proceedings of the 12th International Conference on Automated Deduction","first-page":"545","article-title":"AC-superposition with constraints: No AC-unifiers needed","author":"Nieuwenhuis","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0670","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0675","doi-asserted-by":"crossref","first-page":"742","DOI":"10.1145\/96559.96569","article-title":"Unification in primal algebras, their powers and their varieties","volume":"37","author":"Nipkow","year":"1990","journal-title":"J. of the ACM"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0680","series-title":"Proceedings of the 10th International Conference on Automated Deduction","first-page":"618","article-title":"Unification in monoidal theories","author":"Nutt","year":"1990"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_bb0685","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BF00249020","article-title":"The unification hierarchy is undecidable","volume":"7","author":"Nutt","year":"1991","journal-title":"J. Automated Reasoning"},{"issue":"3,4","key":"10.1016\/B978-044450813-3\/50010-2_bb0690","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","article-title":"Basic narrowing revisited","volume":"7","author":"Nutt","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0695","series-title":"Proceedings of the 15th International Conference on Automated Deduction","first-page":"239","article-title":"A fast algorithm for uniform semiunification","author":"Oliart","year":"1998"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0700","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","article-title":"Linear unification","volume":"16","author":"Paterson","year":"1978","journal-title":"J. Computer and System Sciences"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0705","article-title":"\u00c9quations avec constantes et algorithme de Makanin","author":"P\u00e9cuchet","year":"1981","journal-title":"Th\u00e8se de doctorat, Laboratoire d'Informatique, University of Rouen"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_rf0710","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","article-title":"A technique for establishing completeness results in theorem proving with equality","volume":"12","author":"Peterson","year":"1983","journal-title":"SIAM J. Computing"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0715","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reductions for equational theories with complete unification algorithms","volume":"28","author":"Peterson","year":"1981","journal-title":"J. of the ACM"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0720","series-title":"Basic Category Theory for Computer Scientists","author":"Pierce","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0725","series-title":"Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing (STOC'99)","article-title":"Satisfiability of word equations with constants is in NEXPTIME","author":"Plandowski","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0730","series-title":"Proceedings of the Fortieth Annual IEEE Symposium on Foundations of Computer Science (FOCS'99)","article-title":"Satisfiability of word equations with constants is in PSPACE","author":"Plandowski","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0735","first-page":"73","article-title":"Building in equational theories","volume":"7","author":"Plotkin","year":"1972","journal-title":"Machine Intelligence"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0740","series-title":"Proceedings of the 4th International Conference on Rewriting Techniques and Applications","first-page":"162","article-title":"Minimal solutions of linear diophantine equations: Bounds and algorithms","author":"Pottier","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0745","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0750","series-title":"Proceedings of the 2nd International Conference on Rewriting Techniques and Applications","first-page":"216","article-title":"Improving basic narrowing techniques","author":"R\u00e9ty","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0755","series-title":"Proceedings of the Conference on Logic Programming and Automated Reasoning","first-page":"261","article-title":"Unification in a combination of equational theories with shared constants and its application to primal algebras","author":"Ringeissen","year":"1992"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0760","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/321160.321166","article-title":"Theorem proving on the computer","volume":"10","author":"Robinson","year":"1963","journal-title":"J. of the ACM"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50010-2_bb0765","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. of the ACM"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0770","first-page":"63","article-title":"Computational logic: The unification computation","volume":"6","author":"Robinson","year":"1971","journal-title":"Machine Intelligence"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0775","series-title":"Proceedings of the Workshop on Category Theory and Computer Programming","first-page":"493","article-title":"A categorical unification algorithm","author":"Rydeheard","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0780","series-title":"Proceedings of the 9th International Conference on Rewriting Techniques and Applications","first-page":"106","article-title":"E-unification for subsystems of S4","author":"Schmidt","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0785","series-title":"Proceedings of the 8th International Conference on Automated Deduction","first-page":"538","article-title":"Unification in many-sorted equational theories","author":"Schmidt-Schau\u00df","year":"1986"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_bb0790","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/BF02328450","article-title":"Unification under associativity and idempotence is of type nullary","volume":"2","author":"Schmidt-Schau\u00df","year":"1986","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0795","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0024065","article-title":"Computational Aspects of an Order Sorted Logic With Term Declarations","author":"Schmidt-Schau\u00df","year":"1989"},{"issue":"1,2","key":"10.1016\/B978-044450813-3\/50010-2_bb0800","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","article-title":"Unification in a combination of arbitrary disjoint equational theories","volume":"8","author":"Schmidt-Schau\u00df","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0805","article-title":"Some results for unification in distributive equational theories","author":"Schmidt-Schau\u00df","year":"1992","journal-title":"Internal Report 7\/92, Universit\u00e4t Frankfurt, Frankfurt, Germany"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0810","series-title":"Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA-96)","first-page":"287","article-title":"An algorithm for distributive unification","author":"Schmidt-Schau\u00df","year":"1996"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_rf0815","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1006\/jsco.1996.0054","article-title":"Decidability of unification in the theory of one-sided distributivity and a multiplicative unit","volume":"22","author":"Schmidt-Schau\u00df","year":"1996","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0820","series-title":"Proceedings of the 1st International Workshop on Word Equations and Related Topics (IWWERT '90)","first-page":"85","article-title":"Makanin's algorithm for word equations: Two improvements and a generalization","author":"Schulz","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0825","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF00881904","article-title":"Word unification and transformation of generalized equations","volume":"11","author":"Schulz","year":"1993","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0830","series-title":"Proceedings of the 8th International Conference on Rewriting Techniques and Applications","first-page":"284","article-title":"A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms","author":"Schulz","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0835","article-title":"Tractable and intractable instances of combination problems for unification and disunification","author":"Schulz","year":"1999","journal-title":"J. Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0840","series-title":"Proceedings of the International Symposium on Symbolic and Algebraic Manipulation, EUROSAM'79","first-page":"531","article-title":"Unification of commutative terms","author":"Siekmann","year":"1979"},{"issue":"3,4","key":"10.1016\/B978-044450813-3\/50010-2_bb0845","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","article-title":"Unification theory: A survey","volume":"7","author":"Siekmann","year":"1989","journal-title":"J. Symbolic Computation"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50010-2_bb0850","first-page":"402","article-title":"The undecidability of the DA-unification problem","volume":"54","author":"Siekmann","year":"1989","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0855","series-title":"A Proof Theory for General Unification","author":"Snyder","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0860","series-title":"Proceedings of the 12th International Conference on Automated Deduction","first-page":"665","article-title":"A refined version of general E-unification","author":"Socher-Ambrosius","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0865","series-title":"Proceedings of the 4th International Joint Conference on Artificial Intelligence","first-page":"71","article-title":"A complete unification algorithm for associative-commutative functions","author":"Stickel","year":"1975"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50010-2_bb0870","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","article-title":"A unification algorithm for associative commutative functions","volume":"28","author":"Stickel","year":"1981","journal-title":"J. of the ACM"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0875","article-title":"Unifikationstheorie Erster Ordnung","author":"Szab\u00f3","year":"1982","journal-title":"Ph.D. thesis, Universit\u00e4t Karlsruhe"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0880","series-title":"Proceedings of the 8th International Conference on Automated Deduction","first-page":"431","article-title":"Unification in combinations of collapse-free theories with disjoint sets of function symbols","author":"Tid\u00e9n","year":"1986"},{"issue":"1\u20132","key":"10.1016\/B978-044450813-3\/50010-2_bb0885","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S0747-7171(87)80026-3","article-title":"Unification problems with one-sided distributivity","volume":"3","author":"Tid\u00e9n","year":"1987","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0890","article-title":"Automates avec tests d'\u00e9galit\u00e9s entre cousins germains","author":"Tommasi","year":"1991","journal-title":"Master's thesis, Universi\u00e9 de Lille, France"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50010-2_bb0895","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF02575754","article-title":"Complexity of the unification algorithm for first order expressions","volume":"12","author":"Venturini-Zilli","year":"1975","journal-title":"Calcolo"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0900","article-title":"Unification von Morphismen","author":"Vogel","year":"1978","journal-title":"Diploma thesis, Univ. Karlsruhe, Institut f\u00fcr Informatik I, Karlsruhe, Germany"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0905","series-title":"Proceedings of the 8th International Joint Conference on Artificial Intelligence","first-page":"882","article-title":"A many-sorted calculus based on resolution and paramodulation","author":"Walther","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50010-2_bb0910","article-title":"A Many-Sorted Calculus Based on Resolution and Paramodulation","author":"Walther","year":"1987"},{"issue":"2\u20134","key":"10.1016\/B978-044450813-3\/50010-2_bb0915","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BF02127750","article-title":"Unification in sort theories and its applications","volume":"18","author":"Weidenbach","year":"1996","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50010-2_rf0920","series-title":"Automated Deduction \u2014 A Basis for Applications, Vol. I: Foundations \u2014 Calculi and Methods","first-page":"291","article-title":"Sorted unification and tree automata","author":"Weidenbach","year":"1998"},{"issue":"1,2","key":"10.1016\/B978-044450813-3\/50010-2_bb0925","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0747-7171(87)80025-1","article-title":"Unification in combinations of collapse-free regular theories","volume":"3","author":"Yelick","year":"1987","journal-title":"J. Symbolic Computation"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500102?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500102?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,23]],"date-time":"2020-04-23T01:26:07Z","timestamp":1587605167000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":184,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50010-2","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}