Module 06-26264 (2014)
|Volker Sorge||Semester 2||10 credits|
The module will introduce automated theorem proving. Both implementation and representation theories are covered as are some applications.
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.
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
- 06-21155 - Language & Logic
three-hour weekly lectures/labs.
Contact Hours: 34
Sessional: 1.5 hr examination (80%), continuous assessment (20%).
Supplementary (where allowed): By 1.5 hr examination only (100%).
- 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 3. 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 4. 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 
- BSc Artificial Intelligence & Computer Science with an Industrial Year 
- BSc Computer Science 
- BSc Computer Science with an Industrial Year 
- BSc Computer Science with Study Abroad 
- MSci Computer Science 
- MSci Computer Science with an Industrial Year 
- MSci Computer Science with Study Abroad