En 1936 Alan Turing va demostrar que el "halting problem", 
és a dir, el problema de decidir si un programa acaba o no,
és un problema indecidible per a la immensa majoria dels llenguatges de programació.
Tot i això, la terminació és un problema tan rellevant que 
en les últimes dècades s'ha desenvolupat
una gran nombre de técniques per a demostrar
la terminació de la màxima quantitat de programes possible de manera automàtica. 
Els sistemes de reescriptura  de termes proporcionen un marc teòric
abstracte perfecte per a la caracterizació de les propietats de terminació
de programes. En aquest marc, l'avaluació d'un terme consisteix en l'aplicació
no determinista d'un conjunt de regles de reescriptura.

L'estretiment "narrowing" de termes és una generalització de la reescriptura que 
 proporciona un mecanisme de raonament automàtic. Per exemple,
donat un conjunt de regles que definisquen la suma i la multiplicació dels naturals,
la reescriptura permet calcular expressions aritmètiques,
mentre que l'estretiment permet "resoldre" equacions amb variables.
%Las aplicaciones de este mecanismo son innumerables.
Aquesta tesi constitueix el primer estudi en profunditat de les propietats de terminació
de l'estretiment. Les contribucions són les següents.

En primer lloc, s'identifiquen classes de sistemes en què l'estretiment té
un comportament bo, en el sentit que sempre acaba. Molts mètodes
de raonament automàtic, como l'anàlisi de les propietats de programes basat en
una semàntica computada per mitjà de narrowing, es beneficien d'aquesta caracterització.

En segon lloc, s'introdueix un mètode automàtic, basat en el marc teòric de 
parells de dependència, per a demostrar la terminació de l'estretiment en un sistema particular. El nostre mètode es, por primera volta, aplicable a qualsevol classe de sistemes. 

En tercer lloc, es proposa un nou mètode per l'estudi de la terminació de l'estretiment
des d'un terme particular, cosa que permet  l'anàlisi de la terminació
de programes.
El nostre mètode generalitza els mètodes existents de manera fonamental.
Gràcies a això, es pot estudiar la terminació de llenguatges de programació
lògics a través de la terminació de l'estretiment,
un fet que fins ara no era possible amb els mètodes que hi havia.

En quart lloc, s'analitza detalladament la modularitat de la terminació de l'estretiment. Això és, si els sistemes A i B són terminants, en què casos el sistema unió és terminant. La modularitat té implicacions directes en moltes de les aplicacions de l'estretiment. En concret, desenvolupem el cas de la resolució de equacions simbòliques quan es combinen diversos  sistemes equacionals.

A més, les tècniques automàtiques de la segona i tercera contribució han sigut implementades en la nostra eina de demostració de la terminació de l'estretiment, Narradar.