Unification and Anti-Unification Algorithm Library

This library contains unification, matching, and anti-unification algorithms in various theories developed at RISC.

Unification with sequence variables.
Context sequence matching.
Rigid anti-unification for unranked terms and hedges and its experimental extension with commutative symbols.
Unranked second-order anti-unification and its experimental extension with commutative symbols.
Higher-order anti-unification.
- Deciding alpha-equivalence (a subalgorithm for the higher-order anti-unification algorithm).
Nominal anti-unification
- Deciding equivariance (a subalgorithm for nominal anti-unification).
Term-graph anti-unification (together with the commutative extension).