Local computation in linear logic | Zendy

Solitro Ugo | Zendy; Valentini Silvio | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Premium

Local computation in linear logic

Author(s) -

Solitro Ugo,

Valentini Silvio

Publication year - 1993

Publication title -

mathematical logic quarterly

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.473

H-Index - 28

eISSN - 1521-3870

pISSN - 0942-5616

DOI - 10.1002/malq.19930390123

Subject(s) - mathematics , natural deduction , sequent , sequent calculus , confluence , predicate logic , propositional calculus , linear logic , rewriting , zeroth order logic , curry–howard correspondence , calculus (dental) , intuitionistic logic , cut elimination theorem , substructural logic , many valued logic , fragment (logic) , discrete mathematics , proof calculus , algorithm , computer science , theoretical computer science , programming language , multimodal logic , description logic , medicine , geometry , dentistry , mathematical proof

This work deals with the exponential fragment of Girard's linear logic ([3]) without the contraction rule, a logical system which has a natural relation with the direct logic ([10], [7]). A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut‐elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry‐Howard isomorphism ([6]) with respect to the logical system in question. MSC: 03B40, 03F05.

This content is not available in your region!

Continue researching here.

Having issues? You can contact us here

Accelerating Research