# DEGREE REGULATIONS & PROGRAMMES OF STUDY 2016/2017

 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 Credit level (Normal year taken) SCQF Level 11 (Year 4 Undergraduate) Availability Available to all students SCQF Credits 10 ECTS Credits 5 Summary ***PLEASE NOTE: This course has been replaced with INFR09042 Automated Reasoning*** 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. Course description 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
 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.
 Pre-requisites Prior familiarity with propositional and predicate logic is recommended. High Demand Course? Yes
 Not being delivered
 On completion of this course, the student will be able to: 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
 * 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
 Course URL http://course.inf.ed.ac.uk/ar Graduate Attributes and Skills Not entered Keywords Not entered
 Course organiser Dr Jacques Fleuriot Tel: (0131 6)50 9342 Email: Jacques.Fleuriot@ed.ac.uk Course secretary Mr Gregor Hall Tel: (0131 6)50 5194 Email: gregor.hall@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 Combined Course Timetable Prospectuses Important Information
© Copyright 2016 The University of Edinburgh - 3 February 2017 4:26 am