An interactive theorem prover based on semantic tableaux
|Latest on Hackage:||0.2|
This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.
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
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
Pedro Vasconcelos <firstname.lastname@example.org>, 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