Sequent Calculus in Natural Deduction Style
Negri, Sara ; von Plato, Jan
J. Symbolic Logic, Tome 66 (2001) no. 1, p. 1803-1816 / Harvested from Project Euclid
A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction.
Publié le : 2001-12-14
Classification: 
@article{1183746626,
     author = {Negri, Sara and von Plato, Jan},
     title = {Sequent Calculus in Natural Deduction Style},
     journal = {J. Symbolic Logic},
     volume = {66},
     number = {1},
     year = {2001},
     pages = { 1803-1816},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183746626}
}
Negri, Sara; von Plato, Jan. Sequent Calculus in Natural Deduction Style. J. Symbolic Logic, Tome 66 (2001) no. 1, pp.  1803-1816. http://gdmltest.u-ga.fr/item/1183746626/