A normalization procedure for the equational fragment of labelled natural deduction.

The notion of normal proof theory, and yet it has been somewhat neglected by the systems of equational logic. The intention here is then to show the normalization procedure for the equational logic of the Labelled Natural Deduction system (LND). With this we believe we are making a step towards filling a gap in the literature on equational logic. Besides presenting a normalization procedure for the LND equational fragment, we employ a new method to prove the normalization theorems for equational logic: proof transformation by rewriting, based on a algebraic calculus on the 'rewrite reasons'. [ABSTRACT FROM PUBLISHER]