Scienze filosofiche
Cod 198277
- Laurea magistrale
- 2 anni
- 120 CFU
- LM-78 R
MATH-01/A
Teorie Logiche 1 - LM
Codice: 20710091
Scheda insegnamento
- Anno Accademico di erogazione
- 2026/2027
- Corso di studi
- Scienze filosofiche
- 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.
- Docente
- Roberto Maieli
- Curriculum
- Curriculum unico
- Anno di corso
- 1
- Periodo
- Secondo semestre
- Ore
- 36
- CUIN
- 260007189
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
L'insegnamento di Teorie Logiche 1 rientra nell'ambito delle attività Affini e Integrative del Cds in Scienze Filosofiche. Obiettivo del corso è di fornire una conoscenza rigorosa e approfondita delle problematiche e delle metodologie essenziali delle Teorie Logiche. In particolare, affrontare alcune questioni della teoria della dimostrazione del ventesimo secolo, in connessione con le tematiche della ricerca contemporanea (nello specifico la Logica Lineare).
Risultati di apprendimento attesi
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
dimostrare dei teoremi nella deduzione naturale e nel calcolo dei sequenti della logica intuizionista, classica e lineare