Course pages 2012–13
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.
- 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.
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 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.
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.
The assessment will be done by the lecturer and will consist of three parts:
- The write-up of the literature survey (term paper) will account for 30% of the final mark.
- 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.
- A written test at the end of the course will account for 60% of the mark. The final grade for the course will be provided as a percentage.
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/
L18 Automated Reasoning cannot be taken in conjunction with P34 Advanced Computer Design or R05 Chip Multiprocessors in 2012-13.
Class limit: 16 students