| EPSRC Reference: |
GR/L48256/01 |
| Title: |
EMBEDDED VERIFICATION TECHNIQUES FOR COMPUTER ALGEBRA SYSTEMS |
| Principal Investigator: |
Martin, Professor UH |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of St Andrews |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 1997 |
Ends: |
28 February 2001 |
Value (£): |
216,761
|
| 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 |
|
This is a collaborative project between Mike Dewar of NAG Ltd, developers of the computer algebra system AXIOM and Ursula Martin and Steve Linton of St Andrews university, researchers of international standing in automated theorem proving, algebra and the application of the former to the latter. A goal of much research in the computational logic (CL) is to produce mathematical assistants. A plethora of advanced systems and significant theoretical results have been produced over the last 30 years. Computer algebra systems (CAS) have become standard tools, but few non-specialists understand or use automated theorem provers (ATP). We want to investigate hoe to enhance CAS using the techniques of CL, so as to give users the advantages of the methods of ATP while shielding them from their technicalities. This is in line with recent work on embedded verification techniques (EVT) in domains such as CAD and databases. We expect to produce demonstrator software and sound theoretical analyses and to focus what we are doing by working with local experts on three diverse use cases: combinatorics, theoretical physics and mathematical education, thus providing an evaluation of what CL techniques are of most value as EVT for CAS.
|
|
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.st-and.ac.uk |