EPSRC logo

Details of Grant 

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:
Shackell, Professor J
Researcher Co-Investigators:
Project Partners:
Department: Sch of Computing
Organisation: University of Kent
Scheme: Standard Research (Pre-FEC)
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 type-secure 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 post-conditions 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 larger-scale, 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 non-academic 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