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
Queste informazioni sono destinate esclusivamente agli studenti e alle studentesse già iscritti a questo corso. Se sei un nuovo studente interessato all'immatricolazione, trovi le informazioni sul percorso di studi alla pagina del corso:
Laurea magistrale in Ingegneria e scienze informatiche - Immatricolazione dal 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.
1° Year
| Modules | Credits | TAF | SSD |
|---|
2° Year activated in the A.Y. 2020/2021
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
2 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.
Automated reasoning (2019/2020)
Teaching code
4S02796
Teacher
Coordinator
Credits
6
Language
Italian
Scientific Disciplinary Sector (SSD)
INF/01 - INFORMATICS
Period
I semestre dal Oct 1, 2019 al Jan 31, 2020.
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. The 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 and assignments (SMT/SMA). Combination of theories. Implementation of a prover or solver as individual project.
| 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 | |
| John Harrison | Handbook of Practical Logic and Automated Reasoning (Edizione 1) | Cambridge University Press | 2009 | 9780521899574 | |
| 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% PI + 25% PF + 50% P, where PI is the midterm exam, PF 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.
