The Scottish Theorem Proving seminar series
14:00 - 17:00
80 South Bridge
Times in red are fixed.
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.
Refreshments & Demonstration of Cynthia
16:00 - 16:45
Annotated Reasoning as a Generalization of Rippling
Dieter Hutter, DFKI, Saarbrücken, Germany.
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.
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).
The café at
House on the High Street (Royal Mile), a short way down the hill from the
junction with North and South Bridge, on the left-hand side. (Good, reasonably
Number One Brasserie on the corner of South Bridge and Chambers Street,
directly below our offices. (Fairly expensive.)
Nicolson's restaurant, just beyond the James Thin bookshop and across the
road from the Festival Theatre on South Bridge / Nicolson Street. The
restaurant is upstairs from the street. (For people who have a more
significant appetite at lunchtime.)
In this talk I will describe the implementation of mating_tac - an
tactic based on
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
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.
University of Edinburgh
Annotated Reasoning as a Generalization of Rippling
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.
DFKI, Saarbrücken, Germany