资 源 简 介
Interpreter och beviskontroll för booleanska uttryck i Haskell. Exempel:
Give me theorem.
Prover> (p ==> q, p, q <=> r) -> r
Ok. Prove theorem.
Prover> ImplE (p, p ==> q) q
Valid. Next?
Prover> :gifTrue
Axioms and conclusions:
(p ==> q, p, q <=> r, q)
Now finish your proof.
Prover> ImplE (q, q <=> r) r
Valid. Nice. Proof accepted. Next theorem?
