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.Acquisire una conoscenza elementare della teoria assiomatica degli insiemi di Zermelo-Fraenkel.
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
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