Main differences and relations between Sequent Calculus and Natural Deduction

What are the main differences between the Sequent Calculus and the Natural Deduction (independently of if we're working with classical, intuitionistic or another logic) ?

As far as I know :

Differences :

• The sequent calculus is more suitable for automated proof search. Why is that so ?
• The cut rule is implicit (based on $\Rightarrow$-intro and $\Rightarrow$-elim, right ?) in the Natural Deduction and explicit in the Sequent Calculus.
• The Natural Deduction give a more mathematical-like approach to reasoning while the Sequent calculus give more structural and symmetrical approach.
• I read (about the Sequent Calculus) that It presents numerous analogies with natural deduction, without being limited to the intuitionistic case in Proof and Types by J-Y Girard. Why is Natural Deduction said to be limited to the intuitionistic case ? Can't we add a rule for the excluded middle to simulate classical logic ?

Relations :

• One can be translated to the other

I can't think of others ones.

Are my claims above right ? Is there any other interresting differences and relations (or fact) ?

Probably your last comment about double negation elimination breaking the symmetry of natural deduction is the 'reason' for the cited quote, though I don't agree with the sentiment.

Basically, natural deduction has introduction and elimination rules for each one of "$\land$" and "$\lor$" and "$\to$", which correspond to their intended meanings. We also have negation introduction in the form "$A \to \bot \vdash \neg A$" and negation elimination in the form "$A , \neg A \vdash \bot$". So double negation elimination (DNE) is an 'odd one out', so to speak, being "$\neg \neg A \vdash A$" or equivalently "$( A \to \bot ) \to \bot \vdash A$". I'm excluding the principle of explosion here because it is redundant in the presence of DNE.

Also, note that you can prove each instance of LEM using DNE plus the other rules, so adding DNE suffices to recover classical logic. If you added LEM instead of DNE, you would also have to add the principle of explosion, namely "$\bot \vdash A$" for any proposition $A$. In that sense DNE can be said to be slightly stronger than LEM. Intuitively it is obviously the case, because we would need at least one rule that reduces the total number of occurrences of "$\neg$" or "$\bot$", and LEM does not do so. Both the principle of explosion and DNE reduce that number, by $1$ and $2$ respectively. But adding just the principle of explosion is not enough to get classical logic, because it only results in intuitionistic logic.

For your other points, your statement that natural deduction is less suitable than sequent calculus for automated proof systems is arguably false. Even though the LK calculus works without the cut rule, it is not useful to take that rule away because it shortens proofs drastically in the same way that allowing on-the-fly definitions makes modern mathematics possible (we can't get far if we're not allowed to define arbitrary new terminology).

And as for the cut rule being implicit in ND via implication introduction and elimination, well is that really implicit? We could modify the other rules appropriately so that none of them use the implication symbol, and then indeed those two rules would become redundant in the same manner as the cut rule. So it looks quite explicit to me. As with LK, it is not useful in practice to take away these rules.