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

A.A. 2024/2025 A.A. 2023/2024 A.A. 2022/2023 A.A. 2021/2022 A.A. 2020/2021 A.A. 2019/2020 A.A. 2018/2019 A.A. 2017/2018 A.A. 2016/2017 A.A. 2015/2016 A.A. 2014/2015 A.A. 2013/2014 A.A. 2012/2013 A.A. 2011/2012 A.A. 2010/2011 A.A. 2009/2010

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 Ingegneria e scienze informatiche - 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 

2° Year   activated in the A.Y. 2021/2022

ModulesCreditsTAFSSD
Final exam
24
E
-
activated in the A.Y. 2021/2022
ModulesCreditsTAFSSD
Final exam
24
E
-
Modules Credits TAF SSD
Between the years: 1°- 2°
12
B
ING-INF/05
Between the years: 1°- 2°
12
B
ING-INF/05
Between the years: 1°- 2°
4 modules among the following
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
Between the years: 1°- 2°
2 modules among the following
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
Between the years: 1°- 2°
3 modules among the following
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
SECS-P/10
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
Between the years: 1°- 2°
English language B2 level
3
F
-
Between the years: 1°- 2°
12
D
-
Between the years: 1°- 2°
Other activities
3
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.

A Basic activities
B Characterizing activities
C Related or complementary activities
D Activities to be chosen by the student
E Final examination
F Other training activities
S Placements in companies, public or private institutions and professional associations

Automated reasoning  (2020/2021)

Teaching code

4S02796

Teacher

Andrea Masini

Coordinator

Andrea Masini

Credits

6

Language

Italian

Scientific Disciplinary Sector (SSD)

INF/01 - INFORMATICS

Period

II semestre dal Mar 1, 2021 al Jun 11, 2021.

Lessons timetable MoodleMoodle Seminars 0

Learning outcomes

The aim of the course is to provide an introduction to the techniques of mechanization of logical reasoning, using tools based on automatic deduction systems or proof assistant systems. Particular importance will be given to the techniques of formalization and mechanical reasoning using goal-driven software systems. At the end of the course students will be able to deal with formalization and automatic verification using either automatic reasoners or proof-assistants. Students will be able to continue their studies in the field of mechanical reasoning, for example by developing master's theses.

Program

Part 1- Foundations
Recalls of natural deduction (classical and intuitionistic)
Simple typed Lambda calculus.
Type checking and type inference.
The system F and the Calculus of Constructions.
Introduction to automatic deduction in propositional logic.
Part 2 - The Coq system
Simple proofs in Coq (Goal, assumptions and tactics).
Functional programming in CoQ.
Structured data types.
Polymorphism and higher order functions.
The tactics.
Logic in CoQ.
Induction and co-induction.

Reference texts
Author Title Publishing house Year ISBN Notes
Bertot, Yves, Castéran, Pierre Interactive Theorem Proving and Program Development Springer-Verlag Berlin Heidelberg 2004 978-3-642-05880-6
Jean Louis Krivine, Rene Cori Lambda-calculus, Types and Models Ellis Horwood 1993 978-0130624079
van Dalen, Dirk Logic and Structure. (Edizione 5) Springer 2013 978-1-4471-4557-8

Examination Methods

Written examination

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