A classical propositional theorem prover in Haskell, using Wang's Algorithm.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
execs
src/WangsAlgorithm
tests
.gitignore
.travis.yml
LICENSE
README.md
Setup.hs
WangsAlgorithm.cabal
stack.yaml

README.md

WangsAlgorithm Build Status

A propositional theorem prover in Haskell, using Wang's Algorithm, based on the sequent calculus (LK). Reading a Prolog implementation helped me understand it better.

Usage

In order to use or compile the program you need to have Stack installed.

After you cloning the repository, go to the repository folder and do

stack install

Now you installed the program. You can run it like this:

wang --sequent "[(p->q)&(p->r)] |- [p->(q&r)]" --backend Text

Or shortly:

wang -s "[(p->q)&(p->r)] |- [p->(q&r)]" -b Text

You can also use LaTeX for an output.

Here's an example text proof for that:

Before: [((p) ⊃ (q)) ∧ ((p) ⊃ (r))] ⊢ [(p) ⊃ ((q) ∧ (r))]
Rule:   AndLeft
-------------------
Before: [(p) ⊃ (q),(p) ⊃ (r)] ⊢ [(p) ⊃ ((q) ∧ (r))]
Rule:   ImpliesRight
-------------------
Before: [(p) ⊃ (q),(p) ⊃ (r),p] ⊢ [(q) ∧ (r)]
Rule:   AndRight
-------------------
First branch:
    Before: [(p) ⊃ (q),(p) ⊃ (r),p] ⊢ [q]
    Rule:   ImpliesLeft
    -------------------
    First branch:
        Before: [(p) ⊃ (r),p] ⊢ [p,q]
        Rule:   WeakeningLeft
        -------------------
        Before: [p] ⊢ [p,q]
        Rule:   WeakeningRight
        -------------------
        Before: [p] ⊢ [p]
        Rule:   Id
        -------------------
        End.

    -------------------
    Second branch:
        Before: [q,(p) ⊃ (r),p] ⊢ [q]
        Rule:   WeakeningLeft
        -------------------
        Before: [q,p] ⊢ [q]
        Rule:   WeakeningLeft
        -------------------
        Before: [q] ⊢ [q]
        Rule:   Id
        -------------------
        End.

    -------------------

-------------------
Second branch:
    Before: [(p) ⊃ (q),(p) ⊃ (r),p] ⊢ [r]
    Rule:   ImpliesLeft
    -------------------
    First branch:
        Before: [(p) ⊃ (r),p] ⊢ [p,r]
        Rule:   WeakeningLeft
        -------------------
        Before: [p] ⊢ [p,r]
        Rule:   WeakeningRight
        -------------------
        Before: [p] ⊢ [p]
        Rule:   Id
        -------------------
        End.

    -------------------
    Second branch:
        Before: [q,(p) ⊃ (r),p] ⊢ [r]
        Rule:   ImpliesLeft
        -------------------
        First branch:
            Before: [q,p] ⊢ [p,r]
            Rule:   WeakeningLeft
            -------------------
            Before: [p] ⊢ [p,r]
            Rule:   WeakeningRight
            -------------------
            Before: [p] ⊢ [p]
            Rule:   Id
            -------------------
            End.

        -------------------
        Second branch:
            Before: [r,q,p] ⊢ [r]
            Rule:   WeakeningLeft
            -------------------
            Before: [r,p] ⊢ [r]
            Rule:   WeakeningLeft
            -------------------
            Before: [r] ⊢ [r]
            Rule:   Id
            -------------------
            End.

        -------------------

    -------------------

-------------------
Proof completed.

Here's the LaTeX output for the same sequent.

\begin{prooftree}
    \AxiomC{} \RightLabel{\scriptsize $I$}
    \UnaryInfC{$p\vdash p$} \RightLabel{\scriptsize $WR$}
    \UnaryInfC{$p\vdash p,q$} \RightLabel{\scriptsize $WL$}
    \UnaryInfC{$\left( p\supset r\right) ,p\vdash p,q$}
    \AxiomC{} \RightLabel{\scriptsize $I$}
    \UnaryInfC{$q\vdash q$} \RightLabel{\scriptsize $WL$}
    \UnaryInfC{$q,p\vdash q$} \RightLabel{\scriptsize $WL$}
    \UnaryInfC{$q,\left( p\supset r\right) ,p\vdash q$}
    \RightLabel{\scriptsize $\supset L$}
    \BinaryInfC{$\left( p\supset q\right) ,\left( p\supset
               r\right) ,p\vdash q$} \AxiomC{}
    \RightLabel{\scriptsize $I$} \UnaryInfC{$p\vdash p$}
    \RightLabel{\scriptsize $WR$} \UnaryInfC{$p\vdash p,r$}
    \RightLabel{\scriptsize $WL$}
    \UnaryInfC{$\left( p\supset r\right) ,p\vdash p,r$}
    \AxiomC{} \RightLabel{\scriptsize $I$}
    \UnaryInfC{$p\vdash p$} \RightLabel{\scriptsize $WR$}
    \UnaryInfC{$p\vdash p,r$} \RightLabel{\scriptsize $WL$}
    \UnaryInfC{$q,p\vdash p,r$} \AxiomC{}
    \RightLabel{\scriptsize $I$} \UnaryInfC{$r\vdash r$}
    \RightLabel{\scriptsize $WL$} \UnaryInfC{$r,p\vdash r$}
    \RightLabel{\scriptsize $WL$}
    \UnaryInfC{$r,q,p\vdash r$}
    \RightLabel{\scriptsize $\supset L$}
    \BinaryInfC{$q,\left( p\supset r\right) ,p\vdash r$}
    \RightLabel{\scriptsize $\supset L$}
    \BinaryInfC{$\left( p\supset q\right) ,\left( p\supset
               r\right) ,p\vdash r$}
    \RightLabel{\scriptsize $\wedge R$}
    \BinaryInfC{$\left( p\supset q\right) ,\left( p\supset
               r\right) ,p\vdash \left( q\wedge r\right) $}
    \RightLabel{\scriptsize $\supset R$}
    \UnaryInfC{$\left( p\supset q\right) ,\left( p\supset
              r\right) \vdash \left( p\supset \left( q\wedge
              r\right) \right) $}
    \RightLabel{\scriptsize $\wedge L$}
    \UnaryInfC{$\left( \left( p\supset q\right) \wedge
              \left( p\supset r\right) \right) \vdash \left(
              p\supset \left( q\wedge r\right) \right) $}
\end{prooftree}

If you want to run the tests, use this command:

stack test

License

The MIT License (MIT)

Copyright (c) 2014 Joomy Korkut