Course pages 2015–16

# Automated Reasoning

### Lecture notes

- Lecture 1: Introduction to and History of Automated Reasoning
- Lecture 2: Mathematical Logic - Revision
- Lecture 3: Representation of Mathematical Knowledge
- Lecture 4: Establishing Correctness by Proof
- Lectures 5 and 6: Unification Algorithms and Search for Refutation
- Lecture 7: Rewrite Rules
- Lecture 8: Decision Procedures
- Lecture 9: Mathematical Induction
- Lecture 10: Proof Planning and Rippling - Heuristic Guidance for Inductive Proof
- Lecture 11: Application of AR in Ontologies/Semantic Web
- Lecture 12: Application of AR in Diagrammatic and Heterogeneous Reasoning

### Literature survey:

### Paper review and presentation:

### Exercises:

- Exercises for lecture 2 on mathematical logic
- Exercises for lecture 3 on mathematical knowledge representation
- Exercises for lecture 4 on establishing correctness by proof
- Exercises for lectures 5 and 6 on unification algorithms and search
- Exercises for lecture 7 on rewrite rules
- Exercises for lecture 8 on decision procedures
- Exercises for lecture 9 on mathematical induction
- Exercises for lecture 10 on proof planning and rippling
- Exercises for lecture 11 on ontologies
- Exercises for lecture 12 on diagrammatic and heterogeneous reasoning