funçao para converter sentença em CNF

arademaker / krr

Knowledge Representation and Reasoning

3 stars 6 forks source link

funçao para converter sentença em CNF #31

Open hcrespo opened 9 years ago

hcrespo commented 9 years ago

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

arademaker commented 9 years ago

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 commented 9 years ago

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

arademaker commented 9 years ago

Vide 6773696 a idéia.

hcrespo commented 9 years ago

Entendi

arademaker commented 9 years ago

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 commented 9 years ago

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

arademaker commented 9 years ago

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?