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.

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/2026

The 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.

CURRICULUM TIPO:

1° Year 

ModulesCreditsTAFSSD
Insegnamenti offerti ad anni alterni
Insegnamenti offerti ad anni alterni
ModulesCreditsTAFSSD
Insegnamenti offerti ad anni alterni
Insegnamenti offerti ad anni alterni
Modules Credits TAF SSD
Between the years: 1°- 2°
Between the years: 1°- 2°
Ulteriori competenze
4
F
-

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.




S Placements in companies, public or private institutions and professional associations

Teaching code

4S02855

Credits

6

Coordinator

Ugo Solitro

Language

Italian

Scientific Disciplinary Sector (SSD)

INF/01 - INFORMATICS

The teaching is organized as follows:

Parte 2

Credits

3

Period

I semestre

Academic staff

Gianluigi Bellin

Parte 1

Credits

3

Period

I semestre

Academic staff

Ugo Solitro

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

Reference texts
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.

Students with disabilities or specific learning disorders (SLD), who intend to request the adaptation of the exam, must follow the instructions given HERE