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 to host generated Haddocks.

BSD3 licensed and maintained by Pedro Vasconcelos
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:

Used by 1 package:
comments powered byDisqus