yahc: Yet Another (written in) Haskell checker
yahc is a checker for derivations of
propositional calculus. Its main goal is to help first year
can be used interactively or for
checking derivations from a file.
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
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
for a new version of GHC yahc.tar.bz2.
for an older version of GHC (6.8.2)
you will need to install the following libraries:
as Debian packages for
i386 and for amd64