Jobs in computer algebra and reasoning

		Integrating Computer Algebra and Reasoning

Applications are invited for two posts related to the ESPRC-supported 3 year project 

	"Adding the Axioms to Axiom: Integrating Computer Algebra and Reasoning" 
at the University of Kent, in the Computing Laboratory (investigator Simon Thompson)
and Institute of Mathematics (investigator John Shackell). 

The project aims to explore the integration of reasoning
capabilities into the Aldor library compiler for the Axiom computer algebra
system, and to use this integrated logic to improve support for symbolic 
mathematics. The integration is achieved using the embedding of `propositions 
as types' in a modified version of the Aldor type system.

Integrating a logic into Aldor will make the practice of symbolic mathematics
more reliable - by incorporating conditions on the application of
certain operations, for instance. It will also extend what it is possible to
achieve with CA by allowing logical reasoning as a part of symbolic computation.
As a part of the project, the system developed will be applied to a case study
of symbolic asymptotics.

More details of the project can be found at the URL:
or by e-mail enquiry to S.J.Thompson@ukc.ac.uk or J.R.Shackell@ukc.ac.uk.

Post 1: Post-Doctoral Research Associate (RA1A) 

The Research Assistant will play a central role in the project, working on
  - the theory of the current system of types in Aldor and of extensions to it;
  - practical modifications of the Aldor system itself.

A successful applicant for this post will have a background including
`theoretical' aspects of computer science such as type theories, computer-
assisted reasoning and program semantics. He or she will also be expected to 
perform some programming in C (and possibly a functional language)
in modifying the Aldor system.

Salary will be within the scale 15,735-23,651 pounds. Further particulars can
be obtained from the Personnel Office, quoting reference A99/45.  Please 
telephone the Personnel Office for Further Particulars on
(+44)-1227-827837 (24 hours) or (+44)-1227-823674 (Minicom).

Post 2: Postgraduate Student

The postgraduate student will work on the case study of symbolic asymptotics.

We are looking for someone with a First or good Upper-Second in Mathematics or
Mathematics/Computer Science with at least some experience of programming, or
alternatively a Computer Science graduate with strong Mathematical abilities.
Familiarity with an Algebra System would be an asset, but the willingness to 
learn to program in Aldor is more important. 

This studentship (including maintenance of 6455 pounds) is available to applicants from
any EU member country. Initial enquiries  should be made to Dr John
Shackell, Institute of Mathematics, University of Kent, Canterbury, CT2 7NF,
e-mail J.R.Shackell@ukc.ac.uk, telephone (+44)-1227-823800.

CLOSING DATE: 19 February 1999.