## Paper: Computing Unification Algorithms (at LICS 1986)

**Claude Kirchner**

### Abstract

A framework allowing the study of equational unification and
the design of unification procedures is sketched. For a wide class of theories,
it gives a procedure which yields, whenever it terminates, a complete set of
unifiers for any equation, provided that the mutation transformation, depending
on the theory, is known. We show that the set of axioms defining the theory can
be completed by computing critical pairs, in such a way that the mutation is
syntactically deduced from the axioms form. We apply this result to solve an
open unification problem: unification modulo the axiom
*(xRy)*(yRz)=(xRy)*(xRz)* where *R* may be commutative.

### BibTeX

@InProceedings{Kirchner-ComputingUnificatio, author = {Claude Kirchner}, title = {Computing Unification Algorithms}, booktitle = {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)}, year = {1986}, month = {June}, pages = {206--216 }, location = {Cambridge, MA, USA}, publisher = {IEEE Computer Society Press} }