Course pages 2012–13

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: Student Presentations
• Lecture 14: Student Presentations
• Lecture 15: Student Presentations
• Lecture 16: Student Presentations

Literature survey:

here is more information.

Paper review and presentation:

here is more information.

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