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

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

2° Year  It will be activated in the A.Y. 2026/2027

ModulesCreditsTAFSSD
Final exam
24
E
-
It will be activated in the A.Y. 2026/2027
ModulesCreditsTAFSSD
Final exam
24
E
-
Modules Credits TAF SSD
Between the years: 1°- 2°
2 modules among:
- 1st year - Knowledge representation, Natural Language Processing, HCI - Multimodal Systems - delivered in 2025/2026
- 2nd year - AI & cloud - delivered in 2026/2027
- 1st and 2nd year - Advanced programming for AI, Computer vision & deep learning - delivered in 2025/2026 and in 2026/2027
 
6
B
INF/01
Between the years: 1°- 2°
2 courses among (mutually exclusive with the previous ones):
- 1st year - Knowledge representation, Natural language processing, HCI - multimodal systems - delivered in 2025/2026
- 2nd year - AI & cloud, Visual intelligence - delivered in 2026/2027
- 1st and 2nd year - Advanced programming for AI, Computer Vision & deep learning, Statistical learning - delivered in 2025/2026 and in 2026/2027   
6
C
INF/01
Between the years: 1°- 2°
2 courses among the following
- A.A. 2025/2026 Network Science not activated
- A.A. 2026/2027: Complex Systems not activated
6
C
ING-INF/05
6
C
INF/01 ,ING-INF/05
6
C
INF/01
Between the years: 1°- 2°
Further activities: 3 CFU training and 3 CFU further language skill or 6 CFU training. International students (i.e. students who do not have an Italian bachelor’s degree) must compulsorily gain 3 CFU of Italian language skills (at least A2 level) and 3 CFU training.
6
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

4S010689

Credits

6

Also offered in courses:

Language

English en

Scientific Disciplinary Sector (SSD)

INF/01 - INFORMATICS

Period

1st semester dal Oct 1, 2025 al Jan 30, 2026.

Courses Single

Authorized

Learning objectives

The course covers a range of logics employed in AI, including classical, intuitionistic, modal, epistemic, deontic, and distributed logics, each operating at varying levels of expressivity such as propositional, first-order, and higher-order. Additionally, students explore how logical systems underpin key aspects of computer science relevant to AI, such as the relationships between type systems and programming languages, as well as those between inference systems and interactive or mechanical theorem proving.

By the end of the course, students are expected to demonstrate their ability to:

- Develop formal proofs within the deductive systems covered in class.
- Understand and evaluate the properties of these systems.
- Comprehend how such systems function within reasoning tools like proof assistants, theorem provers, and solvers.

This preparation equips students for further advanced studies or undertaking a thesis in computational logic and AI.

Prerequisites and basic notions

The basic knowledge of logic imparted in the Bachelor's degree in computer science.
It assumes knowledge of propositional logic and natural deduction.
Upon request, the teacher will provide supplementary materials and ad hoc receptions.

Program

1.Propositional logic and its natural deduction system, a short review.
2. Predicate logics: quantifiers, structures semantics, identity, natural deduction, soundness and completeness Theorems
3. Intuitionistic Logic
4. Normalization and confluence in natural deduction.
5. Lambda calculus without types and with types. Lambda calculus as a paradigm for functional programming. Second order lambda calculus.
6. Modal logics

Bibliography

Visualizza la bibliografia con Leganto, strumento che il Sistema Bibliotecario mette a disposizione per recuperare i testi in programma d'esame in modo semplice e innovativo.

Didactic methods

Interactive Frontal teaching/Classroom lecture

Learning assessment procedures

Traditional oral exam on a subset of the topics addressed in class. The list will be built during the course following the lecture notes and the textbook and will be made available on the course Moodle.

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

Evaluation criteria

Knowledge of definitions, results and proofs required. Reasoning skills and evaluation of logical-mathematical competencies.

Criteria for the composition of the final grade

The final grade is the one obtained during the oral exam

Exam language

English for Students enrolled in the LM in Artificial Intelligence; English or Italian for Students enrolled in LM Ingegneria e Scienze Informatiche.