Scottish Theorem Proving

There will be a meeting of STP in St Andrews on December 14th 2001, in the School of Computer Science, North Haugh, St Andrews, from 2.00 to 6.00 pm.

The meeting is in Theatre B of the building (labelled "Physics and Astronomy") housing the staff of the School of Computer Science. For obvious reasons, there is no mention on the outside of thisbuilding that it houses any computer scientists. It is building 19 on the map in How to get to the School of Computer Science; or maybe you need How to get to St Andrews first.

If planning to come beforehand to lunch , the arrangements are that we meet at 12.30, at the building just mentioned, for the five minute walk to New Hall, where there is a cafeteria serving cheap but dull food, and lots of space. It is building 70 on the map. Late arrivals should just go straight to New Hall---parking is available there as well as here.





This talk will review the histories of mathematical proofs about computer systems (that is, of formal verification) and of proofs using computer systems (automated theorem proving, the proof of the four-colour theorem), etc. It will explain why these histories are of interest to the sociology of science, will discuss the first litigation centring on the nature of mathematical proof, and will explore the "cultures of proving" within which different forms of proof are pursued.


Organised by R. Dyckhoff and Ursula Martin