ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

First Annual IEEE Symposium on

Logic in Computer Science (LICS 1986)

Paper: Computing Unification Algorithms (at LICS 1986)

Authors: Claude Kirchner


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.


    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}

Last modified: 2022-10-3113:49
Sam Staton