Dada uma teoria equacional T, isto é, um conjunto T de equações, uma pergunta que se faz é se os teoremas da teoria T podem, ou não, serem verificados através de um algoritmo que termina.Uma abordagem à esta questão, muito divulgada a partir da final da década de sessenta com o trabalho de Knut and Bendix, baseia-se na busca de sistemas de reescrita de termos completos para a teoria T dada, isto é, sistemas de reescrita completos que induzam as mesmas classes de congruência da teoria T. Muitos têm sido os esforços nas últimas décadas para o desenvolvimento de técnicas de completação de sistemas de reescrita com o intuito de conseguir-se obter sistemas completos para uma variedade cada vez maior de teorias equacionais. Neste trabalho, estudamos os aspectos básicos de teorias equacionais, incluindo seus sub-problemas como a unificação de termos e a terminação de sistemas de reescrita. Descrevemos dois algoritmos de completação de sistemas de reescrita, o algoritmo clássico de Knut and Bendix e o algoritmo de completação módulo teorial equacional, de Peterson and Stickel,generalizando o anterior. Por fim, apresentamos uma aplicação do uso de sistemas de reescrita para a Morfologia Matemática, uma área da computação com aplicações diretas no campo de processamento de imagens. Tanto a verificação da identidade entre operadores morfológicos quanto a simplificação de tais operadores são problemas de interesse no campo da morfologia matemática. Apresentamos, para a sub-classe dos operadores morfológicos invariantes por translação e isotônicos para imagens binárias, um método efetivo para a verificação de identidade entre tais operadores morfológicos, que se materializa na existência de um sistema de reescrita completo para a teoria dos reticulados distributivos. Discutimos, por fim, a aplicabilidade dessa abordagem para a simplificação de operadores morfológicos, tanto para o caso de implementações desses operadores em máquinas seqüenciais quanto em máquinas paralelas

Given an equational theory T, that is, a set T of equations, an important question that can be posed concerns the existence of an algorithm that has the termination property, and which could be used to deduce all theorems of T. An approach to that question, well known since the late sixties after a paper by Knuth and Bendix, is based on the search for complete term rewriting systems with respect to the given equation theory T, that is, complete rewriting systems which induce the same congruence classes of theory T. Much effort has been put on the last few decades to develop new techniques to generate complete term rewriting systems to a diversity of equational theories. In this text we study the basic aspects of equational theories, including the problems of term unification and termination. We describe two algorithms for completion of term rewriting systems: the first is the classic one, due to Knuth and Bendix, and the second one is an algorithm for completion modulo equational theories, due to Peterson and Stickel, which generalizes the first one. We also show an application of term rewriting systems to Mathematical Morphology, a research area of computer science with a variety of applications to image processing. The verification of identity between morphological operators and the simplification of these operators are problems of interest to Mathematical Morphology. We present, for the subclass of morphological operators that are isotonic and translation-invariant, an effective method to check the identity between such morphological operators, based on the existence of complete term rewriting system for distributive lattices. Finally, we discuss the applicability of our approach with respect to the simplification of morphological operators, when these operators are implemented in sequential machines as well as in parallel machines