Automated Reasoning (2016-17): This course is undergoing a major update. Some of the topics described below will not be covered in 2016/17.

On this page:

Please register your feedback on this course at the Informatics Course Survey.

The lectures are given by:

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. 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.

Lecture Schedule

Lectures are held at 15.10-16.00 in Semester 1 on Tuesdays and Fridays in venue: to be confirmed .

The first lecture is on Tuesday 20th September 2016.

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 hand-out 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 20th Sep 2016 1. Introduction Bundy, Ch. 1
[background] Logicomix
Fri 23rd Sep 2016 2. Propositional Logic and Natural Deduction
Exercises
H&R Sec 1.1, 1.2, 1.3, start of 1.4
[background] Wadler's Propositions as Types
2 Tue 27th Sep 2016 3. Natural Deduction and Starting with Isabelle
Exercises
H&R Sec 1.2, 1.4
Getting Started with Isabelle
Sec 5.1-5.7 of Tutorial on Isabelle/HOL
Prop.thy Isabelle theory file
Fri 30th Sep 2016 4. Propositional Reasoning in Isabelle
Exercises
Sec 5.1-5.7 of Tutorial on Isabelle/HOL
[background] Pollack's How to Believe a Machine-Checked Proof
[background] How do they verify a verifier of formalized proofs?
3 Tue 4th Oct 2016 5. First-order Logic
Exercises
H&R Secs 2.1-2.4
FOL.thy Isabelle theory file
[background] Logitext - an interactive L-system FOL prover
Fri 7th Oct 2016 6. Representation & Introduction to HOL
Exercises
Bundy Ch. 4
4 Tue 11th Oct 2016 7. Coursework: Proving and Reasoning in Isabelle/HOL
Coursework description
Coursework theory file
Fri 14th Oct 2016 8. Unification
Exercises
Bundy 17.1 - 17.4
[background] Unification theory -- a survey of the state of the art from 2001.
5 Tue 18th Oct 2016 9. Rewriting
Exercises
Bundy Ch. 9
Fri 21st Oct 2016 10. Creativity in Inductive Theorem Proving
Exercises
Bundy Ch. 11
[background] Productive Use of Failure in Inductive Proof
6 Tue 25th Oct 2016 11.
Fri 29th Oct 2016 12.
7 Tue 1st Nov 2016 13.
Fri 4th Nov 2016 14.
8 Tue 8th Nov 2016 15.
Fri 11th Nov 2016 16.
9 Tue 15th Nov 2016 17.
Fri 18th Nov 2016 18.
10 Tue 22nd Nov 2016 19.
Fri 25th Nov 2016 20.

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 is 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