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:
Justification of formal logic. Use of paradoxes to demonstrate negative results in computer science (overview).

2. Introduction to Axiomatic Set Theory:
ZF, relations, functions, quotients, cardinality. Cantor’s Theorem.

3. Propositional Logic:
Syntax and both classical and intuitionistic semantics (overview). Classical and intuitionistic natural deduction for propositional logic. Soundness, compactness, and completeness theorems (without proofs).

4. First-Order Logic:
Syntax of first-order logic (predicates, terms, quantifiers, free and bound variables, alpha-conversion, and substitution). Semantics and natural deduction for first-order logic.

5. Recursion
BNF for Grammar Definitions. Structural induction and structural recursion.

Practical lab sessions are planned for topics 2–5.

Readings/Bibliography

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

Both textbooks cover most of the topics discussed during the lectures. For the remaining ones (intuitionistic semantics, BNF, recursion, and structural induction), supplementary material will be provided by the instructor.

Teaching methods

The course takes place in the first semester and is structured into in-class lectures and weekly lab exercises. During the lectures, all course topics are thoroughly covered, including both explanations and exercise solutions. The instructor uses slides made available through the virtuale learning platform during the lectures.


The lab exercises are designed to ensure that students fully acquire the expected competencies, particularly with regard to proving new theorems and writing recursive programs. These exercises focus on the topics covered in the lectures from the previous week. During the lab sessions, students can ask both the instructor and a lab assistant—who will always be present—for clarification and support.


Given the nature of the activities and the teaching methods adopted, attendance requires all students to have completed Modules 1 and 2 of the safety training for study environments, delivered in e-learning format.

Assessment methods

The assessment of acquired skills is based on a written exam lasting three hours, with a maximum score of 30 points. The written exam consists of 4 exercises, one for each of the course topics 2–5. Each exercise involves either performing a proof or writing a recursive program using the technique associated with the relevant topic. Full marks are awarded if the proof or code is error-free and adheres to the required technique, partial credit is given if the solution's structure is correct but contains some errors, and no points are awarded if the solution's structure is also incorrect.

The final grade proposed to the student—who has at least 48 hours to decide whether to accept it or retake the exam—is the sum of the score obtained in the most recent written exam and a bonus derived from lab exercises completed during the year. Each lab session includes approximately 3–10 exercises, each of which is awarded a small number of points if completed correctly. The total score from all lab exercises is rescaled at the end of the year so that it does not exceed 3 points, forming the bonus to be added to the written exam score. A score of 30 with honors (30/30 e lode) is awarded if the total exceeds 30 points.

 

Students with Disabilities and Specific Learning Disorders (SLD)

Students with disabilities or specific learning disorders (SLD) are entitled to special accommodations based on their condition, subject to evaluation by the University Service for Students with Disabilities and SLD. Students are kindly asked not to contact the instructor directly, but instead to make an appointment with the Service. The Service will determine the appropriate accommodations.

More information is available at:
https://site.unibo.it/studenti-con-disabilita-e-dsa/it/per-studenti

Teaching tools

The slides presented, lecture recordings, lab exercise texts, past exam papers from previous academic years along with their solutions, and additional in-depth materials are made available on the virtuale platform.

For the exercises, an interactive theorem prover (Lean) will be used, with a simplified syntax adapted to the teaching needs of the course.

Office hours

See the website of Claudio Sacerdoti Coen