Maude es un lenguaje de programacion declarativo basado en la logica de reescritura que incorpora 
muchas caracteristicas que lo hacen muy potente. Sin embargo, a la hora de probar ciertas propiedades 
computacionales esto conlleva dificultades. La tarea de probar la  terminacion de sistemas de reesctritura 
es de hecho bastante dura, pero aplicada a lenguajes de programacion reales se concierte en mas 
complicada debido a estas caracteristicas inherentes. Esto provoca que metodos para probar 
la terminacion de este tipo de programas requieran  tecnicas especificas y un analisis cuidadoso. 
Varios trabajos han intentado probar terminacion de  (un subconjunto de) programas Maude. 
Sin embargo, todos ellos siguen una aproximación transformacional, donde el programa original 
es trasformado hasta alcanzar un sistema de reescritura capaz de ser manejado con las tecnicas 
y herramientas de terminacion existentes. En la practica, el hecho de transformar los sistemas 
originales suele complicar la demostracion de la terminacion ya que esto introduce nuevos simbolos
 y reglas en el sistema. En esta tesis, llevamos a cabo el problema de probar terminacion de 
(un subconjunto de) programas Maude mediante metodos directos.

Por un lado, nos centramos en la estrategia de Maude. Maude es un lenguaje impaciente donde 
los argumentos de una funcion son evaluados siempre antes de la aplicacion de la funcion que los usa.
 Esta  estrategia (conocida como llamada por valor) puede provocar la no terminacion si los 
programas no estan escritos cuidadosamente.
Por esta razon,  Maude (en concreto) incorpora mecanismos para controlar la ejecucion de 
programas como las anotaciones sintacticas que estan asociadas a los argumentos de los simbolos. 
En reescritura, esta estrategia es conocida como reescritura sensible al contexto innermost (RSCI).

Por otro lado, Maude tambien incorpora la posibilidad de declarar atributos. 
Semanticamente, declarar un conjunto de atributos ecuacionales para un operador es equivalente 
a declarar las ecuaciones correspondientes para el operador pero evita problemas de terminacion 
y provoca una evaluacion mas eficiente. Declarar atributos ecuacionales se corresponde con 
computar con clases de equivalencia modulo esas ecuaciones.

El marco de los pares de dependencia desarrolla la idea de una aplicacion incremental  
de diferentes tecnicas  de terminacion para  resolver problemas de terminacion. 
Se ha mostrado como una manera potente y eficiente de probar  terminacion de la 
reescritura automaticamente. En esta tesis, abordamos la terminacion de la reescritura 
sensible al contexto innermost y de la reescritura modulo axiomas especificos extendiendo 
el marco de los pares de dependencia.