  Concurrent functional languages that are endowed with symbolic reasoning
capabilities such as Maude offer a high-level, elegant, and efficient approach
to programming and analyzing complex, highly nondeterministic software systems.
Maude's symbolic capabilities are based on equational unification and narrowing
in rewrite theories, and provide Maude with advanced logic programming
capabilities such as unification modulo user-definable equational theories and
symbolic reachability analysis in rewrite theories. Intricate computing
problems may be effectively and naturally solved in Maude thanks to the synergy
of these recently developed symbolic capabilities and classical Maude features,
such as: (i) rich type structures with sorts (types), subsorts, and
overloading; (ii) equational rewriting modulo various combinations of axioms
such as associativity, commutativity, and identity; and (iii) classical
reachability analysis in rewrite theories. However, the combination of all of
these features may hinder the understanding of Maude symbolic computations for
non-experienced developers. The purpose of this article is to describe how
programming and analysis of Maude rewrite theories can be made easier by
providing a sophisticated graphical tool called Narval that supports the
fine-grained inspection of Maude symbolic computations. This paper is under
consideration for acceptance in TPLP.
