Scottish Theorem Provers Seminar
Tuesday 23rd June, 1998
Room B221 (the Board Room),
Glasgow Caledonian University,
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,
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.
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.