Tableaux theorem prover for first order logic

---------------------------------------------

This is a simple interactive theorem prover for first order logic

using the tableaux method. The "tableau" is a tree depicting a proof

where each node is a sentence; linear branches represent conjunctions

while forks represent disjunctions. At each step one introduces

new nodes by "breaking down" a formula into its logical

consequences. To prove a formula F it is sufficient to show that

~F is unsatisfiable, i.e. that all branches of the tableau lead

to contradictions.

The prover is implemented in Haskell as a CGI that shows the

current proof tree and highlights one focus node

(initially the whole formula). The interface is consists of:

* navigate the proof tree (point and click)

* expand the current node

* apply resolution to the branch with the current node

Closed branches end in a "false" sentence, i.e. have been shown to

be inconsistent/unsatisfiable. To prove the original theorem one must close

all branches.

Pedro Vasconcelos <pbv@dcc.fc.up.pt>, 2009.

Tree "zipper" implementation by Krasimir Angelov & Iavor S. Diatchki, 2008.

References: First Order Logic, R. Smullyan, Dover.

On the web: http://en.wikipedia.org/wiki/Method_of_analytic_tableaux