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.
The Elimination of Atomic Cuts and the Semishortening Property for Gentzen's Sequent Calculus with Equality
Parlamento F.;
2019-01-01
Abstract
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.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
RSL-postprint.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
155.09 kB
Formato
Adobe PDF
|
155.09 kB | Adobe PDF | Visualizza/Apri |
|
RSL-preprint.pdf
accesso aperto
Tipologia:
Documento in Pre-print
Licenza:
Creative commons
Dimensione
147.68 kB
Formato
Adobe PDF
|
147.68 kB | Adobe PDF | Visualizza/Apri |
|
RSL-editorial.pdf
non disponibili
Tipologia:
Versione Editoriale (PDF)
Licenza:
Non pubblico
Dimensione
243.21 kB
Formato
Adobe PDF
|
243.21 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
