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 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.
The MIT License (MIT)
Copyright (c) 2014 Joomy Korkut