- Docente: Claudio Sacerdoti Coen
- Credits: 6
- SSD: INF/01
- Language: Italian
- Teaching Mode: Traditional lectures
- Campus: Bologna
-
Corso:
First cycle degree programme (L) in
Computer Science (cod. 8009)
Also valid for First cycle degree programme (L) in Philosophy (cod. 0957)
First cycle degree programme (L) in Information Science for Management (cod. 8014)
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. Prenex normal form and Skolem algorithm. 3. Mathematical induction. 4. Syntactical methods for first order. Natural deduction. Soundnes theorem. Completeness theorem. Compactness theorem. Propositional resolution; unification; first order resolution.
Readings/Bibliography
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
http://www.cs.unibo.it/~sacerdot/logica
Office hours
See the website of Claudio Sacerdoti Coen