This rule is can be used forwards to derive bottom from two contradictory lines or backwards to obtain a contradictory goal line from a bottom goal line and another formula.
Note: Bottom Introduction is the same rule as Not Elimination
To use it forwards:

1. select an empty line and click on Not Elimination
2. then select the two contradictory lines (for example a and ~a). These lines must be in scope and one of the lines must be a not formula with the other formula as the not connectives sub formula (e.g. if we have a^b as one formula the other must be ~(a^b)).
3. a bottom line will then be added to your proof.

1. select a goal line containing a formula which is just the bottom character and click on NotElimination (or Bottom Introduction as it is the same rule).
2. then select a formula which is in the scope of the goal line.
3. the converse of the formula selected will then be added as a new goal in your proof.