The tableaux package

[Tags:bsd3, program]

This is a simple web-based interactive theorem prover using semantic tableaux for propositional and first-order logic (cf. First-Order Logic, Raymond Smullyan, Dover). It allows step-by-step construction of proofs and runs on any web server supporting the CGI interface.

[Skip to Readme]


Versions 0.1, 0.2
Dependencies base (==4.*), cgi (>=3001.1), containers, haskell98, html (>=1.0), mtl (>=1.1), parsec (>=2.1 && <3), QuickCheck (>=2.1) [details]
License BSD3
Author Pedro Vasconcelos <>
Maintainer Pedro Vasconcelos <>
Category Theorem Provers
Uploaded Thu Sep 23 11:45:31 UTC 2010 by PedroVasconcelos
Distributions NixOS:0.2
Downloads 578 total (3 in the last 30 days)
0 []
Status Docs not available [build log]
All reported builds failed as of 2016-12-28 [all 7 reports]


Maintainer's Corner

For package maintainers and hackage trustees

Readme for tableaux

Readme for tableaux-0.1

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 <>, 2009.
Tree "zipper" implementation by Krasimir Angelov & Iavor S. Diatchki, 2008.

References: First Order Logic, R. Smullyan, Dover.
On the web: