Unificação assimétrica módulo operadores nilpotentes com homomorfismo

Abstract

Esta dissertação tem como foco o estudo do problema de unificação módulo uma teoria equacional cuja assinatura contém um operador binário que satisfaz as identidades Associatividade, Comutatividade, Unidade e Nilpotência (ACUN), e que pode ou não conter um operador unário que satisfaz a identidade de homomorfismo (ACUNh), que é a teoria equacional do operador , amplamente utilizado em diversas ferramentas criptográficas, como MAUDE-NPA[10] que utiliza uma encriptação de grupos abelianos, incluindo ( ou exclusivo ), exponenciação e encriptação homomórfica. Primeiro apresentaremos alguns critérios para existência de soluções para problemas de ACUN(h)-unificação elementar com constantes que consiste em associar o problema de unificação à um sistema de equações lineares cujos coeficientes são elementos de ou , dependendo se o homomorfismo é ou não considerado. Segundo, apresentaremos um algoritmo para resolver problemas de ACUN(h)- unificação geral que retorna sempre um conjunto completo de unificadores. Finalmente, apresentaremos o estudo de um novo paradigma de unificação, a dizer, \emph{unificação assimétrica}, que consiste de obter unificadores de um problema de unificação com a propriedade de preservar formas normais do lado direito de cada equação de com relação a um sistema de reescrita convergente e coerente módulo uma teoria equacional . No caso particular da teoria equacional ACUN construiremos um algoritmo de conversão de ACUN-unificadores para ACUN-unificadores assimétricos.