Undergraduate Course: Automated Reasoning (INFR09042)

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

Entry Requirements (not applicable to Visiting Students)
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.

Information for Visiting Students
Pre-requisites	Prior familiarity with propositional and predicate logic is recommended.
High Demand Course?	Yes

Course Delivery Information

Academic year 2017/18, Available to all students (SV1)		Quota: 50
Course Start	Semester 1
Timetable	Timetable
Learning and Teaching activities (Further Info)	Total Hours: 100 ( Lecture Hours 16, Seminar/Tutorial Hours 8, Feedback/Feedforward Hours 1, Summative Assessment Hours 2, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 71 )
Assessment (Further Info)	Written Exam 60 %, Coursework 40 %, Practical Exam 0 %
Additional Information (Assessment)	The course will consist of 1 practical exercise (40%), assessing learning objectives 1 to 3. Students may be asked to represent and reason about particular domains e.g. geometry or inductive proofs in the Isabelle theorem prover. There will be a formative part to the assessment that will involve the students carrying out Natural Deduction proofs in Isabelle and receiving early feedback on their effort during tutorials. For the summative part, the students will submit their files, usually in the form of mechanized theories, electronically for marking. The examination (60%) will concentrate on assessing learning outcomes 4 and 5, which mainly involve theoretical aspects (e.g. important algorithms and techniques), representation issues, problem solving (e.g. proofs using natural deduction) and discussing broader aspects such as the capabilities and limitations of various proof techniques.
Feedback	The students will receive feedback on their weekly tasks during the tutorials. The tasks will include both pen-and-paper and Isabelle-based exercises. Full solutions will be made available on the AR website at the end of each week. A marking guide, with extensive notes, will be released after the marks for the assignment have been returned (as is currently the case). 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

Academic year 2017/18, Part-year visiting students only (VV1)		Quota: None
Course Start	Semester 1
Timetable	Timetable
Learning and Teaching activities (Further Info)	Total Hours: 100 ( Lecture Hours 16, Seminar/Tutorial Hours 8, Feedback/Feedforward Hours 1, Summative Assessment Hours 2, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 71 )
Assessment (Further Info)	Written Exam 60 %, Coursework 40 %, Practical Exam 0 %
Additional Information (Assessment)	The course will consist of 1 practical exercise (40%), assessing learning objectives 1 to 3. Students may be asked to represent and reason about particular domains e.g. geometry or inductive proofs in the Isabelle theorem prover. There will be a formative part to the assessment that will involve the students carrying out Natural Deduction proofs in Isabelle and receiving early feedback on their effort during tutorials. For the summative part, the students will submit their files, usually in the form of mechanized theories, electronically for marking. The examination (60%) will concentrate on assessing learning outcomes 4 and 5, which mainly involve theoretical aspects (e.g. important algorithms and techniques), representation issues, problem solving (e.g. proofs using natural deduction) and discussing broader aspects such as the capabilities and limitations of various proof techniques.
Feedback	The students will receive feedback on their weekly tasks during the tutorials. The tasks will include both pen-and-paper and Isabelle-based exercises. Full solutions will be made available on the AR website at the end of each week. A marking guide, with extensive notes, will be released after the marks for the assignment have been returned (as is currently the case). 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 S1 (December)			2:00

Learning Outcomes
On completion of this course, the student will be able to: Use sophisticated mechanisms available in theorem provers to represent problem. Write interactive proof in procedural and declarative styles. Use interactive and automated methods to carry out proofs in the theorem prover. Represent and reason about mathematical and other less formal knowledge using logic. 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).