AC Unification in hol90
We report on an implementation of associative-commutative unification in
an LCF-style theorem prover. We show how this algorithm can be used to
implement rewriting modulo associativity and commutativity. This is an
example of the sound incorporation of automatic first order methods into
an interactive higher-order logic theorem prover.