Automated reasoning modulo an equational theory $\caE$ is a
fundamental technique in many applications.  If $\caE$ can be split as
a disjoint union $E\!\cup \!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
$\caE$-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 \emph{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$-\emph{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)
\emph{variant-complete} (generate a complete set of variants for any
input term), (ii) \emph{minimal} (such a set does not have redundant
variants), and (iii) are \emph{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 \emph{folding
  variant narrowing} that satisfies above properties (i)--(iii); in
particular, when $E \cup Ax$ has the \emph{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 \emph{finitary}
$E \cup 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$.


Keywords: 
-Narrowing modulo 
-Terminating Narrowing Strategy
-Variants
-Equational Unification