Automated Reasoning (201718): This course is being updated
 Official course descriptor (Note: a pass in Inf2D is a nonnegotiable prerequisite. Do not take this course if you are unfamiliar or uncomfortable with firstorder logic and formal reasoning.)
On this page:
The lectures are given by:
The Teaching Assistant (TA) is:
Demonstrator times:

Lab sessions are held in 5.05  West Lab, Appleton Tower
between 09:00 and 11:00 on Mondays, starting in Week 3 (start date to be confirmed).
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.
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.
 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.
The lectures are held at 15:1016:00 in Semester 1 on:
 Tuesdays: 7 Bristo Square, Room 1.204.
 Fridays: Dugald Stewart Building, Room 1.20.
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 (20161)
Prop.thy Isabelle theory file

Fri 29th Sep 2017 
4. Propositional Reasoning in Isabelle

Sec 5.15.7 of Tutorial
on Isabelle/HOL (20161)
[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 (20161)
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 (Isabelle 20161)
[background] Interpretation of Locales in Isabelle

5 
Tue 17th Oct 2017 
9. Isar — A Language for
Structured Proofs
— Isar Demo Theory

The Isabelle/Isar Quick
Reference
Manual
N&K Ch. 5

Fri 20th Oct 2017 
10. Coursework: Proving and Reasoning in Isabelle/HOL

See coursework files

6 
Tue 24th Oct 2017 
11. Unification

Bundy, Sec 17.117.4 
Fri 27th Oct 2017 
12. Rewriting I 
Bundy, Ch. 9
Sec 3.1 of Tutorial
on Isabelle/HOL (20161)

7 
Tue 31st Oct 2017 
13. Rewriting II 
Bundy, Ch. 9

Fri 3rd Nov 2017 
14. The ACL2 Theorem Prover and How it Came to be Used in Industry
— Guest Lecture/Talk by J Strother Moore
— Venue: Informatics Forum, Room 4.33

— Talk Abstract
— Speaker's Bio
— Session logs for the demos
— ACL2 web page

8 
Tue 7th Nov 2017 
15. Program Verification using Hoare Logic (I)
— 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 10th Nov 2017 
16. Program Verification using Hoare Logic (II)
— Lecture by Petros Papapanagiotou
 
9 
Tue 14th Nov 2017 
17. Inductive Proof (in Isabelle)
— Isabelle Theory file for Lecture 17

H&R Sec 1.4.2
[background] The
Automation of Mathematical Induction 
Fri 17th Nov 2017 
18. No Lecture 

10 
Tue 21st Nov 2017 
19. Exam Review 
Past papers (Note: Papers before 201617 also contain material not in the current course):
— 201617
— 201516
— 201415
— 201314
— 201213
— 201112
— 201011
— 200910
— 200809

Fri 24th Nov 2017 
20. No Lecture


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.
These are additional selfhelp 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.
 The Isabelle20161 theorem prover will be used in this course. 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 the following
command from the terminal: Isabelle
 Isabelle Cheat sheet listing common proof commands and rules (note: ignore the references to Proof General). Also available here.
 Isar Quick Reference.
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:
 Lecture: 17th Oct 2016 during the usual lecture slot
 Deadline: 20th Nov 2017 at 4pm
Coursework