Tree Proof Generator Update

I've spent some more time on the Tree Proof Generator. The algorithm is now a lot faster, more information is displayed during calculation, and there are new buttons to control the drawing.

This formula (the last one on the Examples page) is quite interesting: After the quantifiers have all been dealt with, there are 36 formulas on the tree that have to be broken down by the truth-functional rules. I let it run for several hours. When finally Mozilla ran out of memory it had developed just 25 of those 36 formulas, building a tree with 179797 nodes!

I've got that formula from David Bostock's very fine book "Intermediate Logic", where he says that "the tedium of writing out a completed tableau" for this formula would be "very considerable" (p.177). Indeed.

Comments

No comments yet.

Add a comment

Please leave these fields blank (spam trap):

No HTML please.
You can edit this comment until 30 minutes after posting.