| EPSRC Reference: |
GR/R84092/02 |
| Title: |
Pythagoras: Machine Support for Semi-formalised Proof Oriented Mathematics |
| Principal Investigator: |
Luo, Professor Z |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Royal Holloway, Univ of London |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 2004 |
Ends: |
31 December 2006 |
Value (£): |
83,200
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Logic & Combinatorics |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Machine support for both numerical and symbolic computational mathematics has been very successfully used in mathematics, science and education. This proposal aims to investigate the issues involved in the achievement of such support for proof oriented mathematics. We believe that the theory and technology of interactive theorem proving can be effectively applied to building tools to help research mathematicians as well as students of mathematics in their proof development effort. We believe that a key to this is to focus not on the full formalisation of mathematics but on what we here call semi-formalised mathematics. This is mathematics which is completely formal as far as the formulation of definitions and results is concerned, but where proofs are allowed to have steps which may not be instances of rules of inference, but instead are documented with various kinds of less formal evidence for the step. We shall study the theory and techniques needed to build supporting computer environments for the development and presentation of semi-formal mathematics. Our method is to implement a generic environment based on an existing proof development system. We will develop and implement techniques of meta-variables in multiple-contexts that will provide effective support for the representation and development of semi-formal proofs. The evaluation will be conducted via case studies for educational uses of our tools in Mathematics and Computer Science courses.
|
|
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: |
|