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