En 1936 Alan Turing demostró que el "halting problem", esto es, el problema de decidir si un programa termina o no, es un problema indecidible para la inmensa mayoría de los lenguajes de programación. A pesar de ello, la terminación es un problema tan relevante que en las últimas décadas un gran numero de técnicas han sido desarrolladas para demostrar la terminación de forma automática de la máxima cantidad posible de programas. Los sistemas de reescritura de términos proporcionan un marco teórico abstracto perfecto para el estudio de la terminación de programas. En este marco, la evaluación de un termino consiste en la aplicación no determinista de un conjunto de reglas de reescritura. El estrechamiento (narrowing) de términos es una generalización de la reescritura que proporciona un mecanismo de razonamiento automático. Por ejemplo, dado un conjunto de reglas que definan la suma y la multiplicación, la reescritura permite calcular expresiones aritméticas, mientras que el estrechamiento permite resolver ecuaciones con variables. Las aplicaciones de este mecanismo son innumerables. Esta tesis constituye el primer estudio en profundidad de las propiedades de terminación del estrechamiento. Las contribuciones son las siguientes. En primer lugar, se identifican clases de sistemas en las que el estrechamiento tiene un comportamiento bueno, en el sentido de que siempre termina. Muchos métodos de razonamiento automático, como el análisis de la semántica de lenguajes de programación mediante operadores de punto fijo, se benefician de esta caracterización. En segundo lugar, se introduce un método automático, basado en el marco teórico de pares de dependencia, para demostrar la terminación del estrechamiento en un sistema particular. Nuestro método es, por primera vez, aplicable a cualquier clase de sistemas. En tercer lugar, se propone un nuevo método para estudiar la terminación del estrechamiento desde un termino particular, permitiendo el análisis de la terminación de lenguajes de programación. El nuevo método generaliza los métodos existentes de manera fundamental, gracias a lo cual se puede estudiar la terminación de lenguajes de programación lógicos a través de la terminación del estrechamiento, algo que hasta ahora no era posible con los métodos existentes. En cuarto lugar, se analiza detalladamente la modularidad de la terminación del estrechamiento. Esto es, si los sistemas A y B son terminantes, en que casos el sistema unión es terminante. La modularidad tiene implicaciones directas en muchas de las aplicaciones del estrechamiento. En concreto desarrollamos el caso de la resolución de ecuaciones simbólicas cuando se combinan varios sistemas ecuacionales. Ademas, las técnicas automáticas de la segunda y tercera contribución han sido implementadas en nuestra herramienta de demostración de la terminación del estrechamiento, Narradar.