Skip to content
Unification and Anti-Unification Algorithm Library
Software URLGo to WebsiteThis 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).