Postgraduate Course: Automated Reasoning (Level 11) (INFR11074)

Course Outline
School	School of Informatics	College	College of Science and Engineering
Course type	Standard	Availability	Available to all students
Credit level (Normal year taken)	SCQF Level 11 (Year 4 Undergraduate)	Credits	10
Home subject area	Informatics	Other subject area	None
Course website	http://www.inf.ed.ac.uk/teaching/courses/ar	Taught in Gaelic?	No
Course description	The overall aim of the course is to describe how reasoning can be automated. Its more specific aim is to provide a route into more advanced uses of theorem proving in automated reasoning and in solving challenging problems of mathematics. Major emphases are on: how knowledge can be represented using logic; how these representations can be used as the basis for reasoning and how these reasoning processes can be guided to a successful conclusion. Students are encouraged to develop a deep understanding of automated reasoning from mathematical "first principles" via theorem proving.

Entry Requirements (not applicable to Visiting Students)
Pre-requisites		Co-requisites
Prohibited Combinations	Students MUST NOT also be taking Automated Reasoning (Level 10) (INFR10041)	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. This course assumes prior mathematical knowledge of induction.
Additional Costs	None

Information for Visiting Students
Pre-requisites	Prior familiarity with propositional and predicate logic is recommended.
Displayed in Visiting Students Prospectus?	Yes

Course Delivery Information

Delivery period: 2014/15 Semester 1, Available to all students (SV1)			Learn enabled: No	Quota: None
Web Timetable	Web Timetable
Course Start Date	15/09/2014
Breakdown of Learning and Teaching activities (Further Info)	Total Hours: 100 ( Lecture Hours 20, Supervised Practical/Workshop/Studio Hours 16, Summative Assessment Hours 2, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 60 )
Additional Notes
Breakdown of Assessment Methods (Further Info)	Written Exam 60 %, Coursework 40 %, Practical Exam 0 %
Exam Information
Exam Diet	Paper Name	Hours & Minutes
Main Exam Diet S2 (April/May)		2:00

Delivery period: 2014/15 Semester 1, Part-year visiting students only (VV1)			Learn enabled: No	Quota: None
Web Timetable	Web Timetable
Course Start Date	15/09/2014
Breakdown of Learning and Teaching activities (Further Info)	Total Hours: 100 ( Lecture Hours 20, Supervised Practical/Workshop/Studio Hours 16, Summative Assessment Hours 2, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 60 )
Additional Notes
Breakdown of Assessment Methods (Further Info)	Written Exam 60 %, Coursework 40 %, Practical Exam 0 %
Exam Information
Exam Diet	Paper Name	Hours & Minutes
Main Exam Diet S1 (December)		2:00

Summary of Intended Learning Outcomes
1 - represent mathematical and other knowledge using logic. 2 - analyze the behaviour of various reasoning techniques from "first principles" as theorem proving tasks. 3 - formalize informal knowledge and reason rigorously about it, understanding the role of mathematical proof in this process. 4 - compare precisely the tradeoffs between some rival techniques for the same reasoning task. 5 - implement key reasoning techniques in a computer program/theorem prover. 6 - know how to use more sophisticated reasoning techniques implemented in a computer program/theorem prover. 7 - organize their own study to manage project development. 8 - search and read the literature. 9 - conduct exploratory experiments. 10 - critically analyze and evaluate other people's work. 11 - be broadly up-to-date with current research in the field

Assessment Information
Written Examination 60 Assessed Assignments 40 Oral Presentations 0 The course consists of 2 practical exercises. Students may be asked to reason about particular domains (e.g. geometry) in a theorem prover such as Isabelle or Coq. They may also be asked to verify a program using the a model checker such as SPIN or NuSMV.

Special Arrangements
None

Additional Information
Academic description	Not entered
Syllabus	The course combines an exposition of theory with the analysis of particular computer programs for reasoning. Topics will be selected from the following list: # First Order Logic and Higher Order Logic * Syntax * HOL: Types and terms, currying and binders * Unification algorithm * Natural Deduction # Model Checking * Computation Tree Logic: syntax and semantics * A model checking algorithm * Model checker: NuSMV or SPIN * Fairness * Alternatives and extensions of CTL: LTL, CTL* # Interactive Theorem Proving * Human-oriented methods * Interactive provers and proof checkers * LCF style theorem proving * Proof styles * Formalized Mathematics # Decidable Problems and Automation * Presburger arithmetic * Geometry theorem proving * Induction and recursion * Simplification, proof planning, and rippling # Program Verification * Functional programs * Case studies e.g. sorting algorithms Relevant QAA Computing Curriculum Sections: Artificial Intelligence
Transferable skills	Not entered
Reading list	* T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic , Springer-Verlag, 2002. * Logic in Computer Science, Modelling and and Reasoning about Systems, M.Huth and M.Ryan, Cambridge University Press, 2nd Edition, 2004 * The Computer Modelling of Mathematical Reasoning, A. Bundy, Academic Press 1983
Study Abroad	Not entered
Study Pattern	Lectures 20 Tutorials 0 Timetabled Laboratories 0 Non-timetabled assessed assignments 30 Private Study/Other 50 Total 100
Keywords	Not entered