# tableaux: An interactive theorem prover based on semantic tableaux

[ bsd3, program, theorem-provers ] [ Propose Tags ]

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]

## Downloads

#### Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

• No Candidates
Versions [RSS] 0.1, 0.2, 0.3 base (>=4 && <5), cgi (>=3001.5.0 && <3001.6), containers (>=0.6.2 && <0.7), html (>=1.0.1 && <1.1), mtl (>=2.2.2 && <2.3), parsec (>=3.1.14 && <3.2), QuickCheck (>=2.13.2 && <2.14) [details] BSD-3-Clause Pedro Vasconcelos Pedro Vasconcelos Theorem Provers by PedroVasconcelos at 2023-07-21T16:57:28Z 1 direct, 0 indirect [details] tableaux.cgi 2022 total (9 in the last 30 days) (no votes yet) [estimated by Bayesian average] λ λ λ Docs not available All reported builds failed as of 2023-07-21

## Readme for tableaux-0.3

[back to package description]
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