Folding variant narrowing and optimal variant termination

Automated reasoning modulo an equational theory E is a fundamental technique in many applications. If E can be split as a disjoint union E∪Ax in such a way that E is confluent, terminating, sort-decreasing, and coherent modulo a set of equational axioms Ax, narrowing with E modulo Ax provides a complete E-unification algorithm. However, except for the hopelessly inefficient case of full narrowing, little seems to be known about effective narrowing strategies in the general modulo case beyond the quite depressing observation that basic narrowing is incomplete modulo AC. Narrowing with equations E modulo axioms Ax can be turned into a practical automated reasoning technique by systematically exploiting the notion of E,Ax-variants of a term. After reviewing such a notion, originally proposed by Comon-Lundh and Delaune, and giving various necessary and/or sufficient conditions for it, we explain how narrowing strategies can be used to obtain narrowing algorithms modulo axioms that are: (i) variant-complete (generate a complete set of variants for any input term), (ii) minimal (such a set does not have redundant variants), and (iii) are optimally variant-terminating (the strategy will terminate for an input term t iff t has a finite complete set of variants). We define a strategy called folding variant narrowing that satisfies above properties (i)-(iii); in particular, when E∪Ax has the finite variant property, that is, when any term t has a finite complete set of variants, this strategy terminates on any input term and provides a finitary E∪Ax-unification algorithm. We also explain how folding variant narrowing has a number of interesting applications in areas such as unification theory, cryptographic protocol verification, and proofs of termination, confluence and coherence of a set of rewrite rules R modulo an equational theory E.