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