Proof nets for first-order additive linear logic

Abstract : We present canonical proof nets for first-order additive linear logic, the fragment of linear logic with sum, product, and first-order universal and existential quantification. We present two versions of our proof nets. One, witness nets, retains explicit witnessing information to existential quantification. For the other, unification nets, this information is absent but can be reconstructed through unification. Unification nets embody a central contribution of the paper: first-order witness information can be left implicit, and reconstructed as needed. Witness nets are canonical for first-order additive sequent calculus. Unification nets in addition factor out any inessential choice for existential witnesses. Both notions of proof net are defined through coalescence, an additive counterpart to multiplicative contractibility, and for witness nets an additional geometric correctness criterion is provided. Both capture sequent calculus cut-elimination as a one-step global composition operation.
Document type :
Reports
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01867625
Contributor : Lutz Straßburger <>
Submitted on : Tuesday, September 4, 2018 - 2:40:35 PM
Last modification on : Friday, June 28, 2019 - 3:01:16 PM
Long-term archiving on : Wednesday, December 5, 2018 - 4:49:58 PM

File

RR-9201.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01867625, version 1

Citation

Willem Heijltjes, Dominic Hughes, Lutz Straßburger. Proof nets for first-order additive linear logic. [Research Report] RR-9201, Inria. 2018. ⟨hal-01867625⟩

Share

Metrics

Record views

255

Files downloads

62