Corsi di Laurea Corsi di Laurea Magistrale Corsi di Laurea Magistrale
a Ciclo Unico
Scuola di Scienze
INFORMATICA
Insegnamento
LOGICA 2
SC02111834, A.A. 2015/16

Informazioni valide per gli studenti immatricolati nell'A.A. 2015/16

Principali informazioni sull'insegnamento
Corso di studio Corso di laurea magistrale in
INFORMATICA
SC1176, ordinamento 2014/15, A.A. 2015/16
N0
porta questa
pagina con te
Crediti formativi 6.0
Tipo di valutazione Voto
Denominazione inglese LOGIC 2
Sito della struttura didattica http://informatica.scienze.unipd.it/2015/laurea_magistrale
Dipartimento di riferimento Dipartimento di Matematica
Obbligo di frequenza No
Lingua di erogazione ITALIANO
Sede PADOVA
Corso singolo È possibile iscriversi all'insegnamento come corso singolo
Corso a libera scelta È possibile utilizzare l'insegnamento come corso a libera scelta

Docenti
Responsabile MARIA EMILIA MAIETTI MAT/01

Mutuante
Codice Insegnamento Responsabile Corso di studio
SC03119738 LOGICA MATEMATICA 2 MARIA EMILIA MAIETTI SC1172

Dettaglio crediti formativi
Tipologia Ambito Disciplinare Settore Scientifico-Disciplinare Crediti
AFFINE/INTEGRATIVA Attività formative affini o integrative MAT/01 6.0

Organizzazione dell'insegnamento
Periodo di erogazione Primo semestre
Anno di corso I Anno
Modalità di erogazione frontale

Tipo ore Crediti Ore di
didattica
assistita
Ore Studio
Individuale
ESERCITAZIONE 2.0 16 34.0
LEZIONE 4.0 32 68.0

Calendario
Inizio attività didattiche 01/10/2015
Fine attività didattiche 28/01/2016
Visualizza il calendario delle lezioni Lezioni 2019/20 Ord.2014

Commissioni d'esame
Commissione Dal Al Membri
7 Logica Matematica 2 - a.a. 20182019 01/10/2018 30/09/2019 MASCHIO SAMUELE (Presidente)
MAIETTI MARIA EMILIA (Membro Effettivo)
BONOTTO CINZIA (Supplente)
CIRAULO FRANCESCO (Supplente)
SAMBIN GIOVANNI (Supplente)
6 Logica Matematica 2 - 2017/2018 01/10/2017 30/09/2018 SAMBIN GIOVANNI (Presidente)
MAIETTI MARIA EMILIA (Membro Effettivo)
CIRAULO FRANCESCO (Supplente)
MASCHIO SAMUELE (Supplente)
5 Logica Matematica 2 - 2016/2017 01/10/2016 30/11/2017 SAMBIN GIOVANNI (Presidente)
MAIETTI MARIA EMILIA (Membro Effettivo)
BONOTTO CINZIA (Supplente)
CIRAULO FRANCESCO (Supplente)
MASCHIO SAMUELE (Supplente)
4 Logica Matematica 2 - a.a. 2015/2016 01/10/2015 30/09/2016 MAIETTI MARIA EMILIA (Presidente)
VALENTINI SILVIO (Membro Effettivo)
BONOTTO CINZIA (Supplente)
CIRAULO FRANCESCO (Supplente)
ZANARDO ALBERTO (Supplente)

Syllabus
Prerequisiti: E' caldamente suggerito, ma non strettamente necessario, aver seguito un corso di introduzione alla logica matematica.
Conoscenze e abilita' da acquisire: Potenzialita' e limiti teorici del concetto di dimostrazione formale.
Differenze tra ragionamento classico e costruttivo.
Introduzione alla teoria della dimostrazione in logica e matematica costruttiva e sue applicazioni computazionali.
Modalita' di esame: A scelta tra una di queste tre opzioni:
1. orale su tutto il materiale del corso;
2. scritto su tutto il materiale del corso;
3. relazione orale su tema approfondito in accordo con il docente
e presentazione delle soluzioni di esercizi assegnati a lezione.
Criteri di valutazione: Capacita' dello studente di utilizzare i concetti appresi durante il corso in modo personale. Capacita' di svolgere alcuni semplici esercizi, come applicazione dei concetti appresi e delle loro principali proprieta'.
Contenuti: Calcolo dei sequenti per logica classica predicativa.
Calcolo dei sequenti per logica intuizionista predicativa.
Algoritmo di decisione per la logica intuizionista proposizionale.
Prova costruttiva del teorema di eliminazione taglio di Gentzen per entrambi
i calcoli.
Aritmetica di Peano.
Aritmetica di Heyting.
Differenze tra aritmetica di Peano e di Heyting in termini di Tesi formale di Church e assioma di scelta.
Richiami dei teoremi di incompletezza di Goedel e confronti
tra prova per l'aritmetica classica e costruttiva.
Semantica della realizzabilita' (calcolabilita') per l'aritmetica di Heyting.
Breve inquadratamento in teoria delle categorie e logica categoriale dei risultati di teoria delle dimostrazione trattati precedentemente.
Attivita' di apprendimento previste e metodologie di insegnamento: Si intende sollecitare la partecipazione attiva di ogni studente, allo scopo di mettere in moto la sua visione critica, oltre che l'apprendimento nozionistico. Quindi le lezioni tradizionali saranno accompagnate da discussioni in aula, da esercizi da svolgere personalmente e da approfondimenti a scelta su temi concordati con il docente su articoli relativi ai temi del corso.
Eventuali indicazioni sui materiali di studio: Dispense del docente, esercizi assegnati in aula e articoli
per approfondimenti proposti dal docente.
Testi di riferimento:
  • A. S. Troelstra and D. van Dalen, Constructivism in Mathematics. An Introduction. --: North-Holland, 1988. volume I and II Cerca nel catalogo
  • A. M. Pitts, Categorical Logic in Handbook of Logic in Computer Science, vol. 5. Algebraic and Logical Structures.. --: Oxford University Press, 2000. Chapter 2 Cerca nel catalogo
  • A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory. --: Cambridge University Press, 2000. second edition Cerca nel catalogo