# DEGREE REGULATIONS & PROGRAMMES OF STUDY 2019/2020

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

# Undergraduate Course: Automated Reasoning (INFR09042)

 School School of Informatics College College of Science and Engineering Credit level (Normal year taken) SCQF Level 9 (Year 3 Undergraduate) Availability Available to all students SCQF Credits 10 ECTS Credits 5 Summary The overall aim of the course is to describe how reasoning can be modelled using computers. Its more specific aim is to provide a route into more advanced uses of theorem proving in order to solve problems in mathematics and formal verification. Major emphases are on: how knowledge can be represented using propositional, first-order and higher-order logic; how these representations can be used as the basis for reasoning, and how these reasoning processes can be guided to a successful conclusion through a variety of means ranging from fully-automated to interactive ones. Students will develop a thorough understanding of modern, interactive theorem proving via lectures, tutorials and an assignment. This course will replace Automated Reasoning (Level 11) (INFR11074). 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 tutorials that incorporate practical exercises 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 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 of the challenges that advanced interactive theorem proving entails.
 Pre-requisites Students MUST have passed: Informatics 2D - Reasoning and Agents (INFR08010) Co-requisites Prohibited Combinations Students MUST NOT also be taking Automated Reasoning (Level 11) (INFR11074) Other requirements This course is open to all Informatics students including those on joint degrees. External students should seek special permission from the course organiser. Prior familiarity with propositional and predicate logic is recommended.
 Pre-requisites Prior 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