The folatp from billvanyo

There is a bug in the tree pruning function.

The following exercise is from Raymond Smullyan's book First-Order Logic

         ((∀x)((F(x) ∧ G(x)) ⊃ H(x)) ⊃ (∃x)(F(x) ∧ ¬G(x))) 1=premise
               ((∀x)(F(x) ⊃ G(x)) ∨ (∀x)(F(x) ⊃ H(x))) 2=premise
      ¬((∀x)((F(x) ∧ H(x)) ⊃ G(x)) ⊃ (∃x)((F(x) ∧ G(x)) ∧ ¬H(x))) 3=¬goal

For reference, a proof can be generated here:
https://www.umsu.de/trees/#((((%E2%88%80x((Fx%E2%88%A7Gx)%E2%86%92Hx))%E2%86%92(%E2%88%83x(Fx%E2%88%A7%C2%ACGx)))%E2%88%A7((%E2%88%80x(Fx%E2%86%92Gx))%E2%88%A8(%E2%88%80x(Fx%E2%86%92Hx))))%E2%86%92((%E2%88%80x((Fx%E2%88%A7Hx)%E2%86%92Gx))%E2%86%92(%E2%88%83x((Fx%E2%88%A7Gx)%E2%88%A7%C2%ACHx))))

With the Clojure code, this can be proved with:

(def fmla1 '((forall x (((F x) and (G x)) imp (H x))) imp (exists x ((F x) and (not (G x))))))
(def fmla2 '((forall x ((F x) imp (G x))) or (forall x ((F x) imp (H x)))))
(def fmla3 '((forall x (((F x) and (H x)) imp (G x))) imp (exists x (((F x) and (G x)) and (not (H x))))))
(def tabrs (init-tableau (list fmla1 fmla2) fmla3))
(attempt-proof tabrs 252)

It finds the proof, but too much gets removed during pruning.
To see the unpruned proof, I added the following to attempt-proof right after (print-tree printable-tree):

(spit "tree.txt" (with-out-str (print-tree (convert-tree-map (:tree-map tableau) (:subst closing-subst)))))

The resulting file (the unpruned proof) is attached: tree.txt

The pruned tree is printing as:

          ((∀x)((F(x) ∧ G(x)) ⊃ H(x)) ⊃ (∃x)(F(x) ∧ ¬G(x))) 1=premise
               ((∀x)(F(x) ⊃ G(x)) ∨ (∀x)(F(x) ⊃ H(x))) 2=premise
      ¬((∀x)((F(x) ∧ H(x)) ⊃ G(x)) ⊃ (∃x)((F(x) ∧ G(x)) ∧ ¬H(x))) 3=¬goal
                       (∀X)((F(x) ∧ H(x)) ⊃ G(x)) 4=α₁.3
                      ¬(∃x)((F(x) ∧ G(x)) ∧ ¬H(x)) 5=α₂.3
                        ((F(X₄) ∧ H(X₄)) ⊃ G(X₄)) 6=γ.4
                       ¬((F(X₃) ∧ G(X₃)) ∧ ¬H(X₃)) 7=γ.5
                 ┌─────────────────────┴─────────────────────┐
 ¬(∀x)((F(x) ∧ G(x)) ⊃ H(x)) 8=β₁.1              (∃x)(F(x) ∧ ¬G(x)) 9=β₂.1
 ¬((F(X₃) ∧ G(X₃)) ⊃ H(X₃)) 10=δ.8                (F(X₄) ∧ ¬G(X₄)) 11=δ.9
      (F(X₃) ∧ G(X₃)) 12=α₁.10                         F(X₄) 14=α₁.11
          ¬H(X₃) 13=α₂.10                             ¬G(X₄) 15=α₂.11
           F(X₃) 16=α₁.12                     ┌──────────────┴──────────────┐
           G(X₃) 17=α₂.12         (∀x)(F(x) ⊃ G(x)) 18=β₁.2     (∀x)(F(x) ⊃ H(x)) 19=β₂.2
     (∀x)(F(x) ⊃ H(x)) 23=β₂.2     (F(X₄) ⊃ G(X₄)) 20=γ.18       (F(X₄) ⊃ H(X₄)) 21=γ.19
      (F(X₃) ⊃ H(X₃)) 29=γ.23                                   ┌───────────┴───────────┐
                                                     ¬(F(X₄) ∧ H(X₄)) 26=β₁.6     G(X₄) 27=β₂.6

billvanyo / folatp Goto Github PK

folatp's People

Contributors

Watchers

folatp's Issues

There is a bug in the tree pruning function.

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent