Department of Computer Science
University of Miami
CSC506 - Logic and Automated Reasoning
CSC749 - Automated Reasoning
Fall 2024
Description
- Logics, propositional to higher-order
- Encoding problems in logic
- Using contemporary ATP systems
- Reasoning and resolution
- More complex inference rules
- Theoretical and practical boundaries
- Implementation of an ATP system in Prolog (not for CSC506)
Learning Objectives
- Understand the principles of reasoning in logic
- Be able to encode sample problems into logic
- Be able to use contemporary ATP systems
- Understand and be able to use basic and complex inference rules
- Be aware of the theoretical and practical boundaries of reasoning in logic
- Be able to implement a simple ATP system in Prolog (not for CSC506)
Instructor
Dr Geoff Sutcliffe.
Contact details are on the WWW at
http://www.cs.miami.edu/~geoff.
Contact Hours
- Section P - Tuesday, Thursday 11:00am-12:15pm, UB330G.
- In Zoom: https://miami.zoom.us/j/92841727097
Students are required to read their email regularly, and to consult the course WWW page regularly.
Students are encouraged to ask questions by email at all times.
Students are welcome to come see me whenever I'm on campus and not crazy busy.
I'm also happy to chat in Zoom - just schedule a time by email.
Resource materials
There is no required text.
Course content
and the
assignments
will be available on the WWW.
Assessment
| 15%
| Using ATP tools
|
| 20%
| Encoding and solving a problem
|
| 25% (CSC749)
| Implementing an ATP system in Prolog
|
| 25% (CSC506)
| Second encoding project
|
| 15%
| Midterm test (After "Heuristics", in class 17th October)
|
| 25%
| Final theory exam (11:00am-1:30pm, 10th December)
|
In order to obtain a particular grade, you might be required to attain that grade in all items
of assessment.
Assignments will be placed on the web.
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 a breach of the
Honor code.
The university requires faculty to report all instances of academic integrity violations:
Faculty must immediately report the suspected violation to the
Department Chair (or relevant administrator in the non-departmentalized
schools) and complete the online Academic Integrity Reporting Form. The
Department Chair will immediately inform the Academic Dean for
Undergraduate Studies of the school.
See the
Students Rights and Responsibilities Handbook.
That really means ...
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 and/or fingers for all guilty students involved.