Proof nets for first-order additive linear logic

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationFourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
EditorsHerman Geuvers, Herman Geuvers
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages22:1-22:22
Number of pages22
Volume131
ISBN (Electronic)9783959771078
ISBN (Print)978-3-95977-107-8
DOIs
Publication statusPublished - 18 Jun 2019
EventFourth International Conference on Formal Structures for Computation and Deduction - Dortmund, Germany
Duration: 24 Jun 201930 Jun 2019
http://easyconferences.eu/fscd2019/

Publication series

NameLeibnitz International Proceedings in Informatics
PublisherSchloss-Dagstuhl - Leibniz-Zentrum fuer Informatik
Volume2019
ISSN (Electronic)1868-8969

Conference

ConferenceFourth International Conference on Formal Structures for Computation and Deduction
Abbreviated titleFSCD 2019
CountryGermany
CityDortmund
Period24/06/1930/06/19
Internet address

Keywords

  • First-order logic
  • Herbrand’s theorem
  • Linear logic
  • Proof nets

ASJC Scopus subject areas

  • Software

Cite this

Heijltjes, W., Hughes, D., & Strassburger, L. (2019). Proof nets for first-order additive linear logic. In H. Geuvers, & H. Geuvers (Eds.), Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (Vol. 131, pp. 22:1-22:22). [22] (Leibnitz International Proceedings in Informatics; Vol. 2019). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2019.22

Proof nets for first-order additive linear logic. / Heijltjes, Willem; Hughes, Dominic; Strassburger, Lutz.

Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019). ed. / Herman Geuvers; Herman Geuvers. Vol. 131 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2019. p. 22:1-22:22 22 (Leibnitz International Proceedings in Informatics; Vol. 2019).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Heijltjes, W, Hughes, D & Strassburger, L 2019, Proof nets for first-order additive linear logic. in H Geuvers & H Geuvers (eds), Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019). vol. 131, 22, Leibnitz International Proceedings in Informatics, vol. 2019, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 22:1-22:22, Fourth International Conference on Formal Structures for Computation and Deduction, Dortmund, Germany, 24/06/19. https://doi.org/10.4230/LIPIcs.FSCD.2019.22
Heijltjes W, Hughes D, Strassburger L. Proof nets for first-order additive linear logic. In Geuvers H, Geuvers H, editors, Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Vol. 131. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2019. p. 22:1-22:22. 22. (Leibnitz International Proceedings in Informatics). https://doi.org/10.4230/LIPIcs.FSCD.2019.22
Heijltjes, Willem ; Hughes, Dominic ; Strassburger, Lutz. / Proof nets for first-order additive linear logic. Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019). editor / Herman Geuvers ; Herman Geuvers. Vol. 131 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2019. pp. 22:1-22:22 (Leibnitz International Proceedings in Informatics).
@inproceedings{2f4f851911544cd9ad8950452615140b,
title = "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.",
keywords = "First-order logic, Herbrand’s theorem, Linear logic, Proof nets",
author = "Willem Heijltjes and Dominic Hughes and Lutz Strassburger",
year = "2019",
month = "6",
day = "18",
doi = "10.4230/LIPIcs.FSCD.2019.22",
language = "English",
isbn = "978-3-95977-107-8",
volume = "131",
series = "Leibnitz International Proceedings in Informatics",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
pages = "22:1--22:22",
editor = "Herman Geuvers and Herman Geuvers",
booktitle = "Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019)",
address = "Germany",

}

TY - GEN

T1 - Proof nets for first-order additive linear logic

AU - Heijltjes, Willem

AU - Hughes, Dominic

AU - Strassburger, Lutz

PY - 2019/6/18

Y1 - 2019/6/18

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

UR - http://www.scopus.com/inward/record.url?scp=85068031876&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSCD.2019.22

DO - 10.4230/LIPIcs.FSCD.2019.22

M3 - Conference contribution

SN - 978-3-95977-107-8

VL - 131

T3 - Leibnitz International Proceedings in Informatics

SP - 22:1-22:22

BT - Fourth 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

ER -