Intersection Logic in sequent calculus style

Details Intersection Logic in sequent calculus style Intersection Logic in sequent calculus style

2011-01-24

arxiv.org/abs/1101.4424v1

EPTCS 45, 2011, pp. 16-30

Computer Science

Logic in Computer Science

In Proceedings ITRS 2010, arXiv:1101.4104

Scientific paper

10.4204/EPTCS.45.2

The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, and in order to support this claim we give a sequent calculus formulation of it, and we prove that it enjoys the cut elimination property.

Affiliated with

Also associated with

No associations

Rating

Intersection Logic in sequent calculus style does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Intersection Logic in sequent calculus style, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Intersection Logic in sequent calculus style will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-635547