Some explanations needed about Negation in Gentzen's Natural Deduction rules I'm beginning to have an understanding thanks to some videos relating to "Proposition as Types". But, I don't come from a theoretical CS background, so maybe I'm blocked probably a bit by notation...

Given that I have understood, Conjunction, Disjunction, Implication, 

I'm stumbling on Negation:

intro:
[A]
 /\
--- 
¬ A

elim:
A ¬A    /\
----   ---- .
 /\     D


It comes from an extract of the Gentzen paper during a P. Wadler talk Proposition as Types, and I'm stuck by the meaning of the symbol resembling /\. What is this symbol called, and what is the meaning ?

Moreover, I have no clue about that D (which was not introduced) and . in:

 /\
---- . 
 D


Is it anything related to _|_ bottom in Haskell, or else the Void empty type? 

All those missing pieces makes me unable to grasp the meaning and how to apply these rules.

EDIT: I was also having difficulties with the Universal Introduction rule and this video covers the topic.
I'm guessing your first rule is:


  \begin{align*}
&amp;[A]\\
&amp;~~\vdots\\
&amp;~\bot\\
&amp;\overline{\lnot A}\qquad (I\lnot)
\end{align*}


This means that in order to derive $\lnot A$ one must first assume $A$ (that is $[A]$) and derive a contradiction ($\bot$), the dots between mean a finite number of steps. 


  $$ \frac{A \quad \lnot A}{D} \qquad (E\lnot) $$


This latter rule with $D$ seems to be ex falso quodlibet, since:

$$ \frac{A \quad \lnot A}{\bot} \qquad (E\lnot) $$

therefore:

$$ \frac{\bot}{D} $$

it says that you can derive anything (some $D$) from a contradiction.

Those $(I\circ)$ and $(E\circ)$, where $\circ$ is some operation mean Introduction-Elimination rules. In Gentzen's formulations all rules come in pairs.