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 E1 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} }