Logica
per il corso di Laurea Breve in Informatica
a.a. 2003/2004
docente Silvio Valentini
Periodo
Il corso si svolge nel terzo trimestre.
Prerequisiti
Questo corso non richiede ad alcun prerequisito
specifico in logica matematica ma si suppone che lo studente abbia
seguito i corsi base
di matematica e che della matematica sappia utilizzare almeno le
tecniche piu` elementari che egli dovrebbe aver appreso nel corso di
Matematica di Base. Visto l'accento che il corso porra`
sull'effettivita` dei processi di
calcolo e` opportuno che lo studente abbia seguito pure un corso
introduttivo all'informatica quale ad esempio Informatica di Base.
Scopo del corso
Lo scopo principale del corso e` quello di Illustrare i
legami tra sintassi e semantica e mettere in evidenza sia le
possibilita` che i calcoli sintattici offrono, come pure i limiti
espressivi e dimostrativi che essi impongono.
Programma del corso
Contenuto del corso:
- Richiami di teoria degli insiemi (insieme,
operazione, funzione, relazione) (4 ore)
- Nozioni linguistiche di base: applicazione e
astrazione, lambda calcolo tipato semplice, teorema di forma normale,
decidibilita` dell'ugualianza (6 ore)
- Concetti semantici di base: struttura,
valutazione, interpretazione
(4 ore)
- Concetti sintattici di base: espressione,
proposizione, alberi di confutazione, dimostrazione (6 ore)
- Equivalenza tra semantica e sintassi: teorema di
completezza (4 ore)
- Limiti espressivi del linguaggio: teorema di
compattezza e sue applicazioni (4 ore)
- Limiti computazionali: funzioni recursive e
macchine di Turing (6 ore), problema dell'arresto, indecidibilita` del
calcolo predicativo del primo ordine (4 ore)
- Limiti dimostrativi: teoria formale dei numeri
naturali, rappresentazione delle funzioni recursive (6 ore), teoremi di
Goedel e di Loeb (6 ore)
Testi di riferimento
J.Bell, M.Machover, A course in mathematical logic
G.S.Boolos, R.C.Jeffrey, Computability and Logic
Dispense del docente:
Introduzione agli insiemi,
Lambda calcolo tipato,
Introduzione alla logica classica,
Indecidibilita` del calcolo predicativo,
Esercizi sul lambda calcolo,
Metodo di risoluzione,
Compattezza e unificazione
Correzione Appelli d'esame
24 giugno 2003,
8 luglio 2003,
8 settembre 2003,
26 settembre 2003
25 maggio 2004,
23 giugno 2004,
7 luglio 2004,
1 settembre 2004,
15 settembre 2004
24 giugno 2005,
14 luglio 2005,
2 settembre 2005,
21 settembre 2005.
[Back]
