Linear logic displayed (Q918548): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Removed claim: reviewed by (P1447): Item:Q482532 |
||
Property / reviewed by | |||
Property / reviewed by: Louis F. Goble / rank | |||
Revision as of 08:44, 15 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Linear logic displayed |
scientific article |
Statements
Linear logic displayed (English)
0 references
1990
0 references
The author's Display Logic is a kind of Gentzen consecution calculus designed to effect an easy proof of an Elimination Theorem. Here the original version of Display Logic is modified to make it more elegant, and to extend it to all for the display of the Linear Logic of Girard, a system originally introduced for use in computer science. Linear Logic is displayed in the sense that a Display Logic is constructed that is provably equivalent to Linear Logic's original Hilbert-style formulation. This locates Linear Logic within a proof-theoretic framework which includes intuitionist, relevance and modal logics. It also allows variations of Linear Logic which are not accessible in the Hilbert formulation. This paper presupposes familiarity with Girard's prior work on Linear Logic and the author's prior work on Display Logic.
0 references
Display Logic
0 references
Gentzen consecution calculus
0 references
Linear Logic
0 references