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 
Taught in Gaelic?  No 
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 subfields. 
Entry Requirements (not applicable to Visiting Students)
Prerequisites 
Students MUST have passed:
Informatics 2D  Reasoning and Agents (INFR08010)

Corequisites  
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
Prerequisites  None 
Displayed in Visiting Students Prospectus?  Yes 
Course Delivery Information

Delivery period: 2011/12 Semester 1, Available to all students (SV1)

WebCT enabled: No 
Quota: None 
Location 
Activity 
Description 
Weeks 
Monday 
Tuesday 
Wednesday 
Thursday 
Friday 
Central  Lecture   111  16:10  17:00      Central  Lecture   111     16:10  17:00  
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   

Delivery period: 2011/12 Semester 1, Partyear visiting students only (VV1)

WebCT enabled: No 
Quota: None 
Location 
Activity 
Description 
Weeks 
Monday 
Tuesday 
Wednesday 
Thursday 
Friday 
Central  Lecture   111  16:10  17:00      Central  Lecture   111     16:10  17:00  
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 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 uptodate 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. 
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
* Humanoriented 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: Metalevel 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 HigherOrder Logic , SpringerVerlag, 2002.
* M. R. A. Ruth and M. D. Ryan. Logic in Computer Science, Cambridge University Press, 2nd 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
Nontimetabled assessed assignments 30
Private Study/Other 50
Total 100 
Keywords  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 

