School of Computer Science

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:

  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

Restrictions

None


Pre-requisites


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

  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