Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Strong normalization proofs for cut elimination in Gentzen's sequent calculi

100%

Bittar E. T.

Banach Center Publications

1999

tom 46

nr 1

179-225

We define an equivalent variant $LK_{sp}$ of the Gentzen sequent calculus $LK$. In $LK_{sp}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $𝓔_{LK_{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 gives subrecursive bounds for the length of derivations. We give a strong normalization proof by applying orthogonal term rewriting results for a confluent restriction of the mix elimination system $𝓔_{LK_{sp}}$.

Ograniczanie wyników

1 Banach Center Publications

1 Bittar E. T.

1 1999

Wyniki wyszukiwania

Strong normalization proofs for cut elimination in Gentzen's sequent calculi