Switch to: References

Add citations

You must login to add citations.
  1. Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
    A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their single-succedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and sequent calculus that are obtained as special instances from (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Normal deduction in the intuitionistic linear logic.G. Mints - 1998 - Archive for Mathematical Logic 37 (5-6):415-425.
    We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev. Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined with a construction $<\Gamma>$ introduced by the author to avoid cut-like constructions used in $\otimes$ (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Local computation in linear logic.Ugo Solitro & Silvio Valentini - 1993 - Mathematical Logic Quarterly 39 (1):201-212.
    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 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 (...)
    Download  
     
    Export citation  
     
    Bookmark