## Computer Assisted Proof for Mathematics: an Introduction using
the LEGO Proof System

**Rod Burstall**
*Abstract:* We give brief account of the use of computers
to help us develop mathematical proofs, acting as a clerical
assistant with knowledge of logical rules. The paper then focusses
on one such system, Pollack's LEGO, based on the Calculus of
Constructions, and it shows how this may be used to define
mathematical concepts and express proofs. We aim at a gentle
introduction, rather than a technical exposition.

*LFCS report ECS-LFCS-91-132*

Previous |

Index |

Next