THE UNIVERSITY of EDINBURGH

DEGREE REGULATIONS & PROGRAMMES OF STUDY 2022/2023

Timetable information in the Course Catalogue may be subject to change.

University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Undergraduate Course: Automated Reasoning (INFR10087)

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Credit level (Normal year taken)SCQF Level 10 (Year 3 Undergraduate) AvailabilityAvailable to all students
SCQF Credits10 ECTS Credits5
Summary**This course replaces the Level 9 Automated Reasoning INFR09042 10 credit course from 2022-23**

Automated Reasoning covers the theory, implementation and applications of logic-based reasoning via computers. It is one of the oldest subfields of Artificial Intelligence, originating in the mid-1950s when it was first used to reason about propositional logic. Since then, it has been applied to domains ranging from the formalisation of advanced mathematics to the formal verification of software and hardware systems.

In this course, we take an interactive approach to automated reasoning and explore how the proof assistant Isabelle can work with the user to establish mathematical correctness via a formal but human-friendly proof language. This provides a way of turning logicbased reasoning into a form of programming that can then be used (among other things) to reason about problems in mathematics, e.g. probability theory and multivariate analysis, and industrially-relevant areas e.g. the safety of autonomous systems.
Course description The course starts with an introduction to higher order logic, theorem provers and, more specifically, Isabelle/HOL. This will set the context for the rest of the course in which Isabelle will be the framework for getting hands-on experience about the application of various theoretical concepts.

Through the lectures and weekly exercises that incorporate practical aspects the students will gain the skills needed to get started with Isabelle and progress to more complex concepts involving both representation and reasoning.

The second part will look at representation/modelling of concepts in (higher order) logic in details. Axiomatic versus conservative extensions of theories will be covered and mechanisms such as Isabelle locales will be introduced and used. Recursive definitions and inductive notions will be covered too.

The third part of the course will focus on fundamental notions such as unification and rewriting, within both a first and higher order context. It will look at notions such as termination and use Isabelle's simplifier as the tool for understanding many of the concepts. It will also look at the interplay between (fully) automatic and interactive proofs.

The fourth part will introduce declarative/structured proofs and using the Isar language of Isabelle show how proofs resembling pencil and paper ones can be formalized.

Finally the various strands will be brought together through the discussion of a non-trivial case study. This may involve either formalized mathematics (e.g. looking at a geometric theory) or a formal verification example.

The assignment will be a combination of basic to intermediate representation and reasoning in Isabelle (up to 40%), more advanced proof tackling one particular domain or example (up to 40%) and a final part which, if completed successfully, will clearly demonstrate that the student has a good grasp of the challenges that advanced interactive theorem proving entails.
Entry Requirements (not applicable to Visiting Students)
Pre-requisites Co-requisites
Prohibited Combinations Other requirements None
Information for Visiting Students
Pre-requisitesPrior familiarity with propositional and predicate logic is recommended.

This course is open to full year Visiting Students only, as the course is delivered in Semester 1 and examined at the end of Semester 2.
High Demand Course? Yes
Course Delivery Information
Academic year 2022/23, Available to all students (SV1) Quota:  None
Course Start Semester 1
Timetable Timetable
Learning and Teaching activities (Further Info) Total Hours: 100 ( Lecture Hours 16, Supervised Practical/Workshop/Studio Hours 16, Feedback/Feedforward Hours 1, Summative Assessment Hours 2, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 63 )
Assessment (Further Info) Written Exam 60 %, Coursework 0 %, Practical Exam 40 %
Feedback The students will receive feedback on a weekly task via the mailing list/AR class forum and during the labs. The tasks will include both pen-and-paper and Isabelle-based exercises. Full solutions will be made available in Learn at the end of each week.

A marking guide, with extensive notes, will be released after the marks for the assignment have been returned. This will provide a breakdown of how marks were allocated, especially for the more challenging parts of the formalization. Common pitfalls will be highlighted and advice provided on how these should have been tackled.

The automated reasoning mailing list will be used (as is currently the case) to provide general feedback and any advice deemed appropriate during the course and before the exams.
Exam Information
Exam Diet Paper Name Hours & Minutes
Main Exam Diet S2 (April/May)2:00
Resit Exam Diet (August)2:00
Learning Outcomes
On completion of this course, the student will be able to:
  1. Use sophisticated mechanisms available in theorem provers to represent problem.
  2. Write interactive proof in procedural and declarative styles.
  3. Use interactive and automated methods to carry out proofs in the theorem prover.
  4. Represent and reason about mathematical and other less formal knowledge using logic.
  5. Understand and compare automated reasoning techniques and apply them using pen-and-paper.
Reading List
Recommended reading list:
1. John Harrison. Handbook of Practical Logic and Automated Reasoning, CUP, 2009.
2. Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL, Springer, 2014.
3. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher- Order Logic , Springer, 2002.
4. M.Huth and M.Ryan. Logic in Computer Science, Modelling and and Reasoning about Systems, CUP, 2nd Edition, 2004.

The students will also be asked to read various papers and given links to presentations and websites with materials pertaining to various theorem proving projects and repositories (e.g. The Archive of Formal Proof).
Additional Information
Graduate Attributes and Skills Not entered
KeywordsAutomated Reasoning,Theorem Proving,Formal proof
Contacts
Course organiserDr Jacques Fleuriot
Tel: (0131 6)50 9342
Email: Jacques.Fleuriot@ed.ac.uk
Course secretaryMrs Michelle Bain
Tel: (0131 6)51 7607
Email: michelle.bain@ed.ac.uk
Navigation
Help & Information
Home
Introduction
Glossary
Search DPTs and Courses
Regulations
Regulations
Degree Programmes
Introduction
Browse DPTs
Courses
Introduction
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Combined Course Timetable
Prospectuses
Important Information