On Permuting Cut with Contraction

Mirjana Borisavljevic, Kosta Dosen, Zoran Petric

The 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 whi…