  This paper introduces GLINTS, a graphical tool for exploring variant
narrowing computations in Maude. The most recent version of Maude, version
2.7.1, provides quite sophisticated unification features, including
order-sorted equational unification for convergent theories modulo axioms such
as associativity, commutativity, and identity (ACU). This novel equational
unification relies on built-in generation of the set of 'variants' of a term
$t$, i.e., the canonical form of $t \sigma$ for a computed substitution
$\sigma$. Variant generation relies on a novel narrowing strategy called
'folding variant narrowing' that opens up new applications in formal reasoning,
theorem proving, testing, protocol analysis, and model checking, especially
when the theory satisfies the 'finite variant property', i.e., there is a
finite number of most general variants for every term in the theory. However,
variant narrowing computations can be extremely involved and are simply
presented in text format by Maude, often being too heavy to be debugged or even
understood. The GLINTS system provides support for (i) determining whether a
given theory satisfies the finite variant property, (ii) thoroughly exploring
variant narrowing computations, (iii) automatic checking of node 'embedding'
and 'closedness' modulo axioms, and (iv) querying and inspecting selected parts
of the variant trees. This paper is under consideration for acceptance in TPLP.
