Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude

This work studies the relationship between veriable and computable answers for reachability problems in rewrite theories with an underlying membership equational logic. These problems have the form (∃¯x)t(¯x) →∗ t (¯x) with ¯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.

• Type: Journal
• Year: 2015
• Where: BIRTHDAY
• Authors: Luis Aguirre, Narciso Martí-Oliet, Miguel Palomino, Isabel Pita
• Keywords: Applied Computing, BIRTHDAY 2015