On Permuting Cut with Contraction

Preprint English OPEN
Borisavljevic, Mirjana; Dosen, Kosta; Petric, Zoran;
  • Subject: Mathematics - Logic | 03F07 (Secondary) | 03F05 (Primary) 03B20

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 which pushing cut above contraction is one of the reduction steps. The presentation of this p... View more
  • References (14)
    14 references, page 1 of 2

    Borisavljevi´c, M. [1997] A cut-elimination proof in intuitionistic predicate logic. Annals of Pure and Applied Logic 99 105-136.

    Carbone, A. [1997] Interpolants, cut elimination and flow graphs for the propositional calculus. Annals of Pure and Applied Logic 83 249-299.

    Curry, H. B. [1963] Foundations of Mathematical Logic, McGraw Hill.

    Doˇsen, K., and Petri´c, Z. [1999] Cartesian isomorphisms are symmetric monoidal: A justification of linear logic. The Journal of Symbolic Logic 64 227-242.

    Dyckhoff, R., and Pinto, L. [1997] Permutability of proofs in intuitionistic sequent calculi. University of St Andrews Research Report CS/97/7 (expanded version of a paper in Theoretical Computer Science 212, 1999, 141-155).

    Gentzen, G. [1935] Untersuchungen u¨ber das logische Schließen. Mathematische Zeitschrift 39 176-210, 405-431 (English translation in [Gentzen 1969]).

    Gentzen, G. [1938] Neue Fassung des Wiederspuchsfreiheitsbeweises fu¨r die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, N.S. 4 19-44 (English translation in [Gentzen 1969]).

    Gentzen, G. [1969] The Collected Papers of Gerhard Gentzen, Szabo, M.E. (ed.), North-Holland.

    Girard, J.-Y., Scedrov, A., and Scott, P. J. [1992] Bounded linear logic: A modular approach to polynomial-time computability. Theoretical Computer Science 97 1-66.

    Kleene, S.C. [1952] Permutability of inferences in Gentzen's calculi LK and LJ. In: Kleene, S.C. Two Papers on the Predicate Calculus, American Mathematical Society 1-26.

  • Similar Research Results (4)
  • Metrics
Share - Bookmark