Consertei a skolemização.
Separei o preproc em funções menores: wff?, um preproc para fol e outro para tableaux, e a função "standardize", que coloca todas as variáveis ligadas a "exists" ou "forall" na forma ?X1, ?X2, ?X3...
Modifiquei as funções do to-cnf para aceitarem "exists" e "forall" dentro das fórmulas e adicionei a função "move-universals" que passa todos os "forall" para fora da fórmula.
tinha um bug em uma cond de uma função, vide diff. Faltam testes!! não temos nenhuma garantia de que tantas mudanças assim estão funcionando como esperamos.
Consertei a skolemização. Separei o preproc em funções menores: wff?, um preproc para fol e outro para tableaux, e a função "standardize", que coloca todas as variáveis ligadas a "exists" ou "forall" na forma ?X1, ?X2, ?X3... Modifiquei as funções do to-cnf para aceitarem "exists" e "forall" dentro das fórmulas e adicionei a função "move-universals" que passa todos os "forall" para fora da fórmula.