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
   
Education
Fondamenti logico-matematici dell'informatica

Codice Insegnamento: F1801Q026

Docente responsabile: 
Ugo Moscato

PROGRAMMA:
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 e vari theorem prover.

Programma:
Riepilogo dei principali risultati del corso di Logica e computazione
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.
Risultati di apprendimento previsti.
Si prevede che lo studente acquisisca capacità nel sintetizzare algoritmi, nella formalizzazione e costruzione di dimostrazioni costruttive e loro verifica.

Prerequisiti:
Nozioni di base di logica matematica classica.

Aims and contents:
The lectures will focus on non-classical logics (intuitionism and modal logics) and their proof theory in a tableaux-style suitable for automated theorem proving (ATP).Systems for ATP will be presented.

Program details:
Round-up of the main results of course Logic&Computation.
Logical synthesis of algorithms.
Introduction to intuitionistic logic; tableaux calculi and Kripke semantics.
Validity and completeness theorems.
Introduction to modal logic  S4; tableaux calculi and Kripke semantics.
Validity and completeness theorems.
Relationships between intuitionism and S4.
Logics extending intuitionism and S4.
Theorem provers PITP, PITPINV, IPTP and Isabelle.

Learning outcomes:
Ability in building proofs in intuitionism and S4 and in synthesizing algorithms from constructive proofs.

Prerequisites:
Basics in classical logic

Tipo esame:
Scritto

Tipo valutazione:
Voto finale

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 11/10/2011