66857 - Logic for Computer Science

Course Unit Page

Academic Year 2019/2020

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. Propositional languages: syntax and semantics. Satisfiability and semantic equivalence. Syntactical methods: propositional resolution and natural deduction. Soundness and completeness. 2. First order languages. Predicates, terms, quantifiers. Syntax: free and bound variables. Interpretations. Semantics for a predicative language. Satisfiability and semantic equivalence. 3. Mathematical induction. 4. Syntactical methods for first order. Natural deduction. Soundnes theorem. Completeness theorem. Compactness theorem.


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

Teaching methods

The course is held at the second semester. It consists of frontal lessons and weakly lab sessions. 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.

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.

Links to further information


Office hours

See the website of Claudio Sacerdoti Coen