Library of Unification and Anti-Unification Algorithms

---

Software

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

• Unification with sequence variables.
• Context sequence matching.
• Solving unification constraints modulo fuzzy similarity and proximity relations in commutative theories.
• 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.
• Unranked term-graph anti-unification (together with its commutative extension).
• Higher-order anti-unification.
• Solving alpha-equivalence problems (a subalgorithm for the higher-order anti-unification algorithm).
• Nominal anti-unification.
• Solving equivariance problems (a subalgorithm for nominal anti-unification).
• Nominal equational anti-unification.
• Solving equational equivariance problems (a subalgorithm for nominal equational anti-unification).
• Anti-unification in fuzzy quantitative theories.

Team

• Temur Kutsia
• Alexander Baumgartner
• David Cerna

---

Supported by the Austrian Science Fund (FWF), projects P 24087, P 28789, and P 35530.

---