A Unification Algorithm for the General Unification Problem in the ACUN Theory
LI Zhou-jun · Computer Engineering and Science · 2006
The algebraic properties of the operator exclusive-or are characterized by the ACUN theory. Based on the optimized decomposition algorithm for the unification problem of the union of disjoint equational theories and the Gaussian elimination method,we present a unification algorithm for the general unification problem of the ACUN theory.