The Scottish Theorem Proving seminar series

Friday 26th February 1999

Committee Room 1,
Collins Building,
Richmond St,

14:00 - 16:45


Toby Walsh, Strathclyde University
14:10 "Theorem Proving at Full Throttle"
Helen Lowe,
Glasgow Caledonian University
14:50 "Automatic Theorem Generation in Finite Algebras"
Simon Colton,
Edinburgh University
15:30 Tea
16:00"Life after Theorem Proving"
4.00 Judith Underwood,
QSS Ltd, Edinburgh
16:45: Close


For those interested in lunch, please contact Toby,


Theorem Proving at Full Throttle
Helen Lowe, Glasgow Caledonian University

I am probably the only person in the entire world to have written a formal specification for speedway . . .

The role of proof in formal systems development is too often neglected in undergraduate courses on formal methods. I have never seen the point of teaching this subject merely as another notation. To me, the point of formal methods is to find mistakes, clear up misunderstandings, and resolve ambiguities.

Always on the lookout for engaging examples, I was inspired by the "Soccer referee's book" example used by Yves Ledru for teaching 5th year students at Universite' Joseph Fourier. I liked the general idea, but it is limited. Speedway, on the other hand, is full of ambiguities, contradictions, missing cases, and sheer incomprehensibility. Moreover, the rules are constantly changing in the quest to achieve both justice and excitement, giving even more scope for faulty specification and eleventh hour patches.

In this talk I will give examples of possible rule violations, ambiguities, and incompleteness, and show how a formalization might be of help (but to not your average speedway referee, obviously - unless we automate the process ... but that is another story.)

Automatic Theorem Generation in Finite Algebras
Simon Colton, Edinburgh University

The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties of concepts and assesses the theorems and proofs involving them to estimate the interestingness of each concept and employ a best first search. This approach has led HR to the discovery of interesting new mathematics and enables it to build theories from just the axioms of finite algebras. I'll be concentrating on how HR makes, assesses and settles conjectures in finite algebras.

Life after Theorem Proving
Judith Underwood, QSS Ltd, Edinburgh

What does a type theorist do when she has to earn a buck? I will talk about life as a software engineer in the `real world'. I will also give an overview for theorem provers of requirements management, which is at the heart of QSS's main product.


There is a map of the campus at

The Collins Building is building number 14 on this map, in Richmond St.

Not having a car, I am not a good person for advice in that case. However there is a multi storey car park in Montrose St, and it's marked in the map pointed to above. It's 2 minutes walk from the meeting room.

Glasgow Queen St train station is about 5 minutes walk from the room, 10 minutes if you don't know the way. Out of the main entrance, turn left onto George St, and take the fourth left onto Montrose St. Montrose St rises sharply uphill and the junction has traffic lights. Turn first right into Richmond St.

You go to the other end of the bus station away from the passenger concourse, and then turn right down North Hanover St. Then turn left onto Cathedral St, taking the second right onto Montrose St.

From Glasgow Central or alternatively Buchanan St underground it is a short walk to Queen St, from which you can follow the earlier instructions. A map of the area from Central to Queen St is at

Return to Scottish Theorem Proving page.