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.


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.


You can download yahc in several flavours:
  • for a new version of GHC yahc.tar.bz2.
  • for an older version of GHC (6.8.2) yahc-6.8.tar.bz2. Probably you will need to install the following libraries:
  • as Debian packages for i386 and for amd64
  • Authors
    yahc is being developed by Renato Cherini y Miguel Pagano. You can write Miguel (see below) for reporting bugs and for asking features.
    yahc is licensed under the GPL license.
    Miguel Pagano