Sequent Calculus for Intuitionistic Linear Propositional Logic
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.
KeywordsLinear Structure Binary Function Linear Logic Commutative Semigroup Sequent Calculus
Unable to display preview. Download preview PDF.
- ABRUSCI V.M., Additional results on intuitionistic linear propositional logic,(in preparation).Google Scholar
- AVRON A., The Semantics and Proof Theory of Linear LogicLFCS, Preprint, Edinburgh, April 1987.(Published in Theoretical Computer Science, 1988).Google Scholar
- GIRARD J.-Y., Linear Logic, Theoretical Computer Science, 50,1987.Google Scholar
- GIRARD J.-Y., LAFONT Y., Linear logic and lazy computation, Proceedings of the TAPSOFT, Pisa, Slncs, 250, 1987Google Scholar