93283 - Logics for Informatic (9 CFU)

Learning outcomes

The student will know propositional calculus and first order logic. He will be able to write and understand logical propositions and to verify them. He will be able to apply generalization and instantiation processes both in mathematics and programming.

Course contents

FIRST PART: LOGICS

1. Paradoxes and their resolution. Applications of paradoxes to obtain negative results in computer science.
2. Introduction to axiomatic set theory: ZF, relations, functions, quotients, cardinality. Cantor's theorem.
3. Propositional languages: syntax and semantics. Satisfiability and semantic equivalence. Syntactical methods: propositional resolution and natural deduction. Soundness and completeness.
4. First order languages. Predicates, terms, quantifiers. Syntax: free and bound variables. Interpretations. Semantics for a predicative language. Satisfiability and semantic equivalence.
5. BNF to define grammars. Structural induction and recursion.
6. Syntactical methods for first order. Natural deduction. Soundnes theorem. Completeness theorem. Compactness theorem.

SECOND PART: ALGEBRA

1. Generalization, abstraction, instantiation in mathematics and computer science. Higher order functions.
2. Introduciton to algebra: semigroups, monoids, groups and their applications to generic programming.

Readings/Bibliography

1. A. Asperti - A. Ciabattoni, Logica a informatica, McGraw Hill, 1997.
2. Slides prepared by the teacher

Teaching methods

The course is held during the first semester. It consists of frontal lessons and weakly lab sessions. The lab sessions are held on-line. During the frontal lessons all topics of the course will be presented. Almost every theorem will be proved rigorously. During the labe sessions we ask the student to apply the knowledge acquired during the previous week to proving new theorems.

 

In consideration of the kind of activity and didactic methods, attending this teaching activity requires having attended to Moduli 1 e 2 di formazione sulla sicurezza nei luoghi di studio, [https://elearning-sicurezza.unibo.it/ ]. Attendance of the security modules is in e-learning mode only.

Assessment methods

Assessment is based on the analysis of the scripts produced during the lab sessions, and on a written exam. The student who delivers a sufficent written exam can take an optional oral exam to improve his mark. The final score is obtained from the score of the written exam and from a bonus obtained analyzing the performance in lab.


The lab sessions are aimed at learning tools to self-assess the skill of producing new rigorous mathematical proof. The software Matita is used in the lab sessions.


The written exam lasts 3 hours. It comprises both questions about the definitions, statements and proofs presented during the course, and exercises about problem solving and the production of new proofs.

Students with disabilities and Specific Learning Disorders (SLD)Students with disabilities or Specific Learning Disorders have the right to special accommodations according to their condition, following an assessment by the Service for Students with Disabilities and SLD. Please do not contact the teacher but get in touch with the Service directly to schedule an appointment. It will be the responsibility of the Service to determine the appropriate adaptations. For more information, visit the page:

https://site.unibo.it/studenti-con-disabilita-e-dsa/en/for-students

Teaching tools

All course slides are put on the Web. The software Matita used in the lab sessions is available too.

Lab sessions are organized and driven by two teaching assistants: Davide Barbarossa <davide.barbarossa@unibo.it> and Pietro Lami <pietro.lami@unibo.it>

Office hours

See the website of Claudio Sacerdoti Coen

See the website of Fabio Zanasi