Document Open Access Logo

Proof Nets for First-Order Additive Linear Logic

Authors Willem B. Heijltjes, Dominic J. D. Hughes, Lutz Straßburger

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.22.pdf
  • Filesize: 0.66 MB
  • 22 pages

Document Identifiers

Author Details

Willem B. Heijltjes
  • University of Bath, United Kingdom
Dominic J. D. Hughes
  • Logic Group, UC Berkeley, USA
Lutz Straßburger
  • Inria Saclay, Palaiseau, France
  • LIX, École Polytechnique, Palaiseau, France

Funding

  • Heijltjes, Willem B.: was supported by EPSRC Project EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing.
  • Straßburger, Lutz: was supported by the ANR-FWF international grant ANR-5-CE25-0014 The Fine Structure of Formal Proof Systems and their Computational Interpretations (FISP).

Acknowledgements

We would like to thank the anonymous referees for their constructive feedback. Dominic Hughes thanks his hosts, Wes Holliday and Dana Scott, at the UC Berkeley Logic Group.

Cite AsGet BibTex

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Proof Nets for First-Order Additive Linear Logic. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.22

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
Keywords
  • linear logic
  • first-order logic
  • proof nets
  • Herbrand’s theorem

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Samson Abramsky. Sequentiality vs. Concurrency in Games and Logic. Mathematical Structures in Computer Science, 13(4):531-565, 2003. Google Scholar
  2. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of LNCS, pages 222-236, 2010. Google Scholar
  3. Robin Cockett and Luigi Santocanale. On the Word Problem for ΣΠ-Categories, and the Properties of Two-Way Communication. In Computer Science Logic (CSL), 18th Annual Conference of the EACSL, pages 194-208, 2009. Google Scholar
  4. Vincent Danos. La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du Lambda-calcul). PhD thesis, Université Paris 7, 1990. Google Scholar
  5. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181-203, 1989. Google Scholar
  6. Didier Galmiche and Jean-Yves Marion. Semantic Proof Search Methods for ALL - a first approach -. Short paper in Theorem Proving with Analytic Tableaux, 4th International Workshop (TABLEAUX'95). Available from the first author’s webpage, 1995. Google Scholar
  7. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  8. Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. Logic and Algebra, pages 97-124, 1996. Google Scholar
  9. Stefano Guerrini and Andrea Masini. Parsing MELL proof nets. Theoretical Computer Science, 254(1-2):317-335, 2001. Google Scholar
  10. Willem Heijltjes. Classical proof forestry. Ann. Pure Appl. Logic, 161(11):1346-1366, 2010. Google Scholar
  11. Willem Heijltjes. Proof nets for additive linear logic with units. In 26th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 207-216, 2011. Google Scholar
  12. Willem Heijltjes and Dominic J. D. Hughes. Complexity bounds for sum-product logic via additive proof nets and Petri nets. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 80-91, 2015. Google Scholar
  13. Willem Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Proof nets for first-order additive linear logic. Technical Report RR-9201, INRIA, 2018. URL: https://hal.inria.fr/hal-01867625/.
  14. Jacques Herbrand. Investigations in proof theory: The properties of true propositions. In Jean van Heijenoort, editor, From Frege to Gödel: A source book in mathematical logic, 1879-1931, pages 525-581. Harvard University Press, 1967. Google Scholar
  15. Stefan Hetzl. A sequent calculus with implicit term representation. In Computer Science Logic (CSL), volume 6247 of LNCS, pages 351-365, 2010. Google Scholar
  16. Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In European Symposium on Programming, pages 122-138, 1998. Google Scholar
  17. Dominic J. D. Hughes. Proofs Without Syntax. Annals of Mathematics, 164(3):1065-1076, 2006. Google Scholar
  18. Dominic J. D. Hughes. Unification nets: canonical proof net quantifiers. In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2018. Google Scholar
  19. Dominic J. D. Hughes. First-order proofs without syntax. Available at arXiv.org, 2019. Google Scholar
  20. Dominic J. D. Hughes and Willem Heijltjes. Conflict nets: efficient locally canonical MALL proof nets. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016. Google Scholar
  21. Dominic J. D. Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. Transactions on Computational Logic, 6(4):784-842, 2005. Google Scholar
  22. Andre Joyal. Free Lattices, Communication and Money Games. Proc. 10th Int. Cong. of Logic, Methodology and Philosophy of Science, 1995. Google Scholar
  23. Joachim Lambek. Deductive Systems and Categories I, II, III. Theory of Computing Systems (I), Lecture Notes in Mathematics (II, III), 1968-1972. Google Scholar
  24. Roberto Maieli. Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic. In 14th Int. Conf. Logic for Programming Artificial Intelligence and Reasoning (LPAR), pages 363-377, 2007. Google Scholar
  25. Dale Miller. A Compact Representation of Proofs. Studia Logica, 46(4):347-370, 1987. Google Scholar
  26. Samuel Mimram. The Structure of First-Order Causality. Mathematical Structures in Computer Science, 21(1):65-110, 2011. Google Scholar
  27. Lutz Straßburger. A Characterisation of Medial as Rewriting Rule. In Franz Baader, editor, Term Rewriting and Applications, RTA'07, volume 4533 of LNCS, pages 344-358, 2007. Google Scholar
  28. Philip Wadler. Propositions as Sessions. Journal of Functional Programming, 24(2-3):384-418, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact