Computer Laboratory

Course pages 2011–12

Automated Reasoning

Principal lecturer: Dr Mateja Jamnik
Taken by: MPhil ACS, Part III
Code: L18
Hours: 16
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 uses of theorem proving for solving mathematical 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, machine creativity. [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 about 10 pages long and be based on approximately 10-30 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

Some 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:

1. The write-up of the literature survey (term paper) will account for 25% of the final mark.
2. The student's presentation of the review (an in-depth analysis) of an existing automated reasoning system together with a short assigned filled review form for the research paper (course work) will account for 10% of the final mark.
3. A written test at the end of the course will account for 65% of the mark. The final grade for the course will be provided as a percentage.