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

**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^{1} 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 Symposium on Logic in Computer Science (LICS 1988)}, year = {1988}, month = {July}, pages = {121--130}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }