Maude es un llenguatge de programacio declaratiu basat en  logica de reescriptura que 
incorpora moltes caracteristiques que ho fan molt potent. No obstant aixo, a l'hora 
de provar certes propietats computacionals este factor  comporta dificultats. 
La tasca de provar la terminacio de sistemes de reescriptura es de fet bastant dura, 
pero aplicada a llenguatges de programacio reals es convert en mes complicada a causa 
de aquestes caracteristiques inherents.
Aço provoca que metodes per a provar la terminacio d'aquest tipus de programes requerisquen 
tecniques especifiques i una analisi exhaustiu. Diversos treballs han intentat provar
 terminacio de (un subconjunt de) programes Maude. No obstant aixo, tots ells segueixen
 una aproximacio transformacional, on el programa original es transformat fins a arribar
 a un sistema de reescriptura capaç de ser empleat amb les tecniques i eines de terminacio 
existents. En la practica, el fet de transformar els sistemes originals sol complicar la
 demostracio de la terminacio ja que açouu  introdueix nous simbols i regles en el sistema. 
En aquesta tesi, abordem el problema de provar terminacio de (un subconjunt de) programes 
Maude mitjançant metodes directes. 

D'una banda, ens centrem en l'estrategia de Maude. Maude es un llenguatge impacient on els 
arguments d'una funcio son avaluats sempre abans de l'aplicacio de la funcio que els usa. 
Aquesta estrategia (coneguda com crida per valor) pot provocar la no terminacio si els 
programes no estan escrits amb cura. Per aquesta rao, Maude (en concret) incorpora mecanismes
 per controlar l'execucio de programes com les anotacions sintactiques que estan associades
 als arguments dels siiooombols. En reescriptura, aquesta estrateigia es coneix com reescriptura
 sensible al context innermost (RSCI). 

D'altra banda, Maude tambe incorpora la possibilitat de declarar atributs. Semanticament, 
declarar un conjunt d'atributs equacionals per a un operador ees equivalent a declarar les 
equacions corresponents per a l'operador pero evita problemes de terminacio i provoca una 
avaluacio mes eficient. Declarar atributs equacionals es correspon amb computar amb classes 
d'equivalencia modul aquestes equacions.  

El marc dels parells de dependencia desenvolupa la idea d'una aplicacio incremental de 
diferents tecniques de terminacio per a resoldre problemes de terminacio. S'ha mostrat 
com una manera potent i eficient de provar terminacio de la reescriptura automaaeticament. 
En aquesta tesi,  abordem la terminacio de la reescriptura sensible al context innermost i de 
la reescriptura modul axiomes especifics estenent el marc dels parells de dependencia.