The Point and Click Bilateral TableauThis is a bilateral tableau that one devleops by clicking subformulae and selecting instantiations.
Why Only Bilateral?Good question! I was talking to people who teach with bilateral tableaux when I began building the LRC so that is what I built first. The modification to produce a unilateral tableau is not difficult and these will be released soon.
Not very difficult until one works with quantifiers.
Tableaux identity rules have not been implemented. Identity is just another predicate to the tableaux right now.