Anti-unification in Absorptive Theories
Anti-unificação, Generalização, Teoria Equacional, Dedução
Equacional, Teoria Absortiva.
O interesse em antiunificação, problema dual da unificação, está
aumentando devido a diversas novas aplicações. Por exemplo, técnicas baseadas em
antiunificação têm sido recentemente empregadas em análise de software e áreas relacionadas,
como detecção de clones e reparo automático de programas. Embora formas sintáticas de
antiunificação tenham encontrado muitos usos interessantes, alguns aspectos das aplicações
modernas são modelados de forma mais apropriada pelo raciocínio módulo uma teoria
equacional. Assim, estender os métodos de antiunificação existentes para lidar com teorias
equacionais importantes é um avanço natural. Este trabalho considera antiunificação módulo
teorias absortivas puras, ou seja, onde alguns símbolos de função são associados a uma constante
especial que satisfaz o axioma f(x, e) = f(e, x) = e. Fornecemos um algoritmo baseado em regras
para antiunificação em tais teorias, provamos sua correção e estudamos sua completude. Além
disso, provamos que o tipo do problema de antiunificação módulo teorias absortivas é infinitário e
estudamos a combinação de teorias absortivas com operadores comutativos.