Intersection Logic in sequent calculus style
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 pr...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1101.4424v1 |
| _version_ | 1828933604969807872 |
|---|---|
| author | Simona Ronchi Della Rocca Alexis Saurin Yiorgos Stavrinos Anastasia Veneti |
| author_facet | Simona Ronchi Della Rocca Alexis Saurin Yiorgos Stavrinos Anastasia Veneti |
| author_sort | Simona Ronchi Della Rocca |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-14T01:18:38Z |
| format | Article |
| id | doaj.art-5b3583f756e74734a762ac46e8ad96ef |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-14T01:18:38Z |
| publishDate | 2011-01-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-5b3583f756e74734a762ac46e8ad96ef2022-12-21T23:22:30ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-01-0145Proc. ITRS 2010163010.4204/EPTCS.45.2Intersection Logic in sequent calculus styleSimona Ronchi Della RoccaAlexis SaurinYiorgos StavrinosAnastasia VenetiThe 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.http://arxiv.org/pdf/1101.4424v1 |
| spellingShingle | Simona Ronchi Della Rocca Alexis Saurin Yiorgos Stavrinos Anastasia Veneti Intersection Logic in sequent calculus style Electronic Proceedings in Theoretical Computer Science |
| title | Intersection Logic in sequent calculus style |
| title_full | Intersection Logic in sequent calculus style |
| title_fullStr | Intersection Logic in sequent calculus style |
| title_full_unstemmed | Intersection Logic in sequent calculus style |
| title_short | Intersection Logic in sequent calculus style |
| title_sort | intersection logic in sequent calculus style |
| url | http://arxiv.org/pdf/1101.4424v1 |
| work_keys_str_mv | AT simonaronchidellarocca intersectionlogicinsequentcalculusstyle AT alexissaurin intersectionlogicinsequentcalculusstyle AT yiorgosstavrinos intersectionlogicinsequentcalculusstyle AT anastasiaveneti intersectionlogicinsequentcalculusstyle |