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. A new definition for R, A-rewriting that allows us to solve a bigger class of reachability problems, and a calculus that solves this class of problems always working with canonical terms and normalized 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 a more general one that can be instantiated to that answer.