Normalização Forte Via Ordinal Natural

O método do ordinal natural para obtenção de normalização forte em sistemas de redução corresponde à definição de uma atribuição numérica a termos de um sistema que satisfaça as seguintes propriedades: o número associado a cada termo do sistema é finito (um número natural) e se um termo t se reduz a um termo t' é estritamente menor que o número associado a t (a atribuição numérica diminui com as reduções)...O objetivo principal desta tese é introduzir um método de obtenção de normalização forte via ordinal natural aplicável a sistemas de dedução natural e cálculo lambda tipificado, no qual a atribuição numérica utilizada, por coincidir com o comprimento de uma seqüência de redução específica, representa o menor limitante superior para o comprimento das seqüências de redução dos termos dos sistemas. Juntamente, fazemos um estudo de alguns artigos que também obtêm normalização forte via ordinal natural e os comparamos com o nosso método.