- Oggetto:
- Oggetto:
Logica per l'Informatica
- Oggetto:
Logic for Computer Science
- Oggetto:
Anno accademico 2023/2024
- Codice attività didattica
- INF0102
- Docente
- Luca Luigi Paolini (Titolare)
- Corso di studio
- [008515] Laurea magistrale in informatica
- Anno
- 1° anno, 2° anno
- Periodo
- Secondo semestre
- Tipologia
- A scelta dello studente
- Crediti/Valenza
- 6 CFU (Ore aula: 48)
- SSD attività didattica
- MAT/01 - logica matematica
- Erogazione
- Tradizionale
- Lingua
- Italiano
- Frequenza
- Facoltativa
- Tipologia esame
- Orale
- Prerequisiti
-
Conoscenze elementari ed informali di logica, teoria degli insiemi e matematica discreta. Conoscenze elementari di linguaggi formali.
Insegnamenti propedeutici*:- Logica e Matematica Discreta
- Linguaggi Formali e Compilatori
* Che forniscono le competenze attese in ingresso.
Basic knowledge of informal logic, Set Theory and discrete mathematics. Basic knowledge of formal languages.
Preparatory Courses*:- Logics and discrete mathematics
- Formal Languages and Compilers
* Providing the expected entry skills
- Mutuato da
- Logica per l'Informatica (INF0003)Corso di laurea in Informatica
- Logica per l'Informatica (INF0003)
- Oggetto:
Sommario insegnamento
- Oggetto:
Avvisi
- Oggetto:
Obiettivi formativi
La laurea in Informatica ha l'obiettivo di formare figure professionali dotate di un solido nucleo scientifico e metodologico, arricchito con un'ampia preparazione tecnologica. In questo quadro, il corso fornisce agli studenti gli strumenti formali per il ragionamento rigoroso sia nel contesto informale dei linguaggi naturali che in quelli assistiti dal calcolatore. Sono affrontati approcci algoritmici per l'automazione di verifiche di soddisfacibilità e validità. In particolare, sono enfatizzate le potenzialità della logica come strumento per una descrizione rigorosa della specifica di un programma e per porre le basi della verifica automatica di proprietà di programmi.Questo insegnamento concorre agli obiettivi formativi dell'ambito propedeutico del Corso di Laurea Magistrale in Informatica".
The degree in Computer Science aims to train professionals with a solid scientific and methodological core, enriched by a broad technological preparation. In this framework, the course provides students with the formal tools for rigorous reasoning both in the informal context of natural and computer-aided languages. Algorithmic approaches for the automation of satisfiability and validity checks are addressed. In particular, the potential of logic as a tool for a rigorous description of the specification of a program and for laying the foundations for the automatic verification of program properties is emphasised.This teaching contributes to the educational objectives of the preparatory area of the Master's Degree in Computer Science.
- Oggetto:
Risultati dell'apprendimento attesi
Il irsultato atteso è l'acquisizione dei principi fondamentali della logica formale ed in particolare, la capacità di sviluppare dimostrazioni in modo autonomo. Inoltre, apprende le idee alla base delle tecniche disponibili per il suo utilizzo per la specifica e la verifica della rappresentazione dei dati, dei programmi.CONOSCENZA E CAPACITÀ DI COMPRENSIONE. Sintassi e semantica della logica classica. Procedure di decisione utili alla caratterizzazione di soddisfacibilità e validità delle formule.
CAPACITÀ DI APPLICARE CONOSCENZA E COMPRENSIONE. Capacità di impostare dimostrazioni corrette delle proprietà del software. Capacità di formalizzare proprietà da verificare in maniera automatica.
AUTONOMIA DI GIUDIZIO. Acquisizione dei criteri di base per stabilire la correttezza della formalizzazione di un problema e della sua validità.
ABILITÀ COMUNICATIVE. Capacità di base su come impostare un ragionamento corretto e fluente.
CAPACITÀ DI APPRENDIMENTO. Acquisizione di capacità autonome di apprendimento e di autovalutazione della propria preparazione, teorica e pratica.
Student acquires the fundamental principles of formal logic and in particular, the ability to develop proofs independently. In addition, he learns the ideas behind the techniques available for its use for the specification and verification of data representation, programs.
KNOWLEDGE AND UNDERSTANDING. Syntax and semantics of classical logic. Decision procedures useful for the characterization of satisfiability and validity of formulas.
ABILITY TO APPLY KNOWLEDGE AND UNDERSTANDING. Ability to set up correct demonstrations of software properties. Ability to formalize properties to be verified automatically.
AUTONOMY OF JUDGMENT. Acquisition of the basic criteria to establish the soundness of a formalization its validity.
COMMUNICATION SKILLS. Basic skills on how to set up correct and fluent reasoning.
LEARNING ABILITY. Acquisition of autonomous learning skills and self-assessment of one's own theoretical and practical preparation.
- Oggetto:
Programma
- Linguaggio proposizionale, connettivi e basi.
- Metalinguaggio, induzione strutturale e semantica alla Tarski, interpretazioni.
- Equivalenze e sostituzione, SAT, UNSAT, tautologie e falsificabili.
- Tableaux: terminazione, correttezza e completezza.
- Sistemi deduttivi, Gentzen e corrispondenza con i tableaux.
- CNF, tseytin-transformation, risoluzione: terminazione, correttezza e completezza.
- BDD, DP and DPLL algoritms (SAT solver): terminazione, correttezza e completezza.
- Logica al primo-ordine: sistemi deduttivi, interpretazione e modelli, correttezza e completezza.
- Cenni ad altre sistemi logici.
- Propositional language, operators and basis
- Metalanguage, structural induction and Tarski's semantics, interpretations ans valuations.
- Logical equivalence and substitution, SAT, UNSAT, tautology and falsifiable formulas.
- Tableaux: termination, soundness and completeness.
- Deductive systems, Gentzen and relationship with Tableaux
- CNF, tseytin-transformation, resolution: termination, soundness and completeness.
- BDD, DP and DPLL algoritms (SAT solver): termination, soundness and completeness.
- First order logic: models, tableaux: termination, soundness and completeness.
- Conclusions and suggestions
- Oggetto:
Modalità di insegnamento
Le lezioni sono erogate in maniera tradizionale, ossia frontalmente. La presenza è seriamente consigliata (siccome statisticamente incrementa significativamente le possibilità di superare l'esame). La proiezione di diapositive viene usata per tracciare i contenuti, e queste vengono ampiamente integrate con dettagli su lavagna e/o tablet (ad esempio per le dimostrazioni).
Lectures are delivered in the traditional way, i.e. face-to-face. Attendance is seriously recommended (since statistically it significantly increases the chances of passing the exam). Slideshow is used to outline lecture contents, and these are extensively supplemented with details on whiteboard and/or tablet (e.g. for demonstrations).
- Oggetto:
Modalità di verifica dell'apprendimento
Esame orale in presenza. Lo studente viene interrogato sui contenuti del corso: (i) teoremi e dimostrazioni; (ii) algoritmi e proprietà; (iii) esercizi sugli approcci presentati.Oral exam in presence. The student is questioned about the contents of the course: (i) theorems and their proofs; (ii) algorithms and their properties; (iii) exercises on the presented approaches.Testi consigliati e bibliografia
- Oggetto:
- Libro
- Titolo:
- Mathematical Logic for Computer Science (3rd Ed.)
- Anno pubblicazione:
- 2012
- Editore:
- Springer-Verlag
- Autore:
- Ben-Ari, Mordechai
- ISBN
- Permalink:
- Note testo:
- Materiale a cura del docente verra distribuito nella pagina moodle del corso.
- Obbligatorio:
- Si
- Oggetto:
