# Module 06-26264 (2014)

## Reasoning

## Level 2/I

Volker Sorge | Semester 2 | 10 credits |

### 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 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 [0144]
- BSc Artificial Intelligence & Computer Science with an Industrial Year [9502]
- 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]