Ternary Boolean algebra unification

In order to unify terms in a ternary Boolean algebra (TBA), the authors exploit the properties of complete commutativity and pseudoassociativity and develop an E-unification algorithm for the equational theory E consisting of the axioms which define these two properties. The algorithm is for the most part a modification of J. Siekmann´s (1979) C-unification algorithm, which is itself an extension of J. Robinson´s (1965) unification algorithm for first-order terms. However, in the case of TBA terms, it is necessary to account for the possible rearrangement of subterms due to the effect of the pseudoassociative law. The algorithm for finding such rearrangements is based on both the pseudoassociative law and complete commutativity