The Scottish Theorem Proving seminar series

Friday 10th December 1999
Department of Computing Science
University of Glasgow

14:00 - 17:00

Room 111
Modern Languages
University of Glasgow
Glasgow.

How to get here

If you know where the Computing Science department is then the Modern Languages building is easy to find. There is a car park next to the Computing Science department. On the other side of the car park is the Queen Margret student union. The Modern Languages building is next to this.

Some information on how to get to the Computing Science department is given on the departmental pages. The Modern Language building is on University Gardens (marked D5) on the map. It is worth noting that it is difficult to find parking spaces around the university.

Instructions for getting here from Rail Station:

Get into the underground and go around to Hillhead Station. The department is just up the hill "behind" the station: 

      ---------- Byres Road -----U------------+-------------
                             (Hillhead)       |
                                              |
                                              | (Great George Street)
                                              |
                         Big Car Park         |
             /--------------------------------+
             |             Grass              |
         ___ \-------------------------------+ <<--- Lilybank Gardens
  _____ /QM | Car [][][][][] Houses [][][][][] |
 /Modern      Park    Computing Science
  languages
Room 111 is on the first floor of the modern languages building. Go in the front door and go up one floor. The room is the first room along the corridor that goes towards the back of the building.

Programme

1400 - 1500 "Prosper"
Louise Dennis, Graham Collins, University of Glasgow
Lex Holt, University of Edinburgh
1500 - 1530 Tea/Coffee
1530 - 1600 "Proving correctness of computer algebra gcd and lcm procedures."
Tom Kelsey, University of St Andrews
1600 - 1645 "A Critique of Proof Planning"
Alan Bundy, University of Edinburgh

Abstracts

Proving correctness of computer algebra gcd and lcm procedures.
Tom Kelsey, University of St Andrews

We describe the proof, using LP, of properties of specifications of gcd and lcm procedures contained in the AXIOM computer algebra system. We illustrate the strengths and weaknesses of applying a first order proof system to complex abstract algebraic issues, with particular respect to the verification of the correctness of computational methods for abstract division within integral domains.

PROSPER

Three short (<20min) talks covering some of the work that the Scottish partners in the PROSPER project have been doing.

Louise Dennis, University of Glasgow - The PROSPER Toolkit
Graham Collins, University of Glasgow - Adding verification to Microsoft Excel
Lex Holt, University of Edinburgh - Natural Language Interface

A Critique of Proof Planning
Alan Bundy, University of Edinburgh

Proof planning is an approach to the automation of theorem proving in which search is conducted, not at the object level, but among a set of proof tactics. This approach dramatically reduces the amount of search but at the cost of completeness. We critically examine proof planning, identifying both its strengths and weaknesses. We use this analysis to explore ways of enhancing proof planning to overcome its current weaknesses.
Return to Scottish Theorem Proving page.