LATPub37

{{Publikation Details |Abstract=This work investigates general AC-unification, i.e. unification in the combination of free function symbols and free Abelian semigroups, whose function symbols fulfill associativity and commutativity. The three necessary parts of general AC-unification are presented: a combination algorithm, a procedure for elementary AC-unification, and methods for solving systems of diophantine equations. Starting with A. Boudet's unification algorithm for the combination of regular and collapse-free theories, an efficient algorithm for general AC-unification is developed, setting out conditions that must be fulfilled by the solutions of elementary AC-unification. These conditions are used by the procedure for elementary AC-unification whereby further conditions are set out that must be fulfilled by the solutions of the diophantine equations. Then three methods (those of E. Contejean and H. Devie, E. Domenjoud, L. Pottier) for solving systems of diophantine equations are presented. The three methods are compared and evaluated, trying to use the conditions efficiently. Finally some problems which arise from the reuse of AC-unifiers in unification, such as merging, are presented. It is shown that reusing AC-unifiers for partial problems is often worse than solving the entire problem from the beginning. |ISBN= |ISSN= |Link= |Download=SEKI-SWP-92-12.ps.gz |Slides= |DOI Name= |Projekt= |Forschungsgruppe=Automatentheorie |BibTex=@techreport{ SWP-92-12,

 address = {Postfach 3049, D--67663 Kaiserslautern, Germany},
 author = {J{\"o}rn {Richts} },
 institution = {Fachbereich Informatik, Universit{\"a}t Kaiserslautern},
 number = {SWP--92--12},
 title = {Allgemeine {$AC$}-{U}nifikation durch {V}ariablenabstraktion mit {F}remdtermbedingungen},
 type = {Seki Working Paper},
 year = {1992},

} }}