EPSRC Reference: 
GR/M37851/01 
Title: 
INTERGRATING COMPUTER ALGEBRA AND REASONING: INCORPORATING A LOGIC INTO THE AXIOM SYSTEM 
Principal Investigator: 
Thompson, Professor S 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Sch of Computing 
Organisation: 
University of Kent 
Scheme: 
Standard Research (PreFEC) 
Starts: 
01 July 1999 
Ends: 
30 September 2002 
Value (£): 
203,148

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 

Summary on Grant Application Form 
The principal aim of the programme is to build a reasoning capability within the Axiom computer algebra (CA) system. This will be based on a modification of the Axiom type system to allow the evaluation of type expressions. This allows the types of Axiom to represent logical formulas, and functions to represent proofs. In order to make the integration sound, we will describe a typesecure subset of Axiom, Axiom, in which reasoning will take place.The construction will be accompanied by a substantial case study in symbolic asymptotics. This will both develop new work in mathematics and also explore how logic extends the capabilities of CA systems, by, for instance, using the logic to represent pre and postconditions such as zero equivalence.As a necessary step towards making the modification, we will first give a formal definition of the type system of Axiom. We will also explore how to extend the type system to include algebraic/inductive types, as well as describing a series of (smaller) algebraic examples.A final goal will be to define an interface between Axiom and existing theorem provers such as Coq and Lego to support largerscale, machine assisted verification in Axiom.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.kent.ac.uk 