Desunificação Nominal via Ponto Fixo - Batista, Leonardo; Nantes-Sobrinho, Daniele (Anais do Workshop Brasileiro de Lógica (WBL); 2021: Anais do II Workshop Brasileiro de LógicaDO - 10.5753/wbl.2021.15773, 2021)
Este é um trabalho em andamento sobre a resolução de equações e diferenças entre termos nominais, chamado de problema de desunificação nominal. Ao invés de usarmos as técnicas nominais padrões que envolvem restrições de freshness (i.e., expressões da forma a#t que significa "o átomo a não ocorre livre em t'') para implementar alpha-equivalência, seguiremos uma abordagem alternativa que envolve equações de ponto fixo, i.e., equações da forma pi.t=_α t, onde t é um termo nominal e pi uma permutação. Essa abordagem será conveniente a futuras extensões do problema envolvendo teorias equacionais.