Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic

Lutz Straßburger 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : In this paper we introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.
Document type :
Reports
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-01526831
Contributor : Lutz Straßburger <>
Submitted on : Tuesday, May 23, 2017 - 3:34:21 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on: Friday, August 25, 2017 - 12:47:14 AM

File

RR-9071.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01526831, version 1

Citation

Lutz Straßburger. Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic. [Research Report] RR-9071, Inria Saclay Ile de France. 2017, pp.38. ⟨hal-01526831⟩

Share

Metrics

Record views

243

Files downloads

126