Introduction and Examples

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.