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.
Lectures are held in Semester 1 on:
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 handout 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 19th Sep 2017  1. Introduction  Bundy, Ch. 1 [background] Formal Proof by Tom Hales. [background] Logicomix 
Fri 22nd Sep 2017  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 26th Sep 2017  3. Natural Deduction and Starting with Isabelle
— Isabelle Theory file for Lecture 3 
H&R Sec 1.2, 1.4 Sec 5.15.7 of Tutorial on Isabelle/HOL Prop.thy Isabelle theory file 
Fri 29th Sep 2017  4. Propositional Reasoning in Isabelle

Sec 5.15.7 of Tutorial
on Isabelle/HOL [background] Pollack's How to Believe a MachineChecked Proof [background] How do they verify a verifier of formalized proofs? 

3  Tue 3rd Oct 2017  5. Firstorder Logic

H&R Secs 2.12.4
FOL.thy Isabelle theory file [background] Logitext  an interactive Lsystem FOL prover 
Fri 6th Oct 2017  6. Representation 
Bundy Ch. 4  
4  Tue 10th Oct 2017  7. Introduction to Higher Order Logic in Isabelle 
Sec 1.11.4 of Tutorial
on Isabelle/HOL N&K Sec 2.12.2 
Fri 13th Oct 2017  8. Representation II: Locales in Isabelle/HOL — Isabelle Theory file for Lecture 8 
Tutorial on Locales [background] Interpretation of Locales in Isabelle 

5  Tue 17th Oct 2017  9. Coursework: Proving and Reasoning in Isabelle/HOL  See coursework files 
Fri 20th Oct 2017  10. Isar — A Language for
Structured Proofs — Isar Demo Theory 
The Isabelle/Isar Quick
Reference
Manual N&K Ch. 5 

6  Tue 24th Oct 2017  11. Program Verification using Hoare Logic (TBC) — Lecture by Petros Papapanagiotou — Isabelle's Hoare Logic library 
H&R Sec 4.14.3 N&K Sec 12.2.1 [background] Reading on Hoare Logic (especially pages 127, 3748). 
Fri 27th Oct 2017  12. Guest Lecture (TBC)  
7  Tue 31st Oct 2017  13. Unification  Bundy, Sec 17.117.4 
Fri 3rd Nov 2017  14. Rewriting I  Bundy, Ch. 9 Sec 3.1 of Tutorial on Isabelle/HOL 

8  Tue 7th Nov 2017  15. Rewriting II  Bundy, Ch. 9 
Fri 10th Nov 2017  16. Inductive Proof (in Isabelle) — Isabelle Theory file for Lecture 6 
H&R Sec 1.4.2 [background] The Automation of Mathematical Induction 

9  Tue 14th Nov 2017  17. AR Assignment lecture Q&A  
Fri 17th Nov 2017  18. Exam Review 
Past papers (Note: these also contain material not in the current course): — 201516 — 201415 — 201314 — 201213 — 201112 — 201011 — 200910 — 200809 

10  Tue 21st Nov 2017  19. TBC  
Fri 24th Nov 2017  20. TBC 
Title  Files 

Propositional logic  [pdf][thy] 
Predicate logic  [pdf][thy] 
A riddle: The rich grandfather  [pdf][thy] 
A Bad Axiomatization  [pdf][thy] 
There will be 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 dates for the coursework are as follows:
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, Email: schooloffice@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 