In the first part of this tutorial we are introducing the tableau workbech by means of a small example
based on classical propositional logic. We give the the for the calculus, both in tableau and sequent notation
and we show a simple negation normal form function. Then we show how to run the TWB from the command line
and how to trace the proof.