funçao para converter sentença em CNF

[hcrespo]

função que converte qq formula em FOL para CNF. Potencialmente usada depois por #26 para transformar a KB em listas de listas.

[arademaker]

no 21eb13f aceitei sugestões para to-cnf mas ainda resta tratar variáveis e quantificadores. Várias otimizações possíveis, remoção de implication não precisa tratar outros casos, apenas quando car é implicação acontece algo, nos demais casos apenas passa a chamada.

[hcrespo]

Tratei outros casos considerando que poderia ter uma implicação dentro da sentença, por exemplo (or A (implies B C)).

[arademaker]

Vide 6773696 a idéia.

[hcrespo]

Entendi

[arademaker]

Além disso, veja que sua versão introduziria um bug se chamada antes da preproc que trata de transformar (and A B C) em (and A (and B C)). Queremos que as transformações sejam independentes.

[hcrespo]

Fiz dessa forma pois se o 'or tivesse mais de uma argumento iria complicar para fazer as trocas dos 'and e 'or

[arademaker]

Pessoal,

fol> (skolemization '(exists ?x (forall ?y (or (implies (Q ?x) (P ?x ?y))))))
(forall ?y (or (implies (Q #:g539) (P #:g539 ?y)) nil))
fol> (to-cnf (skolemization '(exists ?x (forall ?y (or (implies (Q ?x) (P ?x ?y)))))))
nil
fol> (to-cnf '(implies (Q ?x) (P ?x ?y)))
(or nil nil)
fol> (to-cnf (skolemization '(exists ?x (forall ?y (or (implies (Q ?x) (P ?x ?y)))))))
nil

Vamos fechar este issue?