Conditional narrowing modulo in Rewriting Logic and Maude

Abstract

Este trabajo presenta un estudio sobre la resolución de problemas de alcanzabilidad en teorías de reescritura con una lógica ecuacional de pertenencia subyacente, usando la técnica de estrechamiento. Para ello se han desarrollado dos cálculos, uno que resuelve el problema de unificación módulo la lógica ecuacional y otro que resuelve el problema de alcanzabilidad basándose en el cálculo de unificación previo. Dichos cálculos hacen uso de algoritmos de pertenencia, de unificación módulo axiomas y de encaje, todos ellos disponibles en el lenguaje de reescritura Maude. En ambos cálculos se hace especial énfasis en el uso eficiente de la información sobre los tipos de los términos. Se ha demostrado la corrección y completitud de los cálculos. Posteriormente se han desarrollado sendos conjuntos de reglas de transformación para estos cálculos que permiten la implementación de los mismos.Finalmente, se han programado estas reglas en un prototipo, usando el lenguaje de reescritura Maude. [ABSTRACT] This master's thesis presents a study about reachability problem solving in rewrite theories with an underlying membership equational logic, using the narrowing technique. To achieve this two calculi have been developed , one that solves the unication modulo equational logic problem and another one that solves the reachability problem based on the former unication calculus. Both calculi make use of membership, unication modulo axioms and matching algorithms, all of them available in the rewriting language Maude. Special emphasis has been made on both calculi in the efficient use of term typing information. Soundness and completeness of both calculi has been proved. Afterwards, two sets of transformation rules have been developed to allow the implementation of both calculi. Finally, those rules have been programmed on a prototype, using the rewriting language Maude.