Module 05931 (2001)
Syllabus page 2001/2002
06-05931
Mechanised Deduction
Level 3/H
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus
The Module Description is a strict subset of this Syllabus Page. (The University module description has not yet been checked against the School's.)
Relevant Links
For more information (like notes, handouts) see the module web page at
http://www.cs.bham.ac.uk/~mmk/Teaching/Deduction/.
Outline
The main notions and problems of mechanised deduction are presented. The standard techniques of automated deduction, in particular the resolution calculus with restrictions (like logic programming) and extensions (dealing with equations and mathematical induction) are presented. Proof planning systems as a human-oriented alternative to deduction will be presented as well. This approach is an extension of the tactic approach in interactive theorem proving. Example applications will motivate the material.
Aims
The aims of this module are to:
- introduce the basic concepts and terminology of mechanised deduction
- present the main approaches to automated, machine-oriented, human-oriented, and interactive mechanised deduction.
- present the strengths and limitations of the different approaches
- enable the students to read recent research papers in mechanised deduction
Learning Outcomes
| On successful completion of this module, the student should be able to: | Assessed by: | |
| 1 | explain the main approaches in mechanised deduction | Examination |
| 2 | discuss the advantages and limitations of the approaches | Examination |
| 3 | apply the different approaches to unseen examples | Examination |
| 4 | explain the relationship between approaches to mechanised deduction and of human theorem proving | Examination |
| 5 | read, understand and give a presentation on a recent research paper in the field | In-class student presentation |
Restrictions, Prerequisites and Corequisites
Restrictions:
None
Prerequisites:
06-08764 (Mathematics & Logic B) or equivalent as knowledge of first-order logic is necessary
Co-requisites:
None
Teaching
Teaching Methods:
2 hrs/week of lectures, exercise classes in the first part; short presentations of original publications in the second part
Contact Hours:
Assessment
- Supplementary (where allowed): As the sessional assessment
- 2 hr examination (80%), continuous assessment (preparation & presentation of seminar) (20%).
Recommended Books
| Title | Author(s) | Publisher, Date |
| Principles of Automated Theorem Proving | Duffy D | 1991 |
Detailed Syllabus
-
Introduction to mechanised deduction, different goals and
approaches (1 week)
- Examples: program verification (Hoare calculus) and planning (situation calculus)
- Resolution calculus (2 weeks)
- unification, clause normal form, skolemisation, resolution rule, extensions to resolution: restriction strategies, selection strategies, sorts
- Equality handling (1 week)
- paramodulation, Knuth-Bendix procedure
- Higher-order treatment (1 week)
- higher-order resolution, higher-order unification
- Interactive theorem proving (1 week)
- natural deduction, tactics, tacticals
- Inductive theorem proving (1 week)
- classical approaches, rippling
- Proof planning (1 week)
- Applications (1 week)
- Student presentations at their choice from a list of more than 50 publications (2 weeks)
Last updated: 29 July 2001
Source file: /internal/modules/COMSCI/2001/xml/05931.xml
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus