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.

1° Year

ModulesCreditsTAFSSD
Un insegnamento a scelta
Un insegnamento a scelta
Un insegnamento a scelta

2° Year  activated in the A.Y. 2012/2013

ModulesCreditsTAFSSD
Un insegnamento a scelta (insegnamenti seminariali ad esclusione di Psicologia dell'educazione e Matematica finanziaria)
Un insegnamento a scelta
6
C
MAT/09
Prova finale
32
E
-
ModulesCreditsTAFSSD
Un insegnamento a scelta
Un insegnamento a scelta
Un insegnamento a scelta
activated in the A.Y. 2012/2013
ModulesCreditsTAFSSD
Un insegnamento a scelta (insegnamenti seminariali ad esclusione di Psicologia dell'educazione e Matematica finanziaria)
Un insegnamento a scelta
6
C
MAT/09
Prova finale
32
E
-
Modules Credits TAF SSD
Between the years: 1°- 2°
Altre attivita' formative
4
F
-
Between the years: 1°- 2°

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 John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman Introduction to Automata Theory, Languages and Computation (Edizione 2) Addison-Wesley 2000 0201441241 testo di riferimento

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