WangsAlgorithm

A propositional theorem prover in Haskell, using Wang's Algorithm. Reading a Prolog implementation helped me understand it better.

Usage

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

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

cabal build

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

./dist/build/wang/wang

Then you can enter propositions to see the proofs of them. Here's an example proof:

?: [(p->q)&(p->r)] |- [p->(q&r)]
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.

License

The MIT License (MIT)

Copyright (c) 2014 Joomy Korkut