search

arademaker / krr

Knowledge Representation and Reasoning
3 stars 6 forks source link

Vinicius f patch 1 #20

Closed vinicius-f closed 9 years ago

vinicius-f commented 9 years ago

Exportei o implies no arquivo packages para resolver o problema de outros pacotes usando tableaux. Adicionei outra variável no prove para devolver apenas o primeiro full-expanded branch.

arademaker commented 9 years ago

acho que (find-if #'full-expanded? branches) está bem ineficiente na rotina prove, afinal, no caso do sudoku podemos ter até 1M branches. Durante o prove-step já temos os branch deveriváveis e não deriváveis, não podemos melhorar onde fazer este teste?

arademaker commented 9 years ago 
tableaux> (prove '(and A C B) :test #'some) 
((<[false] B>) (<[false] (and A C)>))
tableaux> (prove '(and A C B) :test #'every) 
((<[false] C>) (<[false] A>) (<[false] B>))

Seguindo sua idéia de forma mais simples:

(defun prove (wff &key (test #'every))
  (do ((branches (list (list (make-formula 'false (preproc wff))))
         (prove-step branches)))
      ((or (null branches)
       (funcall test #'full-expanded? branches)) 
       branches)
    (dbg :tableaux "Branches: ~a~%" (length branches))))