On Permuting Cut with Contraction

dc.creatorBorisavljevic, Mirjana
dc.creatorDosen, Kosta
dc.creatorPetric, Zoran
dc.date1999-11-10
dc.date.accessioned2026-07-07T05:31:31Z
dc.date.available2026-07-07T05:31:31Z
dc.descriptionThe paper presents a cut-elimination procedure for intuitionistic propositional logic in which cut is eliminated directly, without introducing the multiple-cut rule mix, and in which pushing cut above contraction is one of the reduction steps. The presentation of this procedure is preceded by an analysis of Gentzen's mix-elimination procedure, made in the perspective of permuting cut with contraction. It is also shown that in the absence of implication, pushing cut above contraction doesn't pose problems for directly eliminating cut.
dc.description32 pages, to appear in Mathematical Structures in Computer Science
dc.identifierhttps://arxiv.org/abs/math/9911065
dc.identifierhttp://arxiv.org/abs/math/9911065
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/79375
dc.subjectLogic
dc.subject03F05 (Primary) 03B20; 03F07 (Secondary)
dc.titleOn Permuting Cut with Contraction
dc.typetext

Files

Collections