Modelling Multiplicative Linear Logic via Deep Inference
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911823330017280 |
|---|---|
| author | Galor, Tomer Schalk, Andrea |
| author_facet | Galor, Tomer Schalk, Andrea |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_01026 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Modelling Multiplicative Linear Logic via Deep Inference Galor, Tomer Schalk, Andrea Logic Logic in Computer Science 03F52 F.4 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. |
| title | Modelling Multiplicative Linear Logic via Deep Inference |
| topic | Logic Logic in Computer Science 03F52 F.4 |
| url | https://arxiv.org/abs/2404.01026 |