Undergraduate Course: Automated Reasoning (Level 10) (INFR10041)
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 10 (Year 4 Undergraduate) |
Credits |
10 |
| Home subject area |
Informatics |
Other subject area |
None |
| Course website |
http://www.inf.ed.ac.uk/teaching/courses/ar |
|
|
| Course description |
The aim of the module is to describe how reasoning can be automated. 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. Many of the examples are drawn from mathematics because this domain contains lots of challenging reasoning problems which can be succinctly stated. A version of this course is available also at level 11 for students who wish to explore the mathematics of theorem proving in greater depth, with the aim of specialising in one of its many sub-fields. |
Entry Requirements
| 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 |
Successful completion of Year 3 of an Informatics Single or Combined Honours Degree, or equivalent by permission of the School. This course assumes prior mathematical knowledge of induction.
|
| Additional Costs |
None |
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 |
|
| Delivery period: 2010/11 Semester 1, Part-year visiting students only (VV1)
|
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 - compare various reasoning techniques.
3 - formalize informal knowledge and reason rigorously about it.
4 - discuss some of the tradeoffs between some rival techniques for the same reasoning task.
5 - implement/use reasoning techniques in a computer program/theorem prover.
6 - organize their own study to manage project development.
7 - search and read the literature.
8 - conduct exploratory experiments.
9 - critically analyze and evaluate other people's work.
10 - be broadly up-to-date with current research in the field |
Assessment Information
Written Examination 75
Assessed Assignments 25
Oral Presentations 0
The coursework is comprised of two practical exercises. The 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.
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 Amos Storkey
Tel: (0131 6)51 1208
Email: A.Storkey@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:10 am
|
University Homepage