Course pages 2011–12

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