The Elimination of Atomic Cuts and the Semishortening Property for Gentzen's Sequent Calculus with Equality

We study various extensions of Gentzen's sequent calculus obtained by adding rules for equality. One of them is singled out as particularly natural and shown to satisfy full cut elimination, namely also atomic cuts can be eliminated. Furthermore we tell apart the extensions that satisfy full cut elimination from those that do not and establish a strengthened form of the nonlenghtening property of Lifschitz and Orevkov.