Deep inference and expansion trees for second-order multiplicative linear logic

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 :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-01942410
Contributor : Lutz Straßburger <>
Submitted on : Monday, December 3, 2018 - 11:08:55 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on : Monday, March 4, 2019 - 1:28:18 PM

File

ExpTreesLL.pdf
Files produced by the author(s)

Identifiers

Citation

Lutz Straßburger. Deep inference and expansion trees for second-order multiplicative linear logic. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, pp.1-31. ⟨10.1017/S0960129518000385⟩. ⟨hal-01942410⟩

Share

Metrics

Record views

86

Files downloads

134