Automated Reasoning (201819): This course is being updated
 Official course descriptor (Note: a pass in Inf2D is a nonnegotiable prerequisite for UG3 students. MSc students should talk to me, if they are unsure about the prerequesites. 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 14:1015:00 in Semester 1 on Tuesdays and Thursdays in Room 1.3 of the Lister Learning and Teaching Centre, Roxburgh Street.
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.
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.
Title 
Files 
Solutions 
Propositional logic 
[pdf][thy] 
[thy] 
Predicate logic 
[pdf][thy] 
[thy] 
A riddle: The rich grandfather 
[pdf][thy] 
See Tutorial 4 
A Bad Axiomatization 
[pdf][thy] 

 The Isabelle2018 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: 18th October 2018, during the usual lecture slot.
 Deadline: 4pm, 19th November 2018.
Coursework