TY - GEN
T1 - Proof nets for first-order additive linear logic
AU - Heijltjes, Willem B.
AU - Hughes, Dominic J.D.
AU - Straßburger, Lutz
N1 - Publisher Copyright:
© Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger.
PY - 2019/6/1
Y1 - 2019/6/1
N2 - 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.
AB - 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.
KW - First-order logic
KW - Herbrand’s theorem
KW - Linear logic
KW - Proof nets
U2 - 10.4230/LIPIcs.FSCD.2019.22
DO - 10.4230/LIPIcs.FSCD.2019.22
M3 - Conference contribution
AN - SCOPUS:85068031876
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019
A2 - Geuvers, Herman
A2 - Geuvers, Herman
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019
Y2 - 24 June 2019 through 30 June 2019
ER -