Lemmas and Heuristics
The cartoon below was drawn by Martin Pollock, sometime in 1971 or 1972, when Bob Boyer and I
were working in the Metamathematics Unit (which became the Department of Computational Logic)
at the University of Edinburgh. Martin's wife Jean was a secretary in the Unit and frequently
typed incomprehensible theorem proving manuscripts. This was Martin's response to a paper
by the head of the Unit, Bernard Meltzer. Martin Pollock, FRS, was a molecular biologist who was well known at the university for his satirical cartoons as well as for being a founding father of molecular biology as a distinct field.
Lemmas and Heuristics
