Sequent Calculus for Intuitionistic Linear Propositional Logic

  • V. Michele Abrusci


Classical linear logic and its phase semantics have been introduced in [GIRARD,1987], with the proof that the sequent calculus for classical linear propositional logic is complete and sound w.r. to the validity in every topolinear space. [GIRARDLAFONT,1987] gives a formulation, but not the semantics, of the sequent calculus for the intuitionistic linear propositional logic.


Linear Structure Binary Function Linear Logic Commutative Semigroup Sequent Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. ABRUSCI V.M., Additional results on intuitionistic linear propositional logic,(in preparation).Google Scholar
  2. AVRON A., The Semantics and Proof Theory of Linear LogicLFCS, Preprint, Edinburgh, April 1987.(Published in Theoretical Computer Science, 1988).Google Scholar
  3. FUCHS L., Partially Ordered Algebraic Systems, Pergamon Press, Oxford, 1963.MATHGoogle Scholar
  4. GIRARD J.-Y., Linear Logic, Theoretical Computer Science, 50,1987.Google Scholar
  5. GIRARD J.-Y., LAFONT Y., Linear logic and lazy computation, Proceedings of the TAPSOFT, Pisa, Slncs, 250, 1987Google Scholar
  6. GRISHIN V.N., Predicate and set-theoretic calculi based on logic without contractions, Math. USSR Izvestija, Vol.18(1982), No.1, pp. 44–59.MathSciNetGoogle Scholar
  7. ONO H.- KOMORI Y., Logics without contraction rules, Journal of Symbolic Logic, 50(1985),169.MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Plenum Press, New York 1990

Authors and Affiliations

  • V. Michele Abrusci
    • 1
  1. 1.Dipartimento di Scienze FilosoficheUniversity of BariItaly

Personalised recommendations