Mathematical Logic
A.Y. 2018/2019
Learning objectives
Knowledge of the fundamental concepts of propositional and predicative
mathematical logic. Knowledge of the fundamental concepts underlying
refutational methods for automated deduction.
mathematical logic. Knowledge of the fundamental concepts underlying
refutational methods for automated deduction.
Expected learning outcomes
Undefined
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
Milan
Responsible
Lesson period
First semester
ATTENDING STUDENTS
Course syllabus
NON-ATTENDING STUDENTS
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.
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.
Professor(s)