Julia Sapiña

Variant-based Equational Unification under Constructor Symbols

2020 · Electronic Proceedings in Theoretical Computer Science

Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. A narrowing-based equational unification algorithm relying on the concept of the variants …