Computer Laboratory

Course pages 2015–16

Automated Reasoning

Principal lecturer: Dr Mateja Jamnik
Taken by: MPhil ACS, Part III
Code: L18
Hours: 16
Class limit: 16 students
Prerequisites: Familiarity with basic logic and artificial intelligence beneficial

Aims

This module aims to provide an introduction to how reasoning can be automated. In particular, the course will introduce students to fundamental techniques for designing automated reasoners, provide some experience of how they work and how to use them, and present advanced applications of theorem proving for solving problems via automated reasoning.

Syllabus

  • Introduction to automated reasoning and history of automated theorem provers. [1 lecture]
  • Brief review of mathematical logic: representations, propositional, predicate logic, semantics. [1 lecture]
  • Representing mathematical knowledge using logic. [1 lecture]
  • Proof and correctness: formalization of proof, inference rules and resolution, unification, equational reasoning, combinatorial explosion, search algorithms. [3 lectures]
  • Guidance techniques: rewrite rules, human proofs, decision procedures, meta-level inference. [2 lectures]
  • Inductive theorem proving, heuristic guidance, rippling, proof planning. [2 lectures]
  • Applied uses of automated reasoning: diagrammatic reasoning, ontology/semantic web. [2 lectures]
  • Student presentations of reviews/rational reconstructions of topics in automated reasoning. [4 lectures]

Note that some content may vary, and the number of lectures per topic is provisional; the final plan will depend on the students' background and the number of students taking the course.

Objectives

On completion of this module, students should:

  • be able to represent mathematical and other knowledge using logical formalism;
  • understand the history of formalizing mathematical knowledge;
  • know and understand the advantages and limitations of the main approaches and techniques in automated reasoning of mathematical knowledge;
  • be able to apply different automated reasoning techniques to new problems;
  • be able to locate, read, understand, and present a research paper from the field;
  • be familiar with current research in a number of aspects of the field;
  • be able to critically analyze and evaluate a piece of research.

Coursework

Coursework will consist of two practical exercises.

First, students will be able to select one of a list of topics in automated reasoning and carry out a literature survey of state-of-the-art research on this topic. The literature survey should be 10 pages long and be based on approximately 10-20 papers.

Second, students will be able to select a research paper from a list of papers describing one of state-of-the-art reasoning systems, do a review (an in-depth analysis) of the work described in the paper, and give a short presentation about it to the rest of the class.

Practical work

Exercises will be given to students during lectures that will enable students to practice and apply principles discussed in the lectures. Solutions to exercises should be submitted, but will not be assessed. Feedback will be provided as appropriate.

Assessment

The assessment will be done by the lecturer and will consist of three parts:

  • A literature survey of at most 3,500-words excluding mathematical formula, figures and bibliography (30% of the final mark);
  • A presentation of an in-depth analysis of a selected research paper and a completed review form (10%); and
  • A written test of 1 hour and 30 minutes duration with an additional 15 minutes of reading time (60%).

Recommended reading

Bundy, A. (1983). The computer modelling of mathematical reasoning. London: Academic Press (2nd ed.). Out of print, but available on-line from: http://www.inf.ed.ac.uk/teaching/courses/ar/book/book-postcript/

Notes:

Class limit: 16 students