Proof nets for first-order additive linear logic

Willem Heijltjes; Dominic Hughes; Lutz Strassburger

doi:10.4230/LIPIcs.FSCD.2019.22

Proof nets for first-order additive linear logic

Willem Heijltjes, Dominic Hughes, Lutz Strassburger

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

75 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 language	English
Title of host publication	Fourth International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Editors	Herman Geuvers, Herman Geuvers
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	22:1-22:22
Number of pages	22
Volume	131
ISBN (Electronic)	9783959771078
ISBN (Print)	978-3-95977-107-8
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2019.22
Publication status	Published - 18 Jun 2019
Event	Fourth International Conference on Formal Structures for Computation and Deduction - Dortmund, Germany Duration: 24 Jun 2019 → 30 Jun 2019 http://easyconferences.eu/fscd2019/

Publication series

Name	Leibnitz International Proceedings in Informatics
Publisher	Schloss-Dagstuhl - Leibniz-Zentrum fuer Informatik
Volume	2019
ISSN (Electronic)	1868-8969

Conference

Conference	Fourth International Conference on Formal Structures for Computation and Deduction
Abbreviated title	FSCD 2019
Country/Territory	Germany
City	Dortmund
Period	24/06/19 → 30/06/19
Internet address	http://easyconferences.eu/fscd2019/

Keywords

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

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.FSCD.2019.22Licence: CC BY

LIPIcs-FSCD-2019-22Final published version, 684 KBLicence: CC BY

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). Article 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 or section in a book/report/conference proceeding › Chapter in a published conference proceeding

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). doi: 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{\textquoteright}s theorem, Linear logic, Proof nets",

author = "Willem Heijltjes and Dominic Hughes and Lutz Strassburger",

year = "2019",

month = jun,

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",

note = "Fourth International Conference on Formal Structures for Computation and Deduction, FSCD 2019 ; Conference date: 24-06-2019 Through 30-06-2019",

url = "http://easyconferences.eu/fscd2019/",

}

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 - Chapter in a published conference proceeding

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

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - Fourth International Conference on Formal Structures for Computation and Deduction

Y2 - 24 June 2019 through 30 June 2019

ER -

Proof nets for first-order additive linear logic

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

Proof nets for first-order additive linear logic

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this