Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude.

This work studies the relationship between verifiable and computable answers for reachability problems in rewrite theories with an underlying membership equational logic. These problems have the form $$\begin{aligned} (\exists \bar{x})t(\bar{x})\rightarrow ^* t'(\bar{x}) \end{aligned}$$ with \(\bar{x}\) some variables, or a conjunction of several of these subgoals. A calculus that solves this kind of problems working always with normalized terms and substitutions has been developed. Given a reachability problem in a rewrite theory, this calculus can compute any normalized answer that can be checked by rewriting, or one that can be instantiated to that answer. Special care has been taken in the calculus to keep membership information attached to each term, to make use of it whenever possible.