Linear Realisability over nets: multiplicatives (long version)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909405554933760 |
|---|---|
| author | Ragot, Adrien Seiller, Thomas de Falco, Lorenzo Tortora |
| author_facet | Ragot, Adrien Seiller, Thomas de Falco, Lorenzo Tortora |
| contents | We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL*) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL* and MLL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_17486 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Linear Realisability over nets: multiplicatives (long version) Ragot, Adrien Seiller, Thomas de Falco, Lorenzo Tortora Logic in Computer Science We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL*) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL* and MLL. |
| title | Linear Realisability over nets: multiplicatives (long version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2411.17486 |