Department of Computer Science
University of Miami

CSC749 - Automated Reasoning

Fall 2017


Learning Objectives

  1. Understand the principles of reasoning in 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 logic
  5. Be able to use contemporary ATP systems
  6. Understand current applications of ATP


Dr Geoff Sutcliffe. Contact details are on the WWW at

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.


10% Using ATP tools
20% Encoding and solving a problem
20% Implementing an ATP system in Prolog
10% Midterm test (2nd October, in class)
40% Final exam (3:35-4:50pm, 18th December)
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.