Document

# Generalized Connectives for Multiplicative Linear Logic

## File

LIPIcs.CSL.2020.6.pdf
• Filesize: 0.57 MB
• 16 pages

## Cite As

Matteo Acclavio and Roberto Maieli. Generalized Connectives for Multiplicative Linear Logic. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.6

## Abstract

In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions. We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Linear logic
##### Keywords
• Linear Logic
• Partitions Sets
• Proof Nets
• Sequent Calculus

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. V. Michele Abrusci and Roberto Maieli. Proof nets for multiplicative cyclic linear logic and Lambek calculus. Mathematical Structures in Computer Science, 29(6):733–762, 2019. URL: https://doi.org/10.1017/S0960129518000300.
2. Jean-Marc Andreoli. Focussing and proof construction. Annals of Pure and Applied Logic, 107(1):131-163, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00032-4.
3. Jean-Marc Andreoli and Laurent Mazaré. Concurrent construction of proof-nets. In International Workshop on Computer Science Logic, pages 29-42. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_3.
4. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics in multiplicative-additive linear logic. Annals of Pure and Applied Logic, 102(3):247-282, 2000. URL: https://doi.org/10.1016/S0168-0072(00)00056-7.
5. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical logic, 28(3):181-203, 1989. URL: https://doi.org/10.1007/BF01622878.
6. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
7. Jean-Yves Girard. Multiplicatives. Rendiconti del Seminario Matematico, pages 11-34, 1987.
8. Jean-Yves Girard. On Geometry of Interaction. In Helmut Schwichtenberg, editor, Proof and Computation, pages 145-191, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg.
9. Jean-Yves Girard. On the meaning of logical rules II: multiplicatives and additives. NATO ASI Series F Computer and Systems Sciences, 175:183-212, 2000.
10. Roberto Maieli. Construction of Retractile Proof Structures. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi, pages 319-333. Springer International Publishing, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_22.
11. Roberto Maieli. Non decomposable connectives of linear logic. Annals of Pure and Applied Logic, 170(11):102709, 2019. URL: https://doi.org/10.1016/j.apal.2019.05.006.
12. Roberto Maieli and Quintijn Puite. Modularity of proof-nets. Archive for Mathematical Logic, 44(2):167-193, 2005. URL: https://doi.org/10.1007/s00153-004-0242-2.
13. Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, 474:98-116, 2013.
14. Robin Milner. Communicating and mobile systems: the Pi-calculus. Cambridge university press, 1999.
X

Feedback for Dagstuhl Publishing