[FOM] Mechanising Proof

Roger Bishop Jones rbj at rbjones.com
Tue Jul 8 11:45:27 EDT 2003


In connection with Harvey Friedman's recent postings
on proof checking and program verification,
the following reference may be of interest.
(previously mentioned on FOM but not much discussed)

"Mechanising Proof: Computing, Risk, and Trust"
by Donald MacKenzie
ISBN 0-262-13393-8

The book gives a good historical account of the
connections between mechanised inference and proof
checking and their applications, including software
and hardware verification.

(it also, incidentally, confirms my speculation
about the half century by dating Martin Davis'
implementation of the Pressburger decision
procedure to 1954)

Roger Jones


More information about the FOM mailing list