# yahc: Yet Another (written in) Haskell checker

yahc is a checker for derivations of propositional calculus. Its main goal is to help first year students.

#### Use

yahc can be used interactively or for checking derivations from a file.
##### Interactive mode
In this mode, one starts a derivation by telling the checker the l.h.s. and the r.h.s. of the equivalence to be proved (in the case that the theorem is not of the form p ≡ q, but a formulat, then one can start with the goal t ≡ True). After indicating the goal one proceeds which rule should be applied and the expected outcome of applying that rule; yahc checks that the expected result can be in fact be obtained by using that rule. If that were the case, then the user can continue with the proof until reaching the r.h.s. of the equality indicated at the beginning.
##### Verifying derivations in files
One can also use yahc for verifying complete derivations on files; in this case one does not need to indicate the equivalence to be proved; instead yahc will check that each step is correct; hence the theorem proved will be that p ≡ q is a theorem, where p is the formula in the first line and q the formula in the last line.