Unification and Anti-Unification Algorithm Library

Authors

Software URL

Go to Website
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).