THE UNIVERSITY of EDINBURGH

DEGREE REGULATIONS & PROGRAMMES OF STUDY 2012/2013
- ARCHIVE for reference only
THIS PAGE IS OUT OF DATE

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

Undergraduate Course: Automated Reasoning (Level 10) (INFR10041)

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Course typeStandard AvailabilityAvailable to all students
Credit level (Normal year taken)SCQF Level 10 (Year 4 Undergraduate) Credits10
Home subject areaInformatics Other subject areaNone
Course website http://www.inf.ed.ac.uk/teaching/courses/ar Taught in Gaelic?No
Course descriptionThe 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 (not applicable to Visiting Students)
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
Information for Visiting Students
Pre-requisitesNone
Displayed in Visiting Students Prospectus?Yes
Course Delivery Information
Delivery period: 2012/13 Semester 1, Available to all students (SV1) Learn enabled:  No Quota:  None
Location Activity Description Weeks Monday Tuesday Wednesday Thursday Friday
CentralLecture1-11 16:10 - 17:00
CentralLecture1-11 16:10 - 17:00
First Class Week 1, Monday, 16:10 - 17:00, Zone: Central. LT5 7 Bristo Square
Exam Information
Exam Diet Paper Name Hours:Minutes
Main Exam Diet S2 (April/May)2:00
Delivery period: 2012/13 Semester 1, Part-year visiting students only (VV1) Learn enabled:  No Quota:  None
Location Activity Description Weeks Monday Tuesday Wednesday Thursday Friday
CentralLecture1-11 16:10 - 17:00
CentralLecture1-11 16:10 - 17:00
First Class Week 1, Monday, 16:10 - 17:00, Zone: Central. LT5 7 Bristo Square
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 - 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 60
Assessed Assignments 40
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.
Special Arrangements
None
Additional Information
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 * 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 40
Private Study/Other 40
Total 100
KeywordsNot entered
Contacts
Course organiserDr Mary Cryan
Tel: (0131 6)50 5153
Email: mcryan@inf.ed.ac.uk
Course secretaryMiss 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 2012 The University of Edinburgh - 14 January 2013 4:09 am