# DEGREE REGULATIONS & PROGRAMMES OF STUDY 2011/2012

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

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

 School School of Informatics College College of Science and Engineering Course type Standard Availability Not available to visiting students Credit level (Normal year taken) SCQF Level 11 (Postgraduate) 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 module 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 if 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.
 Pre-requisites Co-requisites Prohibited Combinations Students MUST NOT also be taking Automated Reasoning (Level 10) (INFR10041) Other requirements For Informatics PG and final year MInf students only, or by special permission of the School. This course assumes prior mathematical knowledge of induction. Additional Costs None
 Delivery period: 2011/12 Semester 1, Not available to visiting students (SS1) WebCT enabled:  No Quota:  None Location Activity Description Weeks Monday Tuesday Wednesday Thursday Friday No Classes have been defined for this Course First Class Week 1, Monday, 16:10 - 17:00, Zone: Central. Chrystal Mac Building Sem Rm 5 Exam Information Exam Diet Paper Name Hours:Minutes Main Exam Diet S2 (April/May) 2:00
 1 - represent mathematical and other knowledge using logic. 2 - analyze the behaviour of various reasoning techniques from "first principles" as theorem provign 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 12 - be up-to-date in detail with at least one significant, specific aspect of current research in the field
 Written Examination 75 Assessed Assignments 25 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 SPIN model checker. This version of the course differs from the level 10 one in requiring students to undertake practical exercises demanding deeper analysis of the mathematical theory behind the computational mechanisms. Some aspects of the exercises are thus likely to be open-ended in nature and the students will be expected to analyze various issues to do with their formalization and/or implementation.
 None
 Academic description Not entered Syllabus The module 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: SMV 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 * A. Bundy et al. Rippling: Meta-level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science (No. 56), 2005 * T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic , Springer-Verlag, 2002 * M. R. A. Ruth and M. D. Ryan. Logic in Computer Science, Cambridge University Press, Second Edition, 2004. * Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development: Coq'Art: the Calculus of Inductive Constructions, 2004. 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
 Course organiser Dr Michael Rovatsos Tel: (0131 6)51 3263 Email: mrovatso@inf.ed.ac.uk Course secretary Miss Kate Weston Tel: (0131 6)50 2701 Email: Kate.Weston@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 Timetab Prospectuses Important Information
© Copyright 2011 The University of Edinburgh - 16 January 2012 6:17 am