The Scottish Theorem Proving seminar series

11th December 1998
Mathematical Reasoning Group
Division of Informatics
University of Edinburgh

14:00 - 17:00

Room F10
80 South Bridge
Edinburgh.

Programme

14:00 Start & Welcome
14:10 - 14:40 Implementing the General Matings Method in Isabelle
Claire Quigley, University of Glasgow.
14:50 - 15:20 The Use of Proofs-as-Programs to Build
an Analogy Based Functional Program Editor
Jon Whittle, University of Edinburgh.
15:30 Refreshments & Demonstration of Cynthia
16:00 - 16:45 Annotated Reasoning as a Generalization of Rippling
Dieter Hutter, DFKI, Saarbrücken, Germany.
17:00 Finish
Times in red are fixed.
Times in blue are flexible.

How to get to the venue

The best way to get to the venue if you are not already in Edinburgh is by train. 80 South Bridge is conveniently located within walking distance of Waverley railway station. The shortest way to get from the station is to go up the steps from the station concourse to the overhead walkway and go to the Market Street exit (not the Princes Street exit). From the Market Street exit, cross the road at the pedestrian crossing a few metres to the right and go up the steep steps on the other side (Fleshmarket Close). At the top you'll emerge onto a street that curves upwards to the left onto the High Street (Royal Mile). Follow the street onto the Royal Mile and then head down the Royal Mile to the left for a few metres. Cross over at the pedestrian crossing in front of the Tron Kirk (church). Follow the pavement on the left side of the church. This is South Bridge. The entrance to our building is shortly before the junction with Chambers Street, between O'Neills pub and the Camping & Outdoor Centre.

The inner door will be locked but there is usually a servitor on duty to let you in. If not, use the intercom by the door. Tell the servitor you are here for a seminar and mention my name (Richard Boulton) if necessary. Go up the stairs to Level F then follow the corridor through four fire doors. Room F10, where the seminar will be, is on the right. If you come for lunch, go round the corner to F9 where you should find someone from the Mathematical Reasoning Group to meet you.

If you do find yourself on Princes Street after emerging from Waverley station, turn right, and then right again at the junction with North Bridge. Follow North Bridge to the junction with the Royal Mile and go straight on onto South Bridge. Then follow the instructions above.

If coming by bus, from the central bus station at St Andrew Square ask someone to point you in the direction of Princes Street and then North Bridge. Parking in the centre of Edinburgh is limited, so travelling by car is not recommended. You may find the travel information provided by the University, in particular the maps of Edinburgh, helpful.

Lunch

There are plenty of places to buy sandwiches on South Bridge and in the vicinity, and there is a common room on Level G (the top floor) of 80 South Bridge where you may eat them. There are also a number of places to eat-in in the area, such as: Two lunch groups will leave room F9 at 12:15 sharp, one to the café at John Knox House and the other to the Kalpna (Indian food, buffet style).

Abstracts

Implementing the General Matings Method in Isabelle
Claire Quigley, University of Glasgow

In this talk I will describe the implementation of mating_tac - an Isabelle tactic based on Peter Andrews' Theory of General Matings. The tactic uses the matings method (similar to tableau methods) to search for a proof, before passing the result to Isabelle for checking. I chose to implement the method in Isabelle as the use of the matings method to prove statements in Higher Order Logic requires higher order unification which, unlike some other LCF style provers, Isabelle provides.

The Use of Proofs-as-Programs to Build an Analogy Based Functional Program Editor
Jon Whittle, University of Edinburgh

CYNTHIA is a novel editor for ML that uses proofs-as-programs to represent each function definition. Proofs-as-programs provides a nice framework for the analysis, editing and feedback of users' programs. Each definition has an associated (weak) specification in type theory. The proof of this specification guarantees that any program written in Cynthia is syntactically correct, type correct, terminating and has exhaustive / irredundant patterns. Cynthia's interface means that the user need have no knowledge of logic and proof. Cynthia has been successfully evaluated on two groups of students at Napier University. A short demo of Cynthia will also be given.

Annotated Reasoning as a Generalization of Rippling
Dieter Hutter, DFKI, Saarbrücken, Germany

The use of proof planning techniques in automating deduction results in the need of dealing and maintaining strategic knowledge within the deductive process. In our talk we present a methodology to encode such knowledge into underlying logical structures and to maintain the knowledge by an enhanced inference mechanism. In doing so, strategic knowledge is encoded by annotations of the basic objects of the underlying logic, which are for instance the occurrences of function, predicate, or junction symbols. The enhanced inference mechanism takes care about these annotations and propagate the distributed knowledge along the deduction process. Information functions are used to decode the knowledge from the annotations and are abstractions on the annotated structures. The restrictions to admissible values of this function wrt. to an intermediate deduction step represents an abstract proof. Then, the refinement of the abstract proof is concerned with the selection of appropriate deduction steps which fulfill the postulated restrictions.
Return to Scottish Theorem Proving page.