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
| Modules | Credits | TAF | SSD |
|---|
2° Year It will be activated in the A.Y. 2026/2027
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
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
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 2 courses among the following
- A.A. 2025/2026 Network Science not activated
- A.A. 2026/2027: Complex Systems not activated1 course 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.
Automated reasoning (2025/2026)
Teaching code
4S013604
Teacher
Coordinator
Credits
6
Language
English
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
1st semester dal Oct 1, 2025 al Jan 30, 2026.
Courses Single
Authorized
Learning objectives
The class presents a selection of inference systems, search plans, and transition systems for automated theorem proving and satisfiability modulo theories and assignments. The students learn how to design, apply, and evaluate algorithms, procedures, and strategies for problems formulated as validity or satisfiability queries. At the end of the course the students master the main automated reasoning methods, know how to choose the most appropriate method for a given problem, and are prepared to apply automated reasoning to provide artificial intelligence in a variety of application fields.
Prerequisites and basic notions
Undergraduate-level knowledge of programming, algorithms, and first-order logic.
Program
Inference systems and search plans for theorem-proving strategies in first-order logic. Ordering-based (resolution and paramodulation/superposition), instance-based, or subgoal-reduction (linear resolution) theorem-proving strategies. Transition systems and search plans for SMT solving: first-order theories, decision procedures for the quantifier-free fragment of first-order theories, theory combination.
Bibliography
Didactic methods
Lectures, exercises, independent individual programming project.
Learning assessment procedures
First round: two written tests (midterm and final) and an independent individual programming project.
Later rounds: written exam.
Evaluation criteria
Correctness and completeness of solutions; correctness, usability, and quality of documentation for the project.
Criteria for the composition of the final grade
1st round: 25% PI + 25% PF + 50% P where PI is the grade in the midterm written test, PF is the grade in the final written test, and P is the grade in the project.
Later rounds: 100%E where E is the grade in the written test.
Exam language
Inglese
Sustainable Development Goals - SDGs
This initiative contributes to the achievement of the Sustainable Development Goals of the UN Agenda 2030. More information on sustainability
