Course pages 2013–14

# 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
- Lecture 5+: Unification Algorithms and Search for Refutation
- Lecture 6: Limitations of Uniform Proof Procedures
- 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
- Lecture 13: Revision/Exercise Class
- Lectures 14-16: Student Presentations

### 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 lecture 5 on unification algorithms and search
- Exercises for lecture 6 on limitation of uniform proof procedures
- 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