Lógicas Clássicas
Resolução
O ALGORITMO DE UNIFICAÇÃO - UNIFICA (L1, L2)
1. Se L1 ou L2 for um átomo, então faça o seguinte:
1.1. Se L1 e L2 forem idênticos, retornar NIL
1.2. Caso contrário, se L1 for uma variável, faça
1.2.1. Se L1 ocorrer em L2, retornar F;
1.2.2. Caso contrário, retornar (L2/L1)
1.3. Doutro modo, se L2 for uma variável, faça
1.3.1. Se L2 ocorrer em L1, retornar F;
1.2.2. Caso contrário, retornar (L1/L2)
1.4. Caso contrário, retornar F.
2. Se comprimento(L1) não for igual a comprimento(L2) retornar F.
3. Designar a SUBST o valor NIL. (ao final do procedimento, SUBST conterá todas as substituições utilizadas para unificar L1 e L2).