Natural deduction and its neighbors Abstract: 1. Natural deduction rules 2. Gentzen-type sequent calculus. Prawitz translation vs Gentzen translation 3. Realizability, CH-isomorphism, Constructive type theory 4. Existential instantiation, elimination of projections 5. Resolution and deductions by elimination rules 6. Strengthened normalization: generalized elimination rules