Automated Reasoning (2017-18): This course is being updated

On this page:

The lectures are given by:

The Teaching Assistant (TA) is:

Demonstrator times:

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

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:

Lecture Schedule

The lectures are held at 15:10-16:00 in Semester 1 on:

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 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.1-5.7 of Tutorial on Isabelle/HOL (2016-1)
Prop.thy Isabelle theory file
Fri 29th Sep 2017 4. Propositional Reasoning in Isabelle
Sec 5.1-5.7 of Tutorial on Isabelle/HOL (2016-1)
[background] Pollack's How to Believe a Machine-Checked Proof
[background] How do they verify a verifier of formalized proofs?
3 Tue 3rd Oct 2017 5. First-order Logic
H&R Secs 2.1-2.4
FOL.thy Isabelle theory file
[background] Logitext - an interactive L-system 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.1-1.4 of Tutorial on Isabelle/HOL (2016-1)
N&K Sec 2.1-2.2
Fri 13th Oct 2017 8. Representation II: Locales in Isabelle/HOL
Isabelle Theory file for Lecture 8
Tutorial on Locales (Isabelle 2016-1)
[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.1-17.4
Fri 27th Oct 2017 12. Rewriting I Bundy, Ch. 9
Sec 3.1 of Tutorial on Isabelle/HOL (2016-1)
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.1-4.3
N&K Sec 12.2.1
[background] Reading on Hoare Logic (especially pages 1-27, 37-48).
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 2016-17 also contain material not in the current course):
2016-17
2015-16
2014-15
2013-14
2012-13
2011-12
2010-11
2009-10
2008-09
Fri 24th Nov 2017 20. 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
[pdf][thy]
4 Tutorial 2: First order logic and more Isabelle
[pdf][thy]
5 Tutorial 3: Representation and reasoning in Isabelle using locales
[thy]
6 Tutorial 4: Structured proofs in Isabelle
[thy]
7 Tutorial 5: Unification and Rewrite Rules [pdf]
8 Tutorial 6/7: Rewrite Rules, Reasoning about Hoare Logic, Induction [thy]
[thy]
9 Tutorial 6/7: Rewrite Rules, Reasoning about Hoare Logic, Induction [pdf]

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] [pdf][thy]
Predicate logic [pdf][thy] [pdf][thy]
A riddle: The rich grandfather [pdf][thy]
A Bad Axiomatization [pdf][thy]

Software

Useful Resources

Assessment and Coursework

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:

Coursework


Home : Teaching : Courses 

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