AR: Automated Reasoning
Welcome to Automated Reasoning
I hope you won't mind if we start with a warning. As much as we would love for all of you to find this course a great fit, please note the following:
This is a challenging course that introduces you to novel techniques and skills. You are expected to learn them over a short period of time. So, we strongly advise you to engage with the course materials, discussion forum and instructors right from the start. Ask questions early and often, and do attend the drop-in labs too for hands-on help with Isabelle!
You can browse the course materials as follows:
- Lecture Schedule: the day and times the lectures will take place and how to join them, a schedule for each week including the lecture slides, recommended reading, and quizzes, and a link to the protocol for the lectures.
- Self-help Exercises: the exercises to be completed in your own time to enable you to practice theorem proving in Isabelle and, more generally gain a deeper understanding of the course contents.
- Piazza: a place for you discuss the course with your instructors and your fellow classmates questions. You can ask questions you have regarding the lectures, exercises, coursework and even the optional material!
- Assessment: upon release this page will be populated with information pertaining to the coursework, which will be released on Learn.
- Course Contacts: contact information for the Course Lecturer, Teaching Assistant and Demonstrator.
Help and feedback
If you run into difficulties and are not making satisfactory progress then seek help. The earlier you ask for help the more likely it is that your problems can be solved without damaging your performance in the course.
To seek help
- post questions on the class discussion forum (preferred),
- use the course mailing list ar-students@inf.ed.ac.uk,
- contact the TA(s) and/or the lecturer(s) directly.
Various kinds of feedback are provided during the course.
- Formative feedback including best practices and ways to hone and further develop the taught skills will be provided throughout the lectures.
- You can receive feedback on your progress in the coursework from the demonstrator(s).
- You will also receive your coursework marks and written, individual feedback by personal email. This will include formative feedback aimed at helping you in similar tasks, coursework, and exams in the future.
- Feedback and marks on each the coursework will be provided within 2 weeks (10 working days) from the coursework submission date.
- Feel free to seek help and request extra or other types of feedback by contacting the course TA and/or lecturer.
Note that there are no lecture notes for the course. Instead, recommended reading is associated with each lecture. This reading is usually from:
- T. Nipkow and G. Klein. Concrete Semantics with Isabelle/HOL, Springer, 2014 (N&K).
- J. Harrison. Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009.
- M. Huth and M. Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Edition, Cambridge University Press, 2004 (H&R).
- A. Bundy, The Computational Modelling of Mathematical Reasoning, Academic Press 1983 (Bundy). This book is out of print, but is available online.
Learning Outcomes
On successful completion of this course, you should be able to:
- Use sophisticated mechanisms available in theorem provers to represent problem.
- Write interactive proof in procedural and declarative styles.
- Use interactive and automated methods to carry out proofs in the theorem prover.
- Represent and reason about mathematical and other less formal knowledge using logic.
- Understand and compare automated reasoning techniques and apply them using pen-and-paper.
Course Outline
The course starts with an introduction to higher order logic, theorem provers and, more specifically, Isabelle/HOL. This will set the context for the rest of the course in which Isabelle will be the framework for getting hands-on experience about the application of various theoretical concepts.
Through the lectures and weekly exercises that incorporate practical aspects the students will gain the skills needed to get started with Isabelle and progress to more complex concepts involving both representation and reasoning.
The second part will look at representation/modelling of concepts in (higher order) logic in details. Axiomatic versus conservative extensions of theories will be covered and mechanisms such as Isabelle locales will be introduced and used. Recursive definitions and inductive notions will be covered too.
The third part of the course will focus on fundamental notions such as unification and rewriting, within both a first and higher order context. It will look at notions such as termination and use Isabelle's simplifier as the tool for understanding many of the concepts. It will also look at the interplay between (fully) automatic and interactive proofs.
The fourth part will introduce declarative/structured proofs and using the Isar language of Isabelle show how proofs resembling pencil and paper ones can be formalized.
Finally the various strands will be brought together through the discussion of a non-trivial case study. This may involve either formalized mathematics (e.g. looking at a geometric theory) or a formal verification example.
The assignment will be a combination of basic to intermediate representation and reasoning in Isabelle (up to 40%), more advanced proof tackling one particular domain or example (up to 40%) and a final part which, if completed successfully, will clearly demonstrate that the student has a good grasp of the challenges that advanced interactive theorem proving entails.