Automated Reasoning
Delivery
Lectures will be delivered in person. If the lecturer needs to self-isolate, they will be streamed live. If any student needs to self-isolate, lectures will still be delivered in person and also streamed and recorded.
The link to the Zoom live streaming can be found on the L18 Course Moodle web page.
The recordings of the lectures can also be found on the L18 Course Moodle web page.
Lecture notes
- Lecture 1: Introduction to and History of Automated Reasoning
- Lecture 2: Mathematical Logic - Revision
- Lecture 3: Representation of Mathematical Knowledge
- Lectures 4 and 5: Establishing Correctness by Proof
- Lectures 5, 6 and 7: Unification Algorithms and Search for Refutation
- Lecture 8: Rewrite Rules
- Lecture 9: Decision Procedures
- Lecture 10: Mathematical Induction
- Lecture 11: Proof Planning and Rippling - Heuristic Guidance for Inductive Proof
- Lecture 12: Application of AR in Ontologies/Semantic Web
- Lecture 13: Application of AR in Diagrammatic and Heterogeneous Reasoning
- Lecture 14: Student Presentations
- Lecture 15: Student Presentations
- Lecture 16: Student Presentations
Literature survey/critical analysis:
Paper review and presentation:
Exercises:
- Exercises for lecture 2 on mathematical logic
- Exercises for lecture 3 on mathematical knowledge representation
- Exercises for lectures 4 and 5 on establishing correctness by proof
- Exercises for lectures 5, 6 and 7 on unification algorithms and search
- Exercises for lecture 8 on rewrite rules
- Exercises for lecture 9 on decision procedures
- Exercises for lecture 10 on mathematical induction
- Exercises for lecture 11 on proof planning and rippling
- Exercises for lecture 12 on ontologies
- Exercises for lecture 13 on diagrammatic and heterogeneous reasoning