Intuitionistic BV (Extended version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913058576662528 |
|---|---|
| author | Acclavio, Matteo Strassburger, Lutz |
| author_facet | Acclavio, Matteo Strassburger, Lutz |
| contents | We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_13284 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Intuitionistic BV (Extended version) Acclavio, Matteo Strassburger, Lutz Logic in Computer Science We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus. |
| title | Intuitionistic BV (Extended version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.13284 |