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 Ingegneria e scienze informatiche - 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 |
|---|
4 modules among the following2° Year activated in the A.Y. 2024/2025
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
4 modules among the following| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
2 modules among the following3 modules among the followingLegend | 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.
Interactive Theorem Proving (2023/2024)
Teaching code
4S010508
Teacher
Coordinator
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
Semester 2 dal Mar 4, 2024 al Jun 14, 2024.
Courses Single
Authorized
Learning objectives
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.
Prerequisites and basic notions
Elements of Mathematical Logic
Program
BHK-interpretation
Propositional Logic in the Coq system
First-order Logic in the Coq system
Dependent Type Theory in the Coq system
Induction and co-induction
Polymorphism
Case-studies
Bibliography
Didactic methods
Frontal and interactive lessons
Learning assessment procedures
To pass the exam, a project must be carried out which will be awarded one month before the first exam. Each project can be carried out by a group of one or two people. The project must be written in Coq (with the code properly commented) and be accompanied by a report of a few pages. Each project can be made using the constructs and tactics seen in class. Any construct and tactics used and not explained in class must be explained in the accompanying report. The exam will consist of an oral exam in which the project carried out will be discussed.
Evaluation criteria
The following will be evaluated:
1) the realization of the project;
2) the oral presentation of the project.
Criteria for the composition of the final grade
The final grade will be based on how the project was carried out and on how the examiners will answer the questions during the oral presentation.
Exam language
Italiano/Inglese
