| 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 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 |