Title :
Ternary Boolean algebra unification
Author :
Wilkerson, Ralph ; Murphy, Dan ; Jenness, Jeff ; Pinet, Bill ; Brazeal, Dwayne
Author_Institution :
Dept. of Comput. Sci., Missouri Univ., Rolla, MO, USA
Abstract :
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
Keywords :
Boolean algebra; formal logic; C-unification algorithm; E-unification algorithm; TBA terms; axioms; complete commutativity; equational theory E; first-order terms; pseudoassociative law; pseudoassociativity; subterms; ternary Boolean algebra unification; Boolean algebra; Computer science; Equations; Expert systems; Hardware; Logic programming;
Conference_Titel :
Applied Computing, 1990., Proceedings of the 1990 Symposium on
Conference_Location :
Fayetteville, AR
Print_ISBN :
0-8186-2031-5
DOI :
10.1109/SOAC.1990.82151
