Department of Computer Science
University of Miami

CSC648 - Automated Reasoning

Spring 2012

Description

Learning Objectives

  1. Understand the principles of reasoning in 1st order logic
  2. Understand and be able to use basic and complex inference rules
  3. Be able to implement a simple ATP system in Prolog
  4. Be able to encode sample problems into 1st order logic
  5. Be able to use contemporary ATP systems
  6. Understand current applications of ATP

Instructor

Dr Geoff Sutcliffe. Contact details are on the WWW at http://www.cs.miami.edu/~geoff.

Contact Hours

Students are welcome to come see me whenever I'm on campus. Students are encouraged to ask questions by email at all times. Students are required to read their email regularly, and to consult the course WWW page regularly.

Resource materials

There is no required text. Course content and the assignments will be available on the WWW.

Assessment

10% Using ATP tools
20% Encoding and solving a problem
20% Implementing an ATP system in Prolog
10% Midterm test (8th March, in class)
40% Final exam (11:00am-1:30pm, 9th May)
In order to obtain a particular grade, you may be required to attain that grade in all items of assessment.

Assignments will be placed on the WWW. The submission requirements for each assignment will be given with each assignment. Late submissions will not be accepted. Extensions of the due date will be granted if supporting documentary evidence is supplied (e.g., a doctor's certificate). Application for an extension must be made to the instructor before the due date (if possible).

Assessment items must be completed individually. While general interaction between students is encouraged, plagiarism is considered to be a serious offence. It is ok to talk to other students about general solution techniques for assignments, but it is not ok to copy solutions in part or as a whole. Plagiarism will result in a loss of marks for all guilty students involved.