There is an extra comma in the last formula and the parser is still quite simple and do not support some extra spaces. Try it like this: \to(\lor(\forall x(P x),\forall x(Q x)),\forall x(\lor(P x, Q x))) and it should work fine. Wow, this is cool. However, I don't quite understand the formula format...

Hello, everybody!

I have developed a theorem prover using LOVE2D framework for visualizing the proof tree. It is available at http://www.tecmf.inf.puc-rio.br/TableauxProver .

Cheers,

Bruno.