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 

ModulesCreditsTAFSSD
12
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
C
INF/01

2° Year   activated in the A.Y. 2019/2020

ModulesCreditsTAFSSD
6
B
INF/01
6
B
ING-INF/05
Other activities
4
F
-
Final exam
24
E
-
ModulesCreditsTAFSSD
12
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
C
INF/01
activated in the A.Y. 2019/2020
ModulesCreditsTAFSSD
6
B
INF/01
6
B
ING-INF/05
Other activities
4
F
-
Final exam
24
E
-
Modules Credits TAF SSD
Between the years: 1°- 2°
2 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
SECS-P/10
6
C
INF/01
6
C
INF/01
6
C
FIS/01
Between the years: 1°- 2°
8
D
-

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  (2018/2019)

Teaching code

4S02796

Teacher

Maria Paola Bonacina

Coordinator

Maria Paola Bonacina

Credits

6

Language

Italian

Scientific Disciplinary Sector (SSD)

INF/01 - INFORMATICS

Period

I semestre dal Oct 1, 2018 al Jan 31, 2019.

Lessons timetable MoodleMoodle Seminars 0

Learning outcomes

The class aims at providing knowledge about the following topics:
a) methods for theorem proving and model building;
b) inference systems based on orderings (resolution), instance generation, sub-goal reduction (tableaux);
c) search plans;
d) decision procedures for propositional satisfiability (SAT) and satisfiability modulo theories (SMT).
At class' end the student will have to show her capacity to understand inference systems, search plans, and decision procedures, and evaluate them in terms of soundness, completeness and efficiencly, also via the implementation of a prototype. These skills will allow her to use existing resoners, develop new ones, and choose one appropriate for a problem or application. At class' end the student will be prepared to continue her studies or develop a master thesis in automated reasoning or artificial intelligence.

Program

Foundations of automated reasoning: theorem proving and model building. The problem of propositional satisfiability (SAT): the DPLL and CDCL procedures. The problem of validity in first-order logic: inference systems and search plans. Herbrand theorem. Instance-based inference systems: hyper-linking. Ordering-based inference systems: resolution and paramodulation/superposition. Subgoal-reduction based inference systems: model elimination, tableaux. Search plans: the given-clause algorithm; depth-first search with iterative deepening. Decision procedures for satisfiability modulo theories (SMT). Constraint reasoning. Design and use of general-purpose or special-purpose reasoners.

Reference texts
Author Title Publishing house Year ISBN Notes
Daniel Kroening, Ofer Strichman Decision Procedures. An algorithmic point of view Springer 2008 978-3-540-74104-6
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509
Aaron R. Bradley, Zohar Manna The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) Springer 2007 9783540741
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821
Martin Davis The Universal Computer. The Road from Leibniz to Turing. Turing Centenary Edition. Taylor and Francis Group 2012 978-1-4665-0519-3

Examination Methods

First round: the grade is given by 25% C1 + 25% C2 + 50% P, where C1 is the midterm exam, C2 is the final exam, and P is a project.
Later rounds: the grade is given by 100% E, where E is a written exam, as hard as midterm, final, and project combined.
Attending all classes is crucial, however the exam rules are the same regardless of whether one attends or not.
All grades will be registered; it is possible to withdraw by informing the instructor.

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