Definição – O que significa Unificação?
Em ciência da computação e lógica, a unificação é o procedimento algorítmico usado na resolução de equações que envolvem expressões simbólicas. Em outras palavras, ao substituir certas variáveis de subexpressão por outras expressões, a unificação tenta identificar duas expressões simbólicas. A unificação é usada na tecnologia de raciocínio automatizado, que continua sendo uma das principais áreas de aplicação da unificação.
A unificação é usada em implementações como:
- Implementação de sistema de tipo de linguagem de programação
- Programação lógica
- Solucionadores SMT
- Análise de protocolo criptográfico
- Algoritmos de reescrita de termos
A unificação é uma das técnicas fundamentais nas quais se baseiam os métodos de dedução automatizada.
Definirtec explica a unificação
O termo “unificação” e sua noção podem ser atribuídos a John Alan Robinson. Ele usou a unificação como a operação básica de seu princípio de resolução e também mostrou que os termos unificáveis têm no máximo um unificador geral. Vários frameworks de unificação são diferenciados com base nas expressões que ocorrem no problema de unificação. A unificação de primeira ordem é aquela em que variáveis de ordem superior (variáveis que representam funções) são permitidas nas expressões. Unificação livre ou unificação sintática é aquela em que uma solução é necessária para tornar iguais os dois lados da equação.
A solução de um problema de unificação é representada por substituição, que é o mapeamento de um valor simbólico para cada variável envolvida nas expressões do problema. Em outras palavras, o foco essencial da unificação é procurar uma substituição para unificar dois termos dados. Espera-se que o algoritmo uniforme superior forneça um conjunto de substituição mínimo e completo (um conjunto com todas as soluções relevantes sem membros redundantes) para um determinado problema. Em outras palavras, a unificação não está apenas interessada na capacidade de resolução de um determinado problema de unificação, mas também, se solucionável, em computar o unificador mais geral.
A unificação é considerada o núcleo de:
- Implementações de Prolog
- Sistemas especialistas baseados em inteligência artificial
- Correspondência de padrões em linguagens funcionais
- Certas abordagens de análise
- Bancos de dados dedutivos
- Processamento de linguagem natural
- Provadores de teorema
- Algoritmos de inferência de tipo