References

  1. Beniamino Accattoli (2013): Linear Logic and Strong Normalization. In: Femke van Raamsdonk: 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics (LIPIcs) 21. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 39–54, doi:10.4230/LIPIcs.RTA.2013.39.
  2. Matteo Acclavio (2016): String diagram rewriting: applications in category and proof theory. Aix-Marseille Université. Available at matteoacclavio.com/Archive/PhdThesisAcclavio.pdf.
  3. Matteo Acclavio (2019): Proof diagrams for multiplicative linear logic: Syntax and semantics. Journal of Automated Reasoning 63(4), pp. 911–939, doi:10.1007/s10817-018-9466-4.
  4. Matteo Acclavio & Lutz Straßburger (2018): From Syntactic Proofs to Combinatorial Proofs. In: Didier Galmiche, Stephan Schulz & Roberto Sebastiani: Automated Reasoning. Springer International Publishing, Cham, pp. 481–497, doi:10.1007/978-3-319-94205-6_32.
  5. Matteo Acclavio & Lutz Straßburger (2019): On Combinatorial Proofs for Logics of Relevance and Entailment. In: Rosalie Iemhoff, Michael Moortgat & Ruy de Queiroz: Logic, Language, Information, and Computation. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 1–16, doi:10.1007/978-3-662-59533-6_1.
  6. Matteo Acclavio & Lutz Straßburger (2019): On Combinatorial Proofs for Modal Logic. In: Serenella Cerrito & Andrei Popescu: Automated Reasoning with Analytic Tableaux and Related Methods. Springer International Publishing, Cham, pp. 223–240, doi:10.1007/978-3-030-29026-9_13.
  7. Denis Bechet, Philippe de Groote & Christian Retoré (1997): A complete axiomatisation for the inclusion of series-parallel partial orders. In: Hubert Comon: Rewriting Techniques and Applications. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 230–240, doi:10.1007/3-540-62950-5_74.
  8. Kai Brünnler & Alwen Fernanto Tiu (2001): A Local System for Classical Logic. In: Robert Nieuwenhuis & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 347–361, doi:10.1007/3-540-45653-8_24.
  9. Stephen A. Cook & Robert A. Reckhow (1979): The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44(1), pp. 3650, doi:10.2307/2273702.
  10. V. Danos & L. Regnier (1995): Proof-Nets and the Hilbert Space. In: Proceedings of the Workshop on Advances in Linear Logic. Cambridge University Press, USA, pp. 307328, doi:10.1017/CBO9780511629150.016.
  11. Vincent Danos (1990): La logique linéaire appliquée à l'étude de divers processus de normalisation (principalement du λ-calcul). Thèse de Doctorat. Université Paris VII.
  12. Vincent Danos & Laurent Regnier (1989): The structure of multiplicatives. Arch. Math. Log. 28(3), pp. 181–203, doi:10.1007/BF01622878.
  13. R.J Duffin (1965): Topology of series-parallel networks. Journal of Mathematical Analysis and Applications 10(2), pp. 303–318, doi:10.1016/0022-247X(65)90125-3.
  14. Thomas Ehrhard (2014): A New Correctness Criterion for MLL Proof Nets. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14. Association for Computing Machinery, New York, NY, USA, pp. 1–10, doi:10.1145/2603088.2603125.
  15. Jean-Yves Girard (1987): Linear logic. Theoretical Computer Science 50(1), pp. 1–101, doi:10.1016/0304-3975(87)90045-4.
  16. Jean-Yves Girard (1989): Towards a geometry of interaction. Contemporary Mathematics 92(69-108), pp. 6, doi:10.1090/conm/092/1003197.
  17. Jean-Yves Girard (1998): Light Linear Logic. Information and Computation 143(2), pp. 175–204, doi:10.1006/inco.1998.2700. Available at https://www.sciencedirect.com/science/article/pii/S0890540198927006.
  18. S. Guerrini (1999): Correctness of multiplicative proof nets is linear. In: Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp. 454–463, doi:10.1109/LICS.1999.782640.
  19. Alessio Guglielmi (2007): A System of Interaction and Structure. ACM Trans. Comput. Logic 8(1), pp. 1es, doi:10.1145/1182613.1182614.
  20. Alessio Guglielmi & Lutz Straßburger (2001): Non-commutativity and MELL in the Calculus of Structures. In: Laurent Fribourg: Computer Science Logic. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 54–68, doi:10.1007/3-540-44802-0_5.
  21. Willem Heijltjes & Robin Houston (2014): No Proof Nets for MLL with Units: Proof Equivalence in MLL is PSPACE-Complete. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14. Association for Computing Machinery, New York, NY, USA, pp. 50:1–50:10, doi:10.1145/2603088.2603126.
  22. Dominic Hughes (2005): Simple Multiplicative Proof Nets with Units. Available at http://arxiv.org/abs/math.CT/0507003. Preprint.
  23. Dominic J. D. Hughes (2006): Proofs without Syntax. Annals of Mathematics 164(3), pp. 1065–1076, doi:10.2307/20160016.
  24. Dominic J.D. Hughes (2006): Towards Hilbert's 24th Problem: Combinatorial Proof Invariants: (Preliminary version). Electronic Notes in Theoretical Computer Science 165, pp. 37–63, doi:10.1016/j.entcs.2006.05.036. Proceedings of the 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006).
  25. A.P Kopylov (2001): Decidability of Linear Affine Logic. Information and Computation 164(1), pp. 173–198, doi:10.1006/inco.1999.2834.
  26. Yves Lafont (1989): Interaction nets. In: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 95–108.
  27. Yves Lafont (1995): From Proof Nets to Interaction Nets. In: J.-Y. Girard, Y. Lafont & L. Regnier: Advances in Linear Logic, London Mathematical Society Lecture Notes 222. Cambridge University Press, pp. 225–247, doi:10.1017/CBO9780511629150.012.
  28. Yves Lafont (2004): Soft linear logic and polynomial time. Theoretical Computer Science 318(1), pp. 163–180, doi:10.1016/j.tcs.2003.10.018. Implicit Computational Complexity.
  29. François Lamarche (1994): Proof nets for intuitionistic linear logic I: Essential nets. Technical Report. Imperial College, London.
  30. Olivier Laurent (2002): Étude de la polarisation en logique. Theses. Université de la Méditerranée - Aix-Marseille II. Available at https://tel.archives-ouvertes.fr/tel-00007884.
  31. Olivier Laurent (2020): Polynomial time in untyped elementary linear logic. Theoretical Computer Science 813, pp. 117–142, doi:10.1016/j.tcs.2019.10.002.
  32. Damiano Mazza (2005): Multiport Interaction Nets and Concurrency. In: Martín Abadi & Luca de Alfaro: CONCUR 2005 – Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 21–35, doi:10.1007/11539452_6.
  33. Lê Thành D~ung Nguyen & Thomas Seiller (2019): Coherent Interaction Graphs. In: Thomas Ehrhard, Maribel Fernández, Valeria de Paiva & Lorenzo Tortora de Falco: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Oxford, UK, 7-8 July 2018, Electronic Proceedings in Theoretical Computer Science 292. Open Publishing Association, pp. 104–117, doi:10.4204/EPTCS.292.6.
  34. Benjamin Ralph & Lutz Straßburger (2019): Towards a Combinatorial Proof Theory. In: Serenella Cerrito & Andrei Popescu: Automated Reasoning with Analytic Tableaux and Related Methods. Springer International Publishing, Cham, pp. 259–276, doi:10.1007/978-3-030-29026-9_15.
  35. Laurent Regnier (1992): Lambda-calcul et réseaux. Paris 7.
  36. Christian Retoré (1987): Le système F en logique linéaire. Université Paris 7, Paris.
  37. Christian Retoré (1993): Réseaux et séquents ordonnés. Theses. Université Paris-Diderot - Paris VII. Available at https://tel.archives-ouvertes.fr/tel-00585634.
  38. Christian Retoré (1996): Calcul de Lambek et Logique Linéaire. Traitement Automatique des Langues 37(2), pp. 39–70.
  39. Christian Retoré (1996): Perfect matchings and series-parallel graphs: multiplicatives proof nets as R&B-graphs.. Electronic Notes in Theoretical Computer Science 3, doi:10.1016/S1571-0661(05)80416-5.
  40. Christian Retoré (1999): Handsome Proof-nets: R&B-Graphs, Perfect Matchings and Series-parallel Graphs. Research Report RR-3652. INRIA. Available at https://hal.inria.fr/inria-00073020.
  41. Christian Retoré (1999): Pomset logic as a calculus of directed cographs. In: V. M. Abrusci & C. Casadio: Dynamic Perspectives in Logic and Linguistics: Proof Theoretical Dimensions of Communication Processes,Proceedings of the 4th Roma Workshop. Bulzoni, Roma, pp. 221–247. INRIA Research Report RR-3714 https://hal.inria.fr/inria-00072953.
  42. Christian Retoré (1999): Pomset Logic as a Calculus of Directed Cographs. In: V. M. Abrusci & C. Casadio: Dynamic Perspectives in Logic and Linguistics. Bulzoni, Roma, pp. 221–247. Also available as INRIA Rapport de Recherche RR-3714.
  43. Christian Retoré (2021): Pomset logic: The other approach to non commutativity in logic. In: Claudia Casadio & Philip J. Scott: Joachim Lambek: on the interplay of mathematics, logic and linguistics, Outstanding contributions to logic. Springer Verlag, pp. 299–246, doi:10.1007/978-3-030-66545-6.
  44. Christian Retoré (2003): Handsome proof-nets: perfect matchings and cographs. Theoretical Computer Science 294(3), pp. 473–488, doi:10.1016/S0304-3975(01)00175-X. Linear Logic.
  45. Lutz Straßburger (2003): Linear Logic and Noncommutativity in the Calculus of Structures. Technische Universität Dresden.
  46. Lutz Straßburger (2007): A Characterization of Medial as Rewriting Rule. In: Franz Baader: Term Rewriting and Applications. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 344–358, doi:10.1007/978-3-540-73449-9_26.
  47. Lutz Straßburger (2017): Combinatorial Flows and Their Normalisation. In: Dale Miller: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics (LIPIcs) 84. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 31:1–31:17, doi:10.4230/LIPIcs.FSCD.2017.31.
  48. Lutz Stra\IeCß burger (2003): MELL in the calculus of structures. Theoretical Computer Science 309(1), pp. 213–285, doi:10.1016/S0304-3975(03)00240-8.
  49. Lutz Stra\IeCß burger (2019): On the decision problem for MELL. Theoretical Computer Science 768, pp. 91–98, doi:10.1016/j.tcs.2019.02.022.
  50. Lorenzo Tortora de Falco (2000): Additives of linear logic and normalization–Part II: the additive standardization theorem.
  51. Lorenzo Tortora de Falco (2003): Additives of linear logic and normalizationPart I: a (restricted) Church–Rosser property. Theoretical Computer Science 294(3), pp. 489–524, doi:10.1016/S0304-3975(01)00176-1.
  52. Anne Sjerp Troelstra & Helmut Schwichtenberg (2000): Basic proof theory, Second Edition. Cambridge tracts in theoretical computer science 43. Cambridge University Press, doi:10.1017/CBO9781139168717.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org