Module 06-26264 (2017)

The module will introduce automated theorem proving. Both implementation and representation theories are covered as are some applications.

• 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.

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

None

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

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