Unificação para fol

[paulodt]

Creio que agora o código está mais organizado. Me baseei no "Designing a Theorem Prover", sugerido pelo senhor. Meu objetivo não foi reproduzir a fórmula, feita em ML, no Lisp, e sim criar novamente a função unify. Essa função recebe dois termos e a lista de atribuições das variáveis, em uma estrutura do tipo alist, e retorna tal lista atualizada.

[arademaker]

(unify (and ?a ?b) (and x y) nil) não funcionou. Não tem testes para termos certeza que está funcionando.

Em unify-var, veja que com comentários antes das clausulas do cond fica mais claro.

(defun unify-var (a b env)
  (let ((ca (chasevar a env)) (cb (chasevar b env)))
    (cond
      ;; caso já unificado
      ((or (equal a b) (equal ca cb)) env)
      ;; quando não há nenhuma atribuição de "a" no env, mas há atribuição de "b"
      ((and (equal a ca) (not (equal b cb)))
       (push `(,a . ,b) env))
      ;; aqui o mesmo caso, agora com "b" e "a", respectivamente
      ((and (equal b cb) (not (equal a ca))) 
       (push `(,b . ,a) env))
      ;; caso em que não há possibilidade de unificação
      (t nil))))

Em unify, vários comentários online fora do lugar, excesso de uso de cond quando if poderia funcionar pois são apenas 2 casos. sugiro antes da funcao colocar um paragrafo na forma de comentario explicando a idéia. veja que geralmente deixo cond separado na linha para evitar que o código fique com linhas muito longas.

Não aceitei.

[paulodt]

Professor, na sua chamada da função faltou apenas o "quote" antes das listas. Testei agora e está funcionando corretaente. Vou reorganizar o código!