On this page:
The lectures are given by:
The Teaching Assistant (TA) is:
Demonstrator times:
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
Various kinds of feedback are provided during the course.
Note that there are no lecture notes for the course. Instead, recommended reading is associated with each lecture. This reading is usually from:
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
|
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 | |
Thu 21st Nov 2019 | No Lecture |
Title | Files | Solutions |
---|---|---|
Propositional logic | [pdf][thy] | |
Predicate logic | [pdf][thy] | |
A riddle: The rich grandfather | [pdf][thy] | |
A Bad Axiomatization | [pdf][thy] |
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:
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Logging and Cookies Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh |