Automated Reasoning
2009–10

Principal lecturer: Dr Mateja Jamnik
Taken by: MPhil ACS

• Syllabus



• Recommended textbook available online: Bundy, A. (1983). The Computer Modelling of Mathematical Reasoning. Academic Press, London, UK, Second Edition



• Lecture notes:
  • Lecture 1: Introduction to and History of Automated Reasoning
  
  
  • Lecture 2: Mathematical Logic - Revision (updated!)
  
  
  • Lecture 3: Representation of Mathematical Knowledge (updated!)
  
  
  • Lecture 4: Establishing Correctness by Proof
  
  
  • Lecture 5+: Unification Algorithms and Search for Refutation (updated!)
  
  
  • 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: Some Recent Applications of AR
  
  
  • Lecture 12: Diagrammatic and Heterogeneous Reasoning
  
  
  • Lectures 13-16: Student Presentations
  
  


• Literature survey: below you will find instructions for doing your literature survey with some suggestions of topics. You are welcome to suggest your own topic of automated reasoning that you would like to survey. You need to finalize with the lecturer your choice of topic by 28 January 2010 and submit your literature survey in pdf format via email to the lecturer by 12 March 2010.
  
  • Instructions for literature survey with suggestions of topics
  • Your chosen literature survey topics
  
  
  


• Paper review and presentation: below you will find instructions for doing your paper review and presentation on its content. You should review a research paper from the list of suggested papers at the end of this document, or suggest to the lecturer a conference or a journal paper on a topic in Automated Reasoning of your interest (of length between 8 to 15 pages). You should finalize the choice of a research paper for review and presentation with the lecturer by Thursday, 4 February 2010.
  
  • Instructions for paper review and presentation with suggestions of papers
  
  
  • Paper review form: you should fill this in and hand it to the lecturer immediately prior to your presentation
  
  
  • Anonymous student presentation peer review form
  
  
  • Student presentation evaluation form: the lecturer uses this form to evaluate a student presentation
  
  
  • Presentation timetable