Paper: Computing Unification Algorithms (at LICS 1986)

Authors: 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}
  }