\subsection{Natural deduction}
The rules from above here are used to construct derivations under assumptions, e.g.
$A_1, \ldots, A_n \vdash A$, which is read as ``$A$ follows from $A_1, \ldots, A_n$''.

The derivations are always represented as derivation trees and a \bi{proof} is a derivation whose root has no assumptions.

Since we have to prove a statement, we have to draw the derivation trees from the bottom up, with the goal of reaching an axiom or a rule that is an assumption
using the other rules of the rule set.