On this page:

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

The lectures will be given by:

- Jacques Fleuriot. Email:
`jdf@inf.ed.ac.uk`. Room IF2.15. - Paul Jackson. Email:
`pbj@inf.ed.ac.uk`. Room IF2.12.

Demonstrator times:

- The TA for the first half of the course (Victor Dumitrescu) will be available in
**FH 1.B31**between**3pm and 5pm**on**Thursdays**to help with any problems with course material and coursework. There will be 4 lab sessions, from Week 3 (Thu 28/01) to Week 6 (Thu 25/02). Note that there will be no lab session during Innovative Learning Week (15-19 Feb). - Demonstrator times for second half of the course TBC

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 `ar-students@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.

- 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 the first 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 lecturers.

Lectures are held at 16.10-17.00 in Semester 2 on Tuesdays and
Fridays in **LG34**
of Paterson's Land.

The first lecture is on Tuesday 12th January 2016.

Note that there are *no* lecture notes for the
course. Instead, recommended reading is associated with each
lecture. This reading is usually from:

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

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.

There are two pieces of software that we will be using for this course.

The Isabelle2015 theorem prover. 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`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.

- The NuSMV model checker. This will be used in the second half of the course, and is also installed on DICE.

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:

- Coursework 1: Hand out 2nd February 2016 by 4pm (Week 4),
**Deadline: Friday 26th February at 4pm**(Week 6) - Coursework 2: Hand out 4th March 2016 by 4pm (Week 7),
**Deadline: Friday 18th March 2016 at 4pm**(Week 9)

The first coursework overlaps with Innovative Learning Week, which accounts for the longer elapsed time between hand out and deadline.

Hand out: 2nd February 2016. Deadline: **4pm, Friday 26th February 2016**.

- The coursework description.
- The coursework theory file (to be filled in with your proofs).

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 |