School of Computer Science

Module 06-26264 (2016)


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.


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.

Learning Outcomes

On successful completion of this module, the student should be able to:

  1. describe the basic concepts of automated theorem proving
  2. demonstrate an understanding of applications of automated theorem proving
  3. demonstrate an understanding of the techniques of implementing automated theorem provers
  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




Teaching methods

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%).

Detailed Syllabus

  1. Introduction and preliminaries
  2. 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