Skip to Main content Skip to Navigation
New interface
Journal articles

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

Lutz Strassburger 1, 2 
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 :
Journal articles
Complete list of metadata
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Monday, December 3, 2018 - 11:08:55 AM
Last modification on : Friday, July 8, 2022 - 10:09:15 AM
Long-term archiving on: : Monday, March 4, 2019 - 1:28:18 PM


Files produced by the author(s)



Lutz Strassburger. Deep inference and expansion trees for second-order multiplicative linear logic. Mathematical Structures in Computer Science, 2019, Special Issue 8 (A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday), 29, pp.1030-1060. ⟨10.1017/S0960129518000385⟩. ⟨hal-01942410⟩



Record views


Files downloads