arXiv · 2404.01026
Modelling Multiplicative Linear Logic via Deep Inference
Abstract
Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the standard sequent calculus one, provide a simplified translation, and provide a formal proof that a standard approach to modelling is indeed invariant to all these translations. En route we establish a necessary condition for provable sequents related to the number of pars and tensors in a formula that seems to be missing from the literature.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Tomer Galor, Andrea Schalk. 2024-04-01. Modelling Multiplicative Linear Logic via Deep Inference. https://arxiv.org/abs/2404.01026
Cite the original work for its findings. Save a collection to share your selection of sources.