TableauxProver

[blopesvieira]

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.

[vrld]

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?

[blopesvieira]

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:

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?