@hackage tableaux0.3

An interactive theorem prover based on semantic tableaux

  • Categories

    • License

      BSD-3-Clause

    • Maintainer

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

    • Links

    • Versions

      • 0.3 Fri, 21 Jul 2023
      • 0.2 Fri, 5 Apr 2013
      • 0.1 Thu, 23 Sep 2010

    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