Hostname: page-component-599cfd5f84-z6fpd Total loading time: 0 Render date: 2025-01-07T07:25:23.121Z Has data issue: false hasContentIssue false
  • English
  • Français

On permuting cut with contraction

Published online by Cambridge University Press:  01 April 2000

MIRJANA BORISAVLJEVIĆ ,
KOSTA DOšEN  and
ZORAN PETRIĆ
MIRJANA BORISAVLJEVIĆ
Affiliation:
Faculty of Transport and Traffic Engineering, University of Belgrade, Vojvode Stepe 305, 11000 Belgrade, Yugoslavia
KOSTA DOšEN
Affiliation:
IRIT, University of Toulouse III, 31062 Toulouse cedex, France, and Mathematical Institute, P.O. Box 367, 11001 Belgrade, Yugoslavia, Email: [email protected]
ZORAN PETRIĆ
Affiliation:
Faculty of Mining and Geology, University of Belgrade, Djušina 7, 11000 Belgrade, Yugoslavia
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 10 , Issue 2 , April 2000 , pp. 99 - 136
Copyright
© 2000 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)