Created by Jesse Rappaport
In constructing a tableau, we start with the premises (if any) and the NEGATION of the conclusion. If the argument is VALID, then it should NOT be possible for the premises to be true and the conclusion false. Therefore, if we accept the negation of the conclusion, we should be able to derive a contradiction. If a branch of a tableau contains a contradiction, then we say it is "closed" (indicated here with ╳).
In the derivation, we try to break down non-atomic propositions into atomic ones or ones with negation (i.e., "literals"). Thus, we try to eliminate all binary connectives. Sometimes, reducing a binary connective requires considering two possible "states of affairs" - thus the tableau splits into two branches. For the tableau as a whole to be closed, all branches must be closed. This shows that the initial set of propositions leads to a contradiction in all cases.
HINT: To test a tautology, enter it as the conclusion with no premises.