Matematica
Cod 198373
- Laurea magistrale
- 2 anni
- 120 CFU
- LM-40 R
MATH-01/A
LM510 - Teorie Logiche 1
Codice: 20410529
Scheda insegnamento
- Anno Accademico di erogazione
- 2026/2027
- Corso di studi
- Matematica
- Periodo di erogazione
- Secondo semestre
- CFU
- 6 CFU
- Lingua
- Italiano
- SSD
- MATH-01/A
Scopri il programma didattico
Programma, testi adottati e modalità d’esame sono quelli pubblicati dai docenti per l’anno accademico 2026/2027. L’insegnamento è diviso in canali: ogni canale ha il suo programma.
- Docente
- Roberto Maieli
- Curriculum
- Teorico
- Anno di corso
- 1
- Periodo
- Secondo semestre
- Ore
- 36
- CUIN
- 260004521
Programma
Dimostrazioni (Sequent Proofs)
***************************************
Deduzione Naturale (ND)
Il Calcolo dei Sequenti per la Logica Intuizionista (LJ) e Logica Classia (LK)
L'eliminazione dei Tagli per LJ ed LK
Il calcolo dei sequenti della Logica Lineare (LL)
Il teorema di Eliminazione dei Tagli per LL
Il Teorema di Focalizzazione delle dimostrazioni di LL
Reti dimostrative (Proof Nets)
*************************************
(stutture dimostrative, correttezza, normalizzazione, adeguatezza, sequenzializzazione, focalizzazione, complessità)
Reti puramente moltiplicative
Reti moltplicative-additive
Reti moltiplicative-esponenziali
Semantica Denotazionale
Prerequisiti
è consigliato che lo studente abbia già seguito un corso di logica di base
Testi adottati
Libri, aricoli, APPUNTI E SLIDES DISPONIBILI SULLA PAGINA WEB DEL CORSO
https://sites.google.com/view/lm510/
Bibliografia di riferimento
J.-Y. Girard, Proofs and Types
AA.VV., Handbook of Linear Logic
V. Danos and L. Regnier, The structure of Multiplicatives
O. Laurent, Sequentialization of Multiplicative Proof Nets
J.-M. Andreoli and R. Maieli, Focusing and proof nets in linear and non-commutative logic
R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicativeand Additive Fragment of Linear Logic
D. Mazza, Attack of the Exponentials
C. Retoré, On the relation between coherence semantics and multiplicative proof nets
Modalità di erogazione
LEZIONI CON ESERCITAZIONI in presenza in aula ed in streaming
Modalità di frequenza
la frequenza delle lezioni non è obbligatoria ma fortemente incoraggiata ed auspicata
Modalità di valutazione
domande ed esercizi sui temi affrontati a lezione con una esposizione in forma seminariale
Prove previste
- Prova orale
- Prova scritta
- Docente
- Roberto Maieli
- Curriculum
- Matematica applicata e computazionale
- Anno di corso
- 1
- Periodo
- Secondo semestre
- Ore
- 36
- CUIN
- 260004579
Programma
Dimostrazioni (Sequent Proofs)
***************************************
Deduzione Naturale (ND)
Il Calcolo dei Sequenti per la Logica Intuizionista (LJ) e Logica Classia (LK)
L'eliminazione dei Tagli per LJ ed LK
Il calcolo dei sequenti della Logica Lineare (LL)
Il teorema di Eliminazione dei Tagli per LL
Il Teorema di Focalizzazione delle dimostrazioni di LL
Reti dimostrative (Proof Nets)
*************************************
(stutture dimostrative, correttezza, normalizzazione, adeguatezza, sequenzializzazione, focalizzazione, complessità)
Reti puramente moltiplicative
Reti moltplicative-additive
Reti moltiplicative-esponenziali
Semantica Denotazionale
Prerequisiti
è consigliato che lo studente abbia già seguito un corso di logica di base
Testi adottati
Libri, aricoli, APPUNTI E SLIDES DISPONIBILI SULLA PAGINA WEB DEL CORSO
https://sites.google.com/view/lm510/
Bibliografia di riferimento
J.-Y. Girard, Proofs and Types
AA.VV., Handbook of Linear Logic
V. Danos and L. Regnier, The structure of Multiplicatives
O. Laurent, Sequentialization of Multiplicative Proof Nets
J.-M. Andreoli and R. Maieli, Focusing and proof nets in linear and non-commutative logic
R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicativeand Additive Fragment of Linear Logic
D. Mazza, Attack of the Exponentials
C. Retoré, On the relation between coherence semantics and multiplicative proof nets
Modalità di erogazione
LEZIONI CON ESERCITAZIONI in presenza in aula ed in streaming
Modalità di frequenza
la frequenza delle lezioni non è obbligatoria ma fortemente incoraggiata ed auspicata
Modalità di valutazione
domande ed esercizi sui temi affrontati a lezione con una esposizione in forma seminariale
Prove previste
- Prova orale
- Prova scritta
Esplora gli obiettivi dell’insegnamento
Ambito disciplinare: Attività formative affini o integrative
Affrontare alcune questioni della teoria della dimostrazione del ventesimo secolo, in connessione con le tematiche della ricerca contemporanea
Risultati di apprendimento attesi — Roberto Maieli
Al termine del corso lo studente dovrà:
* conoscere i principali sistemi di deduzione della logica intuizionista, classica e lineare;
* saper costruire e analizzare derivazioni in deduzione naturale e nei calcoli dei sequenti LJ, LK e della logica lineare;
* comprendere i principali risultati di teoria della dimostrazione, in particolare normalizzazione, proprietà della sottoformula, eliminazione del taglio e focalizzazione;
* conoscere la nozione di proof net e i principali criteri di correttezza, sequenzializzazione e normalizzazione;
* saper confrontare differenti rappresentazioni delle dimostrazioni e valutarne proprietà strutturali e computazionali;
* utilizzare con autonomia e precisione il linguaggio e gli strumenti della teoria della dimostrazione.
Risultati di apprendimento attesi — Roberto Maieli
Al termine del corso lo studente dovrà:
* conoscere i principali sistemi di deduzione della logica intuizionista, classica e lineare;
* saper costruire e analizzare derivazioni in deduzione naturale e nei calcoli dei sequenti LJ, LK e della logica lineare;
* comprendere i principali risultati di teoria della dimostrazione, in particolare normalizzazione, proprietà della sottoformula, eliminazione del taglio e focalizzazione;
* conoscere la nozione di proof net e i principali criteri di correttezza, sequenzializzazione e normalizzazione;
* saper confrontare differenti rappresentazioni delle dimostrazioni e valutarne proprietà strutturali e computazionali;
* utilizzare con autonomia e precisione il linguaggio e gli strumenti della teoria della dimostrazione.
Esempi di domande d’esame
Roberto Maieli
dimostrare dei teoremi nella deduzione naturale e nel calcolo dei sequenti della logica intuizionista, classica e lineare
Roberto Maieli
dimostrare dei teoremi nella deduzione naturale e nel calcolo dei sequenti della logica intuizionista, classica e lineare