Scottish Theorem Provers Seminar

Tuesday 23rd June, 1998

2-5pm

Room B221 (the Board Room),

Britannia Building,

Glasgow Caledonian University,

Cowcaddens Road,

Glasgow

Programme

Directions


Programme

 
14:00 Welcome 
14:10-14:40 Computers, theorem proving and mathematical practise  
 
Ursula Martin, St Andrews
14:50-15:20 From Proofs to Programs ... and back again Ian Gent, Strathclyde
15:30-16:00 Tea/coffee 
 
16:00-16:30 Symbolic Bisimulations for Full LOTOS 
 
Carron Shankland, Stirling
16:40 Close

Abstracts

Computers, theorem proving and mathematical practise

Ursula Martin, St Andrews

Computer aided formal reasoning, mathematical assistants and automated proofs of new and interesting mathematical results have been part of the dream of  computational logic for many years, and there have been some impressive achievements.  Yet it is still the case that few mathematicians use such programs, and their impact outside certain specialised communities has been less that might have been
 hoped.  The main impact of computation on research mathematics has been through ,experiment, using systems like Maple,  construction, in for example the classification of finite simple groups, or computations used as part of a traditional mathematical proof, like that of the four colour theorem, but in many of the major achievements of 20th century mathematics the role of computation has been slight. There is nothing to compare with the achievements of numerical techniques: without computation we would have no Mars pathfinder robot, no human genome project and no CAT scans.  We might still have the proof of Fermat's theorem.

In the light of this we suggest a new agenda for computer aided reasoning, aimed at  enhancing the techniques  available for mathematical experimentation, developing community standards for experiment and modelling and developing methods which  will make computation more acceptable as part of a proof.



 

From Proofs to Programs ... and back again

Ian Gent, Strathclyde

I will give an informal report on how Judith Underwood, Jim Caldwell and I went about extracting runnable code from a type theoretic proof of correctness. The process was not unidirectional, and computational experiments I performed fed back into the Nuprl proof and extract which Jim and Judith provided.
 



 

Symbolic Bisimulations for Full LOTOS

Carron Shankland, Stirling

Full LOTOS is an ISO standard message passing process algebra. One of the problems of reasoning about Full LOTOS processes is we cannot reason about partial specifications (i.e. behaviour expressions parameterised over data), because the standard semantics gives meaning only to processes with ground data. This is a consequence of the approach taken to accommodate multi-way synchronisation, i.e. associative synchronisation between two or more processes, in the language.

We tackle this problem by defining a symbolic semantics for Full LOTOS in terms of symbolic transition systems; the semantics extends the standard one by giving meaning to symbolic, or (data) parameterised processes.   To support reasoning over these processes we define symbolic bisimulation and a related modal logic are defined.  Symbolic bisimulation preserves the usual concrete (strong) bisimul
ation on the standard semantics.

The approach taken follows that of message passing CCS in [Hennessy & Lin 95], but differs in several significant aspects, taking account of the particular features of LOTOS (multi-way synchronisation, value negotiation, selection predicates).

I will present the symbolic transition system and symbolic bisimulation, illustrating with reference to examples.  An outline of the logic will presented if there is time.



 

Directions

The meeting is on the City Campus of Glasgow Caledonian University, which is on Cowacaddens Road, opposite Buchanan Street Bus Station. If you are travelling by rail, it is about five minutes walk from Queen Street station; nearby undergound stations are Buchanan Street and Cowcaddns. The Britannia Building is on your left as you enter the campus. It is shaped like a pound (£) sign, although this may possibly only be apparent if you arrive by helicopter.