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).
scheda docente materiale didattico
***************************************
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
https://sites.google.com/view/lm510/
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
Testi Adottati
Libri, aricoli, APPUNTI E SLIDES DISPONIBILI SULLA PAGINA WEB DEL CORSOhttps://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 netsModalità Erogazione
LEZIONI CON ESERCITAZIONI in presenza in aula ed in streamingModalità Valutazione
domande ed esercizi sui temi affrontati a lezione con una esposizione in forma seminariale