Department of Computer Science and Technology

Course pages 2019–20

Automated Reasoning

Principal lecturer: Prof 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

Topics may include - to be confirmed in September 2019:

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

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

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. Full details will follow in September preceding the start of Michaelmas term:

  • A literature survey 35%;
  • A presentation of an in-depth analysis of a selected research paper and reading group participation 15%; and
  • A written test of up to 90 minutes in duration 50%.

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