Skip to content

A classical propositional theorem prover in Haskell, using Wang's Algorithm.

License

Notifications You must be signed in to change notification settings

joom/WangsAlgorithm

Repository files navigation

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

Further Reading

  • Hao Wang, 1960, "Toward Mechanical Mathematics"
  • John McCarthy, 1961, "LISP 1.5 Programmer's Manual"

License

The MIT License (MIT)

Copyright (c) 2014 Joomy Korkut

About

A classical propositional theorem prover in Haskell, using Wang's Algorithm.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published