LÖVE

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.

Wow, this is cool. However, I don't quite understand the formula format:

As far as I understand, \((\forall x p(x) \vee \forall x q(x)) \rightarrow \forall x(p(x)\vee q(x))\) would be coded as: But the prover seems to be unable to parse it. Any suggestions?

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.

vrld wrote:Wow, this is cool. However, I don't quite understand the formula format:

As far as I understand, \((\forall x p(x) \vee \forall x q(x)) \rightarrow \forall x(p(x)\vee q(x))\) would be coded as:

Code: Select all

\to( \lor( \forall x(P x), \forall x(Q x) ), \forall x( \lor(P x, Q, x) ) )

But the prover seems to be unable to parse it. Any suggestions?