Um estudo em unificação e desunificação módulo

Abstract

Estuda-se a comparação entre unificação assimétrica e desunificação módulo teorias equa- cionais em relação às suas complexidades, como desenvolvida por Ravishankar, Narendran e Gero. A unificação assimétrica é um tipo de unificação equacional em que as soluções devem fornecer o lado direito dos problemas apresentados na forma normal. E a desunifi- cação é resolver problemas com equações e “disequações” em relação à uma teoria equaci- onal dada. As soluções para os problemas de desunificação são substituições que tornam os dois termos de cada equação iguais, mas os dois termos de cada “disequação” diferen- tes. Unificação e desunificação equacional foram comparadas por os autores mencionados com relação as suas complexidades de tempo para duas teorias equacionais: a primeira associativa (A), comutativa (C), com unidade (U) e nilpotente (N), como (ACUN) e a segunda com tais propriedades, mas adicionando um homomorfismo (h), como (ACUNh), mostrando que desunificação pode ser resolvida em tempo polinomial enquanto unificação assimétrica é NP-difícil para ambas as teorias equacionais. Além disso, foi estudada a abordagem introduzidas por Zhiqiang Liu, em sua dissertação de doutorado, para converter osunificadores módulo ACUN em assimétricos, com símbolos de função não interpretados, usando as regras de inferência. Para a teoria associativa comutativa com homomorfismo (ACh), estudou-se a prova de que unificação módulo ACh é indecidível, assim como o algoritmo de semi-decisão, recentemente introduzido por Ajay Kumar Eeralla e Christopher Lynch, que apresenta um conjunto de regras de inferência para resolver o problema com limitações.