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.