Automated reasoning (2010/2011)

Course code
Name of lecturer
Alessandro Farinelli
Alessandro Farinelli
Number of ECTS credits allocated
Academic sector
Language of instruction
I semestre dal Oct 4, 2010 al Jan 31, 2011.

Lesson timetable

Learning outcomes

The class presents problems, methods and systems for automated reasoning. The class combines theoretical foundations with algorithmic and practical issues, emphasizing mechanization throughout. The student learns how to design, apply and evaluate methods and systems for automated reasoning, focusing on applications such as HW and SW verification, artificial intelligence and robotics.


Automated Reasoning: theorem-proving strategies. Inference Systems, choosing among: instance-based, ordering-based (e.g., resolution, superposition, rewriting), subgoal-reduction (e.g., model elimination). Search Plans. Algorithmic Reasoning in specific domains, choosing among: reasoning under uncertainty; reasoning in multi-agent systems; reasoning procedures for satisfiability modulo theories. Design and use of general-purpose or specific automated reasoners.

Assessment methods and criteria

Partial tests mode: it applies only to the exam sessions right at the end of the class. The exam consists of a written test (partial test)and an individual project to be developed either at home or in the lab. The final grade is given by 50% partial test + 50% project.

Single-test mode: the exam consists of a single written test (exam test), whose difficulty is equivalent to that of the partial test and the project, and whose grade determines alone the final grade. This mode applies to all sessions.

Notes: the partial test is administered on the same date, time and place as the exam test (contents and duration of the partial test and of the exam test will be different).