| 14:00 | Welcome 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 |
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.
http://www.strath.ac.uk/Campus/images/strath/jacampus.gif
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 http://www.cs.strath.ac.uk/~ipg/home/CB1.gif
| Return to Scottish Theorem Proving page. |
