Computer Aided Formal Reasoning, 1996/7

Course Information


Judith Underwood
JCMB 1603
50 5185

Where and When

The course meets Tuesdays at noon in room 3218 and Thursdays at 2:00pm in room 3317, through 6 December.

We will be using the Lego proof assistant extensively during the course. To help you get started with the system, I plan to arrange a few lab/tutorial sessions during the first half of the course. These will probably be in the lab in room 2501.


A rough outline of the course is:

There is some flexibility in the later part of the term, and once the foundation has been laid I will offer the class a number of topics to choose from.

Reading List

Background material

A couple of books on proof, useful if you do not have much experience with mathematical proofs in practice are:

Kelleman, D.J. (1994) How to Prove it: a Structured Approach. (£14.95) and

Exner, George R. (1996) An Accompaniment to Higher Mathematics. (£22.50) This book is designed for undergraduate mathematics students, but contains a good deal of practical logic as well, and is written in a very friendly style.

For background mathematics which you might need to catch up on, the following book covers the material needed without too much elaboration.

Truss, J.K. (1991) Discrete Mathematics for Computer Scientists, Addison Wesley (£19.95). See especially chapters 1, 2, 5 and 6.

For background in functional programming, using ML, see Paulson (1991) ML for the Working Programmer.

For background in lambda-calculus, see Gunter (1992), Semantics of Programming Languages, sections 2.1 and 2.2.

Main books relevant to the course

There is no set text for the course. Lecture notes will be distributed, which will cover all examinable material. The books below give more details on the topics covered. The most suitable for M.Sc. students are probably Thompson and chapters 7 and 8 of Luo. Ph.D. students may be interested in Proofs and Types.

Thompson, S. (1991) Type Theory and Functional Programming, Addison Wesley (about £24.95).

Luo, Z. 1994 Computation and Reasoning: a type theory for computer science. Clarendon Press, Oxford (£30.00).

Girard, Lafont and Taylor. Proofs and Types. Cambridge (about £18).

Nordstrom, B., Petersson, K. and Smith, J. (1990) Programming in Martin-Lof Type Theory: an introduction. Clarendon Press, Oxford.

For related reading in resolution and automatic theorem proving, see

Bundy, A. (1983) The Computer Modelling of Mathematical Reasoning. Academic Press.

Judith Underwood
Wed Oct 2 16:22:27 BST 1996