Logic in Computer Science (LICS 1988)

Paper: Unification in free extensions of Boolean rings and Abelian groups (at LICS 1988)

Authors: Alexandre Boudet Jean-Pierre Jouannaud Manfred Schmidt-Schauß

Abstract

A complete unification algorithm is presented for the combination of two arbitrary equational theories E in T(F,X) and E¹ in T (F',X), where F and F' denote two disjoint sets of function symbols. The method adapts to unification of infinite trees. It is applied to two well-known open problems, when E is the theory of Boolean rings or the theory of Abelian groups, and E is the free theory. The interest to Boolean rings originates in VSLI verification

BibTeX

  @InProceedings{BoudetJouannaudSchm-Unificationinfreeex,
    author = 	 {Alexandre Boudet and Jean-Pierre Jouannaud and Manfred Schmidt-Schauß},
    title = 	 {Unification in free extensions of Boolean rings and Abelian groups },
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {121--130},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }