Variant-Based Equational Anti-unification

The dual of most general equational unifiers is that of least general equational anti-unifiers, i.e., most specific anti-instances modulo equations. This work aims to provide a general mechanism for equational anti-unification that leverages the recent advances in variant-based symbolic computation in Maude. Symbolic computation in Maude equational theories is based on folding variant narrowing (FVN), a narrowing strategy that efficiently computes the equational variants of a term (i.e., the irreducible forms of all of its substitution instances). By relying on FVN, we provide an equational anti-unification algorithm that computes the least general anti-unifiers of a term in any equational theory E where the number of least general E-variants is finite for any given term.