Mathematical Logic
A.Y. 2020/2021
Learning objectives
The aim of the course is to introduce and deepen the fundamental concepts of propositional and predicative mathematical logic. Fundamental concepts underlying automatic deduction methods will be also explored.
Expected learning outcomes
The student must have understood the concepts and the proofs of the fundamental results of mathematical logic, both at the propositional and at the predicative level.
Further, She must have learnt the theoretical concepts automated deduction techniques are based upon
Further, She must have learnt the theoretical concepts automated deduction techniques are based upon
Lesson period: First semester
Assessment methods: Esame
Assessment result: voto verbalizzato in trentesimi
Single course
This course cannot be attended as a single course. Please check our list of single courses to find the ones available for enrolment.
Course syllabus and organization
Single session
Responsible
Lesson period
First semester
Lectures will be delivered via the platform zoom.
Course syllabus
The Mathematical Logic course provides the conceptual tools needed to implement automated deduction methods.
The course introduces syntax and semantics both at the propositional and at the predicative level, proving some of the main theorems. Further, the refutation calculi based on resolution are studied in detail. In particular, the problem of unsatisfiability will be considered, and its complexity -at propositional level- and its semi-decidability -at predicate level-.
Compactness theorem will be dealt with, together with Robinson's refutational completeness theorem, Godel's completeness theorem, Skolemisation and prenex conjunctive normal forms, and Herbrand's theory.
The course introduces syntax and semantics both at the propositional and at the predicative level, proving some of the main theorems. Further, the refutation calculi based on resolution are studied in detail. In particular, the problem of unsatisfiability will be considered, and its complexity -at propositional level- and its semi-decidability -at predicate level-.
Compactness theorem will be dealt with, together with Robinson's refutational completeness theorem, Godel's completeness theorem, Skolemisation and prenex conjunctive normal forms, and Herbrand's theory.
Prerequisites for admission
None
Teaching methods
Lectures. During the CoViD emergency, lectures will be delivered via the platform zoom.
Teaching Resources
See the web page of the course: https://homes.di.unimi.it/aguzzoli/logica.html
Bibliography:
Andea Asperti e Agata Ciabattoni: Logica a informatica. McGraw Hill Education, 1997.
Daniele Mundici: Logica: Metodo Breve. Unitext, Springer-Verlag, 2011.
Bibliography:
Andea Asperti e Agata Ciabattoni: Logica a informatica. McGraw Hill Education, 1997.
Daniele Mundici: Logica: Metodo Breve. Unitext, Springer-Verlag, 2011.
Assessment methods and Criteria
The exam consists in an oral interview that aims at verifying the students has learnt and understood the concepts introduced in the course.
This examination is divided in several parts:
- small exercises to be solved in short time
- questions about the exercises and the way the student has dealt with them
- in-depth questions
- proofs of main results
The final evaluation, expressed on a scale from 1 to 30. keeps into account how the student masters the concepts, of the exhibition clarity and property of language.
This examination is divided in several parts:
- small exercises to be solved in short time
- questions about the exercises and the way the student has dealt with them
- in-depth questions
- proofs of main results
The final evaluation, expressed on a scale from 1 to 30. keeps into account how the student masters the concepts, of the exhibition clarity and property of language.
Professor(s)