Title :
Unification in free extensions of Boolean rings and Abelian groups
Author :
Boudet, Alexandre ; Jouannaud, Jean-Pierre ; Schmidt-Schauß, Manfred
Author_Institution :
Univ. de Paris-Sud, Osray, France
Abstract :
A complete unification algorithm is presented for the combination of two arbitrary equational theories E in T(F,X) and E/sup 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.<>
Keywords :
Boolean functions; Abelian groups; Boolean rings; arbitrary equational theories; free extensions; infinite trees; unification; Algebra; Artificial intelligence; Computer science; Equations; Logic programming; Transforms; Very large scale integration;
Conference_Titel :
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location :
Edinburgh, UK
Print_ISBN :
0-8186-0853-6
DOI :
10.1109/LICS.1988.5110
