This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic. A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a. special trea.tInent 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 with respect to the logical system in question.

Local computations in linear logic

SOLITRO, Ugo;
1993-01-01

Abstract

This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic. A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a. special trea.tInent 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 with respect to the logical system in question.
1993
linear logic; constructive proofs; computation
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/311994
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact