| Activity | Credits | Period | Academic staff | Timetable |
|---|---|---|---|---|
| Parte 1 | 3 | I semestre | Ugo Solitro | |
| Parte 2 | 3 | I semestre | Gianluigi Bellin |
An introduction to the theory of computability and to computational logic.
Module: Computability.
-------
Introduction.
Automata, languages and grammars. Main results.
Computability.
Algorithms. Models for the effective computations: Turing machines, partial recursive functions, ...
Main results. Church Thesis. Arithmetization and Universality. Unsolvable problems.
Mathematical theory of recursion.
Complexity.
Complexity classes. NP-completeness.
-------------------
Module: Computational Logic.
-------
Representation of proofs and algorithms.
Sequent calculi, cut elimination, semantic tableaux. Intuitionistic Natural Deduction.
Lambda calculus, Church-Rosser property. Representation of partial recursive functions. Simple types and typability.
Curry-Howard correspondence and weak normalization theorem for simply typed lambda calculus. Further advanced topics.
The exam consists in a test for every module and a final oral examination.
| Activity | Author | Title | Publisher | Year | ISBN | Note |
| Parte 1 | Christos H. Papadimitriou | Computational complexity | Addison Wesley | 1994 | 0201530821 | Testo di consultazione |
| Parte 1 | Garey, M. R. and Johnson, D. S. | Computers intractability: a guide to the theory of NP-completeness | Freeman | 1979 | 0-7167-1045-5 | Testo di consultazione |
| Parte 1 | John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman | Introduction to Automata Theory, Languages and Computation (Edizione 2) | Addison-Wesley | 2000 | 0201441241 | Testo di consultazione |
| Parte 1 | H. Rogers | Theory of recursive functions and effective computability | MIT Press | 1988 | Testo di consultazione |
