Syntactic, commutative and associative anti-unification

Abstract

Esta dissertação apresenta um estudo detalhado do Problema de Anti-Unificação, investigado originalmente por Plotkin, Popplestone e Reynolds no início dos anos 70. Este problema consiste em encontrar um termo que mantém a maior estrutura comum entre dois outros termos dados. Isto é, dados s e t, o problema consiste em encontrar um terceiro termo r, que tem uma noção de maximalidade, tal que existam σ1 e σ2 tais que rσ1 = s e rσ2 = t. Tal termo r é chamado de generalizador menos geral de s e t. Neste trabalho investigaremos o Problema de Anti-Unificação Sintático, isto é, quando consideramos a igualdade sintática entre os termos; e também dos Problemas de AntiUnificação módulo Comutatividade (C) e Associatividade (A), isto é, quando o problema de anti-unificação considera as igualdades módulo C e módulo A, respectivamente. Em todos os casos, apresentamos um algoritmo para resolução do problema além de suas propriedades de terminação, correção e completude. A partir das propriedades de cada algoritmo, apresentaremos então as propriedades dos conjuntos de soluções de cada problema.