Esami

Date PROSSIMI Appelli:

- 15/01/2025 ore 11:00

- 05/02/2025 ore 11:00

- 19/02/2025 ore 11:00 19/02/2025 ore 11 (aula L, Matematica)

- 04/06/2025 ore 10:00

- 30/06/2025 ore 10:00

- 10/07/2025 ore 10:00

- 08/09/2025 ore 11:00

- 22/09/2025 ore 11:00

• 22/01/2026 ore 11:00

• 05/02/2026 ore 11:00

• 19/02/2026 ore 11:00

Saranno ammessi alla prova d'esame solo gli studenti regolarmente iscritti all'appello tramite il portale dello studente GOMP. Alle ore 10 si svolgerà l'appello degli studenti iscritti all'esame, successivamente verrà stabilito dal docente un calendario con gli orari nei quali gli studenti faranno la loro presentazione.

L'esame consiste in una prova scritta (peso 1/3) + una esposizione in forma seminariale della durata di circa 30 minuti.

Prova scritta:

• Esercizi sulla deduzione naturale: (scarica esercizi svolti)

• Esercizi sulle dimostrazioni (di equivalenze fondamentali) della logica lineare usando il calcolo dei sequenti e le proof nets:

• https://lfcps.org/course/constlog16/24-linear.pdf

• https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=0985976b692d48169f411ecd116c153170f70573

• pagine 15 e 16 dell'Handbook of LL

• Esercizi sulla reversibiltà dei connettivi lineari e sulla focalizzazione delle reti.

• Esercizi sulla sequenzializzazione delle reti

• Esercizi sulla cut-reduction sulle reti.

Esempio di traccia della prova scritta:

1. scrivere le dimostrazioni di alcuni sequenti intuizionisti usando la Natural Deduction NJ e il Calcolo dei sequenti LJ

2. Scrivere le dimostrazioni di alcuni sequenti nel calcolo dei sequenti della Logica Lineare.

3. Per i vari frammenti MLL, MLL+units, MALL e MELL:

• Desequenzializzare nelle Reti Dimostrative alcune delle dimostrazioni scritte nel calcolo dei sequenti

• Effetttuare l'eliminazione dei tagli direttamente sulle Reti dimostrative

• Effettuare la sequenzializzazione di qualche rete dimostrativa nel calcolo dei sequenti.

Prova Orale

 Ogni studente sceglierà uno degli argomenti indicati nei capitoli dei libri o negli articoli di ricerca proposti qui di seguito:

MLL

7. V. Danos and L. Regnier, The structure of Multiplicatives

8. V. Danos, Une Application de la Logique Linéaire a l’Etude des Processus de Normalisation (principalement du $\lambda$-calcul)

9. O. Laurent, Sequentialization of Multiplicative Proof Nets

10. O. Laurent, Thèorie de la dèmonstration

11. S. Guerrini. A linear algorithm for MLL proof net correctness and sequentialization

12. J.-M. Andreoli and R. Maieli, Focusing and proof nets in linear and non-commutative logic

MALL

13. R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic

14. Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic.  R. Maieli

15. Conflict Nets for MALL: Dominic Hughes and Willem Heijltjes

16. Proof Nets for Unit-Free Multiplicative-Additive Linear Logic, DOMINIC J. D. HUGHES and ROB J. VAN GLABBEEK 

MELL

17. D. Mazza, Attack of the Exponentials

18. Parsing MLL Proof Nets,  Stefano Guerrini and Andrea Masini

19. C. Retoré, On the relation between coherence semantics and multiplicative proof nets.

Semantics

20. Michele Pagani ”Proofs, Denotational Semantics and Observational Equivalences in Multiplicative Linear Logic”

21. Note sulla semantica denotazionale delle strutture di prova a cura di Lorenzo Tortora de Falco.