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 (Postgraduate) |
Credits |
10 |
| Home subject area |
Informatics |
Other subject area |
None |
| Course website |
http://www.inf.ed.ac.uk/teaching/courses/ar |
|
|
| 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. |
Course Delivery Information
|
| Delivery period: 2010/11 Semester 1, Available to all students (SV1)
|
WebCT enabled: No |
Quota: None |
| Location |
Activity |
Description |
Weeks |
Monday |
Tuesday |
Wednesday |
Thursday |
Friday |
| Central | Lecture | | 1-11 | | | | 16:10 - 17:00 | | | Central | Lecture | | 1-11 | 16:10 - 17:00 | | | | |
| First Class |
Week 1, Monday, 16:10 - 17:00, Zone: Central. Faculty Room North, David Hume Tower |
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 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 |
Assessment Information
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.
If delivered in semester 1, this course will have an option for semester 1 only visiting undergraduate students, providing assessment prior to the end of the calendar year. |
| Please see Visiting Student Prospectus website for Visiting Student Assessment information |
Special Arrangements
| Not entered |
Contacts
| 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 |
|
copyright 2010 The University of Edinburgh -
1 September 2010 6:11 am
|
University Homepage