Automated reasoning (2010/2011)

Course code
4S02796
Name of lecturer
Alessandro Farinelli
Coordinator
Alessandro Farinelli
Number of ECTS credits allocated
6
Academic sector
INF/01 - INFORMATICS
Language of instruction
Italian
Period
I semestre dal Oct 4, 2010 al Jan 31, 2011.

Lesson timetable

I semestre
Day Time Type Place Note
Monday 4:30 PM - 6:30 PM lesson Lecture Hall I from Oct 25, 2010  to Jan 31, 2011
Tuesday 4:30 PM - 6:30 PM lesson Lecture Hall I  
Friday 11:30 AM - 1:30 PM lesson Lecture Hall B from Oct 22, 2010  to Oct 23, 2010

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.

Syllabus

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).