Reduction Rules for Intuitionistic $${{\lambda}{\rho}}$$ λ ρ -calculus

Studia Logica 103 (6):1225-1244 (2015)
  Copy   BIBTEX

Abstract

The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules for the \-calculus, and give a simple and purely syntactical proof to the theorem by use of the reduction. In addition, we show that we can give a computation model with rich expressive power with our system

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,296

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2015-05-26

Downloads
1 (#1,913,683)

6 months
36 (#102,577)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.

Add more references