Studying at the University of Verona
Here you can find information on the organisational aspects of the Programme, lecture timetables, learning activities and useful contact details for your time at the University, from enrolment to graduation.
Study Plan
This information is intended exclusively for students already enrolled in this course.If you are a new student interested in enrolling, you can find information about the course of study on the course page:
Laurea magistrale in Mathematics - Enrollment from 2025/2026The Study Plan includes all modules, teaching and learning activities that each student will need to undertake during their time at the University.
Please select your Study Plan based on your enrollment year.
1° Year
Modules | Credits | TAF | SSD |
---|
2° Year activated in the A.Y. 2011/2012
Modules | Credits | TAF | SSD |
---|
Due tra i seguenti insegnamenti
Modules | Credits | TAF | SSD |
---|
Modules | Credits | TAF | SSD |
---|
Due tra i seguenti insegnamenti
Modules | Credits | TAF | SSD |
---|
Legend | Type of training activity (TTA)
TAF (Type of Educational Activity) All courses and activities are classified into different types of educational activities, indicated by a letter.
Mathematics methods for computer science (2011/2012)
Teaching code
4S02855
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
The teaching is organized as follows:
Parte 2
Parte 1
Learning outcomes
An introduction to the theory of computability and to computational logic.
Program
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.
Bibliography
Activity | Author | Title | Publishing house | Year | ISBN | Notes |
---|---|---|---|---|---|---|
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 |
Examination Methods
The exam consists in a test for every module and a final oral examination.