In this thesis I study several deductive systems for linear logic, its fragments, and some noncommutative extensions. All systems will be designed within the calculus of structures, which is a proof theoretical formalism for specifying logical systems, in the tradition of Hilbert's formalism, natural deduction, and the sequent calculus. Systems in the calculus of structures are based on two simple principles: deep inference and top-down symmetry. Together they have remarkable consequences for the properties of the logical systems. For example, for linear logic it is possible to design a deductive system, in which all rules are local. In particular, the contraction rule is reduced to an atomic version, and there is no global promotion rule. I will also show an extension of multiplicative exponential linear logic by a noncommutative, self-dual connective which is not representable in the sequent calculus. All systems enjoy the cut elimination property. Moreover, this can be proved independently from the sequent calculus via techniques that are based on the new top-down symmetry. Furthermore, for all systems, I will present several decomposition theorems which constitute a new type of normal form for derivations.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:24262 |
| Date | 24 July 2003 |
| Creators | Straßburger, Lutz |
| Contributors | Guglielmi, Alessio, Hölldobler, Steffen, Reichel, Horst, Lamarche, Francois |
| Publisher | Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | doc-type:doctoralThesis, info:eu-repo/semantics/doctoralThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0024 seconds