search

arademaker / krr

Knowledge Representation and Reasoning
3 stars 6 forks source link

FOL formulas #24

Open arademaker opened 9 years ago

arademaker commented 9 years ago

podemos agora implementar a função wff? que estende a função preproc do tableaux tratando formulas em FOL. Para variáveis, vamos usar símbolos que começam com interrogação, ?x.

Vamos usar forall e exists para os quantificadores. Por enquanto podemos evitar funções.

arademaker commented 9 years ago

deve passar no teste

(preproc '(implies (P (f a b) (g ?x)) (not (Q a))))
arademaker commented 9 years ago

falta renomear preproc para wff? e fazer conjunto de testes, vide #37. Observem que CNF é uma WFF e deveria passar no teste. Acho que deveríamos evitar transformações em wff?, apenas teste. As transformações deveriam estar em outras funções. Em wff? só queremos saber se a entrada é uma fórmula em FOL (first order logic) e, consequentemente, em PL (propositional logic).