On this page:
The lectures will be given by Robert Atkey. Email: bob.atkey@ed.ac.uk. Room IF5.28.
Demonstrator times: the course lecturer will be available in AT5.05 (the west computer lab on Level 5 of Appleton Tower) between 2pm and 4pm on Thursdays and Fridays to help with any problems with course material and coursework.
Note: There are no lab sessions on Thursday 19th and Friday 20th. Instead there will be lab sessions, in the usual place, between 2pm and 4pm on Tuesday 17th February and Monday 23rd February.
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. You can contact the lecturer using the details above. You can also ask questions on the course mailing list arstudents@inf.ed.ac.uk.
Do not be ashamed of asking for help. This is a challenging course, which introduces you to novel techniques and skills. You are expected to learn them during the course, not to come already equipped with them.
Lectures are held at 16.1017.00 in Semester 2 on Tuesdays and Fridays in Lecture Theatre 3 of 7 Bristo Square.
The first lecture is on Tuesday 13th January 2015.
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 each of the coursework assignments to provide some general information and background. Note: These lectures do not necessarily coincide with the handout dates for the assignment sheets. Students should start work on their courseworks 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 13th Jan 2015  1. Introduction  Bundy, Ch. 1 [background] The Univalent Foundations presentation by Vladimir Voevodsky. [background] Logicomix 
Fri 16th Jan 2015  2. Propositional Logic and Natural Deduction
—Exercises —Solutions 
H&R Sec 1.1, 1.2, 1.3, start of 1.4 [background] Wadler's Propositions as Types 

2  Tue 20th Jan 2015  3. Natural Deduction and Starting with Isabelle
—Exercises —Solutions 
H&R Sec 1.2, 1.4 Getting Started with Isabelle Sec 5.15.7 of Tutorial on Isabelle/HOL Prop.thy Isabelle theory file 
Fri 23rd Jan 2015  4. Propositional Reasoning in Isabelle
—Exercises —Solutions 
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 27th Jan 2015  5. Firstorder Logic
—Exercises —Solutions 
H&R Secs 2.12.4
FOL.thy Isabelle theory file [background] Logitext  an interactive Lsystem FOL prover 
Fri 30th Jan 2015  6. Representation & Introduction to HOL — Exercises — Solutions 
Bundy Ch. 4  
4  Tue 3rd Feb 2015  7. Coursework 1: Proving and Reasoning in Isabelle/HOL — Coursework description — Coursework theory file 
[background] Some Theorems on Deducibility: the original paper on quantifier elimination for DLOs, from 1927. [background] Linear Quantifier Elimination contains a more efficient QE procedure for DLOs (and linear arithmetic). 
Fri 6th Feb 2015  8. Unification — Exercises — Solutions 
Bundy 17.1  17.4 [background] Unification theory  a survey of the state of the art from 2001. 

5  Tue 10th Feb 2015  9. Rewriting — Exercises — Solutions 
Bundy Ch. 9 
Fri 13th Feb 2015  10. Inductive proofs (in Isabelle) — Exercises — Solutions 
Bundy Ch. 11 [background] Productive Use of Failure in Inductive Proof 

Tue 16th Feb 2015  Innovative Learning Week (no lecture)  
Fri 20th Feb 2015  Innovative Learning Week (no lecture)  
6  Tue 24th Feb 2015  11. Introduction to Model checking and Linear Temporal Logic  H&R Sections 3.1, 3.2 
Fri 27th Feb 2015  12. Linear Temporal Logic, continued  H&R Section 3.2  
7  Tue 3rd Mar 2015  13. The NuSMV model checker — Coursework Description 
H&R Section 3.3 NuSMV Startup Guide 
Fri 6th Mar 2015  14. Coursework 2  
8  Tue 10th Mar 2015  15. Computation Tree Logic  H&R Sections 3.4 and 3.5 
Fri 13th Mar 2015  16. LTL Model Checking Idea  H&R Sections 3.6.2 and 3.6.3  
9  Tue 17th Mar 2015  17. CTL Model Checking  H&R Sections 3.6.1 and 3.7 
Fri 20th Mar 2015  18. TBD  
10  Tue 23rd Mar 2015  19. Introduction to BDDs  H&R Section 6.1 
Fri 27th Mar 2015  20. Operations on BDDs  H&R Sections 6.2, 6.3  
11  Tue 31st Mar 2015  21. TBD  
Fri 3rd Apr 2015  22. No Lecture 
There are two pieces of software that we will be using for this course.
The Isabelle20132 theorem prover. This is a release behind the current version (Isabelle2014). Isabelle should be installable on your own computer by following the instructions on the linked webpage.
To run Isabelle on the DICE machines in the labs, run one of the following two commands from the terminal:
~ratkey2/Isabelle20132/bin/isabelle emacs
or
~ratkey2/Isabelle20132/bin/isabelle jedit
The first command will start the Emacs/Proofgeneral interface. The second command will start the JEdit interface.
More information about using Isabelle is available in the Isabelle Startup Guide.
There is also a Cheat sheet listing common Isabelle proof commands and rules.
There will be two items of assessed coursework for this course, both of which count for 20% of the overall mark (the other 60% is assessed by exam).
The dates for the coursework are as follows:
The first coursework overlaps with Innovative Learning Week, which accounts for the longer elapsed time between hand out and deadline.
The first coursework was handed out on 3rd February 2015. The deadline is 2pm, Friday 27th February 2015.
The second coursework was handed out on 3rd March 2015. The deadline is 2pm, Friday 20th March 2015.
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 