Department of Computer Science
University of Miami
CSC749  Automated Reasoning
Fall 2017
Description
 Logics, propositional to higherorder
 Reasoning and resolution
 More complex inference rules
 Using contemporary ATP systems
 Encoding problems in logic
 Applications of ATP in research and industry
Learning Objectives
 Understand the principles of reasoning in logic
 Understand and be able to use basic and complex inference rules
 Be able to implement a simple ATP system in Prolog
 Be able to encode sample problems into logic
 Be able to use contemporary ATP systems
 Understand current applications of ATP
Instructor
Dr Geoff Sutcliffe.
Contact details are on the WWW at
http://www.cs.miami.edu/~geoff.
Contact Hours
 Section H  Monday, Wednesday 3:354:50pm, Ungar 330G.
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 (2nd October, in class)

40%
 Final exam (2:004:3pm, 11th 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.