Done! or It's A Start!

Last night (or, more correctly, this morning) I constructed a model: ~a, b for the formulæ: ~a, a∨b using only the tableau framework and an automatically generated implementation of the propositional calculus:

Tableau> prove [Neg (Prop "a"), Disj (Prop "a") (Prop "b")]
Model [b,~a]

Now all I have to do is fix the bugs, extend what's there to labelled tableau and test it all. :-)