73149 - Logic for Informatics (1)

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.

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 oral exam is mandatory for those students that could not attend the lab sessions.


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.

Teaching tools

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

Office hours

See the website of Claudio Sacerdoti Coen