Advanced Search

We define an equivalent variant $L{K}_{sp}$ of the Gentzen sequent calculus $LK$. In $L{K}_{sp}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules ${}_{L{K}_{sp}}$ by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation...