Automated reasoning (2009/2010)

Course code
4S02796
Name of lecturer
Alessandro Farinelli
Coordinator
Alessandro Farinelli
Number of ECTS credits allocated
6
Other available courses
Academic sector
INF/01 - INFORMATICS
Language of instruction
Italian
Period
1st Semester dal Oct 1, 2009 al Jan 31, 2010.
Web page
http://profs.sci.univr.it/~farinelli/courses/ar2009/ar2009.html

Lesson timetable

1st Semester
Day Time Type Place Note
Thursday 10:30 AM - 12:30 PM lesson Lecture Hall C from Oct 8, 2009  to Jan 31, 2010
Friday 11:30 AM - 1:30 PM lesson Lecture Hall C from Oct 9, 2009  to Jan 31, 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).