Page begin -
Logo DISCO
|
Go to the Highly accessible area
|
Go to the Content page
|
Go to the End of content
|
Go to the Main menu
|
Go to the Navigation Bar (location)
|
Go to the Navigation menu (tree)
|
Go to the Commands list
|
Go to the Further readings
|
Go to the Bottom Menu
|
Logo Ateneo
   
Enrolled
Fondamenti logico-matematici dell'informatica

Docente: Ugo Moscato

Crediti: 4 cfu 

CONOSCENZE

Il corso si propone di analizzare alcuni argomenti di logica matematica legati alla teoria della dimostrazione in logiche non classiche (intuizionismo e logiche modali) e alla dimostrazione automatica di teoremi in tali logiche. Verranno presentati per tali logiche sistemi deduttivi a tableaux.

CAPACITA’

Si prevede che lo studente acquisisca capacità nel sintetizzare algoritmi, nella formalizzazione e costruzione di dimostrazioni e loro verifica.

PROGRAMMA

Riepilogo dei principali risultati del corso di Fondamenti logico-matematici dell'informatica (elementi).

Sintesi logica degli algoritmi

Introduzione alla logica intuizionista; sintassi a tableaux e semantica con modelli di Kripke.

Teoremi di validità e completezza.

Introduzione alla logica modale S4; sintassi a tableaux e semantica con modelli di Kripke.

Teoremi di validità e completezza.

Rapporti fra S4 e la logica intuizionista Cenni a estensioni dell'intuizionismo e di S4.

I theorem prover PITP, PITPINV, IPTP e Isabelle.

 

Further readings
(C) Copyright 2016 - Dipartimento Informatica Sistemistica e Comunicazione - Viale Sarca, 336
20126 Milano - Edificio U14
redazioneweb@disco.unimib.it - last update of this page 28/03/2011