# Module 06-26264 (2015)

## Reasoning

## Level 2/I

Volker Sorge | Semester 2 | 10 credits |

Co-ordinator: Volker Sorge

Reviewer: Manfred Kerber

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]