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

Learning Objectives

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

Instructor

Teaching Assistant

Parniyan Farvardin

Contact Hours

• Section S - Tuesday, Thursday 3:30-4:45pm, Ungar 305.
• In Zoom: https://miami.zoom.us/j/92841727097
• See the instructor's web page for office hours.
• Parniyan has office hours TBA, in UB310T and in Zoom.
• Students are encouraged to ask questions by email at all times.
• Students are required to read their email regularly, and to consult the course web page regularly.

Resource materials

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.