Authors: Borisavljević, Mirjana
Došen, Kosta 
Petrić, Zoran 
Affiliations: Mathematical Institute of the Serbian Academy of Sciences and Arts 
Mathematical Institute of the Serbian Academy of Sciences and Arts 
Title: On permuting cut with contraction
Journal: Mathematical Structures in Computer Science
Issue Date: 1-Jan-2000
Rank: M23
ISSN: 0960-1295
DOI: 10.1017/S0960129599003011
This 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. We also show that in the absence of implication, pushing cut above contraction does not pose problems for directly eliminating cut.
Publisher: Cambridge University Press

Show full item record


checked on Jul 22, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.