okitsune 狐
I am working on a new project called: okitsune 狐 - it is going to be a simple theorem prover of sorts for logic students. Okitsune is being written in Haskell and open for contributions: okitsune.sourceforge.net code sample: analytic tableaux for propositional logic