search

arademaker / krr

Knowledge Representation and Reasoning
3 stars 6 forks source link

otimização prove #19

Closed arademaker closed 9 years ago

arademaker commented 9 years ago

podemos evitar que prove sempre retorne todos os branches possíveis para falsificar uma fórmula. O ideal seria termos um parâmetro em prove que pudéssemos usar para pedir apenas o primeiro branch totalmente expandido que torna a fórmula falsa.

arademaker commented 9 years ago

No c335879 introduzi um parâmetro no prove que permite que o primeiro branch full-expanded possa ser retornado sem que demais fórmulas sejam expandidas.

Comportamento default continua sendo expandir tudo:

tableaux> (prove '(and A (or C B)) :test #'every)
((<[false] B> <[false] C>) (<[false] A>))
tableaux> (prove '(and A (or C B)) :test #'some)
((<[false] A>))
tableaux> (prove '(and A (or C B)))
((<[false] B> <[false] C>) (<[false] A>))