Automated Reasoning (2020-21): The updated AR course materials for 2020-21 will be in LEARN. The contents on this page are for information only and may be removed at any time.

Official course descriptor (Note: a pass in Inf2D is a non-negotiable prerequisite for UG3 students. MSc students should talk to me, if they are unsure about the prerequisites. Do not take this course if you are unfamiliar or uncomfortable with first-order logic and formal reasoning.)

On this page:

Staff
Help and Feedback
Lecture Schedule
Tutorials
Additional Isabelle Exercises
Software
Useful Resources
Assessment and Coursework

The lectures are given by:

Jacques Fleuriot
Email: jdf@inf.ed.ac.uk
Office: IF 2.15 (Informatics Forum)

The Teaching Assistant (TA) is:

Imogen Morris
Email: s1402592@ed.ac.uk

Demonstrator times:

Lab sessions are held in 4.12, Appleton Tower between 09:00 and 11:00 on Mondays, starting in Week 3 Monday 30th September. At each lab session, the course TA is available to help with the course material and coursework. You are strongly encouraged to try the additional Isabelle exercises during the first few labs.

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.

Note: This is a challenging course, which introduces you to novel techniques and skills. You are expected to learn them over a short period of time.

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 and/or the lecturer directly using the details above.

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 in person from the demonstrator. See above for the demonstrator times.
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.

Lecture Schedule

The lectures are held at 14:10-15:00 in Semester 1 on Tuesdays in 1.02, 21 Buccleuch Place, Central Campus and on Thursdays in G.02 - Classroom 2, High School Yards Teaching Centre, Central Campus.

There will be one lecture on the coursework assignment to provide some general information and background. Note: These lectures do not necessarily coincide with the hand-out dates for the assignment sheet. Students should start work on their coursework as soon as they are handed out rather than wait for the lectures, if these come later on.

Please note: At any point of the course, the future schedule gives a strong indication of the topics to be covered. However, some details might change.

Week	Date	Title	Recommended Reading
1	Tue 17th Sep 2019	1. Introduction	Bundy, Ch. 1 [background] Formal Proof by Tom Hales. [background] Logicomix
1	Thu 19th Sep 2019	2. Propositional Logic and Natural Deduction	H&R Sec 1.1, 1.2, 1.3, start of 1.4 [background] Wadler's Propositions as Types
2	Tue 24th Sep 2019	3. Natural Deduction and Starting with Isabelle — Lecture by Petros Papapanagiotou — Isabelle Theory file for Lecture 3	H&R Sec 1.2, 1.4 Sec 5.1-5.7 of Tutorial on Isabelle/HOL (2018) Prop.thy Isabelle theory file
2	Thu 26th Sep 2019	4. Propositional Reasoning in Isabelle	Sec 5.1-5.7 of Tutorial on Isabelle/HOL (2018) [background] Pollack's How to Believe a Machine-Checked Proof [background] How do they verify a verifier of formalized proofs?
3	Tue 1st Oct 2019	5. First-order Logic	H&R Secs 2.1-2.4 FOL.thy Isabelle theory file [background] Logitext - an interactive L-system FOL prover
3	Thu 3rd Oct 2019	6. Representation	Bundy Ch. 4
4	Tue 8th Oct 2019	7. Introduction to Higher Order Logic in Isabelle	Sec 1.1-1.4 of Tutorial on Isabelle/HOL (2018) N&K Sec 2.1-2.2
4	Thu 10th Oct 2019	8. Representation II: Locales in Isabelle/HOL — Isabelle Theory file for Lecture 8	Tutorial on Locales (Isabelle 2018) [background] Interpretation of Locales in Isabelle
5	Tue 15th Oct 2019	9. Isar — A Language for Structured Proofs — Isar Demo Theory	The Isabelle/Isar Quick Reference Manual N&K Ch. 5
5	Thu 17th Oct 2019	10. Coursework: Proving and Reasoning in Isabelle/HOL	See coursework files and coursework slides
6	Tue 22nd Oct 2019	11. Unification	Bundy, Sec 17.1-17.4
6	Thu 24th Oct 2019	12. Rewriting I	Bundy, Ch. 9 Sec 3.1 of Tutorial on Isabelle/HOL (2018)
7	Tue 29th Oct 2019	13. Rewriting II	Bundy, Ch. 9
7	Thu 31st Oct 2019	14. Inductive Proof (in Isabelle)) — Isabelle Theory file for Lecture 14	H&R Sec 1.4.2 [background] The Automation of Mathematical Induction
8	Tue 5th Nov 2019	Coursework Q and A with Teaching Assistant	This will be held as a lab session in Room 7.01, Appleton Tower
8	Thu 7th Nov 2019	15. Program Verification using Hoare Logic (I) — Lecture by Petros Papapanagiotou — Isabelle's Hoare Logic library	H&R Sec 4.1-4.3 N&K Sec 12.2.1 [background] Reading on Hoare Logic (especially pages 1-27, 37-48).
9	Tue 12th Nov 2019	16. Program Verification using Hoare Logic (II) — Lecture by Petros Papapanagiotou — Isabelle Theory file
9	Thu 14th Nov 2019	17. Exam Review	Past papers (Note: Papers before 2016-17 also contain material not in the current course): — 2018-19 — 2017-18 — 2016-17 — 2015-16 — 2014-15 — 2013-14 — 2012-13 — 2011-12 — 2010-11 — 2009-10 — 2008-09
10	Tue 19th Nov 2019	No Lecture
10	Thu 21st Nov 2019	No Lecture

Tutorials

Each tutorial sheet will be released the week before it's due to take place. Solutions will usually be added the week after that of the tutorial.

Week	Title	Solutions
3	Tutorial 1: Propositional logic and some Isabelle
4	Tutorial 2: First order logic and more Isabelle
5	Tutorial 3: Representation and reasoning in Isabelle using locales
6	Tutorial 4: Structured proofs in Isabelle
7	Tutorial 5: Unification and Rewrite Rules
8	Tutorial 6/7: Rewrite Rules, Reasoning about Hoare Logic, Induction [thy]
9	Tutorial 6/7: Rewrite Rules, Reasoning about Hoare Logic, Induction

Additional Isabelle Exercises

These are additional self-help exercises for you to familiarize yourself with theorem proving in Isabelle. Note that some of the statements that you're asked to prove may overlap with those in the tutorials.

Acknowledgement: Some of these originate from an annual Isabelle/HOL lab course taught at the Technische Universität München.

Title	Files	Solutions
Propositional logic	[pdf][thy]
Predicate logic	[pdf][thy]
A riddle: The rich grandfather	[pdf][thy]
A Bad Axiomatization	[pdf][thy]

Software

The Isabelle2018 theorem prover will be used in this course. Isabelle should be installable on your own computer by following the instructions on the linked webpage. Note that Isabelle2019 is probably fine for the purpose of the course but is not supported on DICE yet.
To run Isabelle on the DICE machines in the labs, run the following command from the terminal: Isabelle

Useful Resources

Isabelle Cheat sheet listing common proof commands and rules (note: ignore the references to Proof General). Also available here.
Isar Quick Reference.

Assessment and Coursework

There is one item of assessed coursework for this course, which will count for 40% of the overall mark (the other 60% is assessed by exam).

The deadline for the coursework will be 4pm on the 18th of November 2019. The coursework is described in the files below:

Home : Teaching : Courses