A propositional theorem prover in Haskell, using Wang's Algorithm. Reading a Prolog implementation helped me understand it better.
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 buildNow you compiled the program. You can run it like this:
./dist/build/wang/wangThen 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.
The MIT License (MIT)
Copyright (c) 2014 Joomy Korkut