Tree Prover Bugfix
I've fixed a tricky bug in my tableau prover that messed up the displayed proof in cases where the expansions of an alpha or beta formula are different, but their negation normal form is the same (example). Thanks to Christoph Pfisterer for pointing out this problem to me.
I've also begun working on a new version that allows for easy switching and editing the algorithm, so that one can use different logics and try out different precedence rules etc. At the current rate of development, this version will probably be finished around 2012.