Automated Reasoning (INFR10087)
Normal Year Taken
Delivery Session Year
Prior familiarity with propositional and predicate logic is recommended.
**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.
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.
Written Exam 60%, Coursework 0%, Practical Exam 40%
All course information obtained from this visiting student course finder should be regarded as provisional. We cannot guarantee that places will be available for any particular course. For more information, please see the visiting student disclaimer: