Module 06-26264 (2017)
Reasoning
Level 2/I
Volker Sorge | Semester 2 | 10 credits |
Co-ordinator: Volker Sorge
Reviewer: Mark Lee
The Module Description is a strict subset of this Syllabus 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:
- describe the basic concepts of automated theorem proving
- demonstrate an understanding of applications of automated theorem proving
- demonstrate an understanding of the techniques of implementing automated theorem provers
- 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
Restrictions
None
Pre-requisites
- 06-21155 - Language & Logic
Teaching methods
three-hour weekly lectures/labs.
Contact Hours: 34
Assessment
Sessional: 1.5 hr examination (80%), continuous assessment (20%).
Supplementary (where allowed): By 1.5 hr examination only (100%).
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
Programmes containing this module
- BSc Artificial Intelligence & Computer Science [0144]
- BSc Artificial Intelligence & Computer Science with an Industrial Year [9502]
- BSc Artificial Intelligence & Computer Science with Study Abroad [452B]
- BSc Computer Science [4436]
- BSc Computer Science with an Industrial Year [9499]
- BSc Computer Science with Study Abroad [5571]
- MSci Computer Science [4443]
- MSci Computer Science with an Industrial Year [9509]
- MSci Computer Science with Study Abroad [5576]