Inizio della pagina -
Logo DISCO
|
Visita la Versione ad elevata leggibilità
|
Vai al Contenuto della pagina
|
Vai alla Fine dei contenuti
|
Vai al Menu Principale
|
Vai alla Barra di navigazione (sei in)
|
Vai al Menu di navigazione (albero)
|
Vai alla Lista dei comandi
|
Vai alla Lista degli approfondimenti
|
Vai al Menu inferiore
|
Logo Ateneo
   
Didattica
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

Approfondimenti

Google Translate
Translate to English Translate to French Translate to German Translate to Spanish Translate to Chinese Translate to Portuguese Translate to Arabic
Translate to Albanian Translate to Bulgarian Translate to Croatian Translate to Czech Translate to Danish Translate to Dutch Translate to Finnish Translate to Greek Translate to Hindi
Translate to Hungarian Translate to Irish Translate to Japanese Translate to Korean Translate to Norwegian Translate to Polish Translate to Romanian Translate to Russian Translate to Serbian
Translate to Slovenian Translate to Swedish Translate to Thai Translate to Turkish

(C) Copyright 2016 - Dipartimento Informatica Sistemistica e Comunicazione - Viale Sarca, 336
20126 Milano - Edificio U14
redazioneweb@disco.unimib.it - ultimo aggiornamento di questa pagina 11/10/2011