66857 - Logic for Computer Science

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

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. Hints to the main teoretical results, like the soundnes theorem, the completeness theorem and the compactness theorem.

Readings/Bibliography

Mandatory:

• Slides prepared by the teacher

Additional suggested texts:

• A. Asperti - A. Ciabattoni, Logica a informatica, McGraw Hill, 1997.

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 of the acquired skill level 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 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

The slides, the records of lessons and additional teaching material are put in the platform Virtuale. The software Matita used in the lab sessions is available too.


Lab sessions are organized and driven by two teaching assistants.

Office hours

See the website of Claudio Sacerdoti Coen