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

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:

1. J.-Y. Girard, Proofs and Types (Capitoli 1,2,5,10,13, e Appendice B)

2. AA.VV., Handbook of Linear Logic (Capitoli 3 e 4)

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

4. O. Laurent, Sequentialization of Multiplicative Proof Nets

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

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

7. D. Mazza, Attack of the Exponentials

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

9. Stefano Guerrini, Correctness of Multiplicative Proof Nets is Lineare