Module 26264 (2013)
Syllabus page 2013/2014
06-26264
Reasoning
Level 2/I
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
Further information about this module can be found on the
module web page
.
Outline
The module will introduce automated theorem proving. Both implementation and representation theories are covered as are some applications.
Aims
The aims of this module are to:
- present automated reasoning;
- introduce the principal techniques such as resolution, forward and backward chaining;
- introduce areas of application such as default reasoning, constraint-based reasoning, case-based reasoning, reasoning by analogy, learning through induction.
Learning Outcomes
| On successful completion of this module, the student should be able to: | Assessed by: | |
| 1 | describe the basic concepts of automated theorem proving | Examination, Continuous Assessment |
| 2 | demonstrate an understanding of applications of automated theorem proving | Examination, Continuous Assessment |
| 3 | demonstrate an understanding of the techniques of implementing automated theorem provers | Examination, Continuous Assessment |
| 4 | Demonstrate an understanding of unsound reasoning methods such as abduction, case-based reasoning, constraint satisfaction reasoning, default reasoning, learning/inductive logic programming, and reasoning by analogy | Examination, Continuous Assessment |
Restrictions, Prerequisites and Corequisites
Restrictions:
None
Prerequisites:
06-21155 Language and Logic
Co-requisites:
None
Teaching
Teaching Methods:
three-hour weekly lectures/labs.
Contact Hours:
Assessment
- Sessional: 1.5 hr examination (80%), continuous assessment (20%).
- Supplementary (where allowed): By 1.5 hr examination only (100%).
Recommended Books
| Title | Author(s) | Publisher, Date |
| Artificial Intelligence: A Modern Approach (3rd edn) | S Russell & P Norvig | Prentice Hall , 2010 |
Detailed Syllabus
- Introduction and preliminaries
- Propositional logic theorem proving
- Proof by resolution
- Completeness properties
- Horn clauses and definite clauses
- Forwards and backwards chaining
- Implementation, e.g. Wang prover
- Predicate logic theorem proving
- Unification
- Resolution for predicate logic
- Forward chaining algorithms
- Backward chaining algorithms
- Logic programming as theorem proving
- Implementations, e.g. Prolog, Constraint Handling Rules
- Varieties of theorem provers in applications, for instance:
- Abduction
- Case-based reasoning
- Constraint satisfaction reasoning
- Default reasoning
- Learning/inductive logic programming
- Reasoning by analogy
Last updated: 30 May 2013
Source file: /internal/modules/COMSCI/2013/xml/26264.xml
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus