Department of Computer Science
University of Miami
CSC749 - Automated Reasoning
- Logics, propositional to higher-order
- Reasoning and resolution
- More complex inference rules
- Using contemporary ATP systems
- Encoding problems in logic
- Applications of ATP in research and industry
- 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
Dr Geoff Sutcliffe.
Contact details are on the WWW at
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.
- Section H - Monday, Wednesday 3:35-4:50pm, Ungar 330G.
There is no required text.
will be available on the WWW.
In order to obtain a particular grade, you may be required to attain
that grade in all items of assessment.
|| Using ATP tools
|| Encoding and solving a problem
|| Implementing an ATP system in Prolog
|| Midterm test (2nd October, in class)
|| Final exam (2:00-4:3-pm, 11th December)
Assignments will be placed on the WWW.
The submission requirements for each assignment will be given with each
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