Unificação

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